Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes

Bodirsky, Manuel; Guzmán-Pro, Santiago

doi:10.4230/LIPIcs.CSL.2026.6

Hereditary First-Order Logic:
the Tractable Quantifier Prefix Classes

Manuel Bodirsky

Institut für Algebra, TU Dresden, Germany Santiago Guzmán-Pro

Institut für Algebra, TU Dresden, Germany

Abstract

Many computational problems can be modelled as the class of all finite structures $\mathbb{A}$ that satisfy a fixed first-order sentence $\phi$ hereditarily, i.e., we require that every (induced) substructure of $\mathbb{A}$ satisfies $\phi$ . We call the corresponding computational problem the hereditary model checking problem for $\phi$ , and denote it by $\operatorname{Her}(\phi)$ .

We present a complete description of the quantifier prefixes for $\phi$ such that $\operatorname{Her}(\phi)$ is in P; we show that for every other quantifier prefix there exists a formula $\phi$ with this prefix such that $\operatorname{Her}(\phi)$ is coNP-complete. Specifically, we show that if $Q$ is of the form $\forall^{\ast}\exists\forall^{\ast}$ or of the form $\forall^{\ast}\exists^{\ast}$ , then $\operatorname{Her}(\phi)$ can be solved in polynomial time whenever the quantifier prefix of $\phi$ is $Q$ . Otherwise, $Q$ contains $\exists\exists\forall$ or $\exists\forall\exists$ as a subword, and in this case, there is a first-order formula $\phi$ whose quantifier prefix is $Q$ and $\operatorname{Her}(\phi)$ is coNP-complete. Moreover, we show that there is no algorithm that decides for a given first-order formula $\phi$ whether $\operatorname{Her}(\phi)$ is in P (unless P $=$ NP).

Keywords and phrases:

Quantifier prefix, first-order Logic, Computational Complexity, Polynomial-time algorithm, coNP-completeness

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Complexity theory and logic

Related Version:

Full Version: https://arxiv.org/abs/2411.10860 [3]

Acknowledgements:

This is a low-co2 research paper: https://tcs4f.org/low-co2-v1. This research was developed, written, submitted and presented without the use of air travel.

Funding:

Both authors have been funded by the European Research Council (Project POCOCOP, ERC Synergy Grant 101071674). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them.

DOI:

10.4230/LIPIcs.CSL.2026.6

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Vertex-deletion problems were first studied as optimization problems [17, 18]: Given an input graph $\mathbb{G}$ determine the minimum number of vertices to be deleted so that the remaining (induced) subgraph belongs to a specified class $\mathcal{C}$ . Krishnamoorthy and Deo [17] showed that this problem is NP-hard for several natural graph classes $\mathcal{C}$ such as trees, planar, bipartite, hamiltonian, interval, and chordal graphs. Shortly after, Lewis and Yanakkakis [18] proved that if $\mathcal{C}$ is a non-trivial hereditary class of finite graphs (i.e., $\mathcal{C}$ is an infinite class of finite graphs which is closed under induced subgraphs and which is not the class of all finite graphs), then the vertex-deletion problem defined by $\mathcal{C}$ is $\operatorname{NP}$ -hard.

Given the previous hardness results, it was natural to study vertex-deletion problems from the viewpoint of approximation or of parametrized complexity. Regarding the former, Fujito [13] proposed a unified polynomial-time algorithm that approximates an optimal solution to a vertex-deletion problem defined by a non-trivial hereditary class. Some well-known results include the fixed parameter tractability of the odd-cycle transversal problem [21], and of the feedback vertex set problem [20] – the former corresponds to the vertex-deletion problem for bipartite graphs, and the latter to the vertex-deletion problem for forests.

Recently, the parametrized complexity perspective has been studied systematically for vertex-deletion problems defined by graph classes expressible by some first-order sentence $\phi$ [1, 12]. In this paper we are interested in the class of graphs $\mathbb{G}$ such that no matter how many vertices are removed from $\mathbb{G}$ , the remaining induced subgraph does not satisfy $\phi$ . Since first-order logic is closed under negations, we prefer the positive phrasing of this problem: Given a graph $\mathbb{G}$ , test whether all non-empty induced subgraphs of $\mathbb{G}$ satisfy a specified first-order formula $\psi$ .

Hereditary first-order logic

From now on we work in the setting of relational structures, for which graphs and digraphs are prototypical examples. We use the convention that all structures have a non-empty domain. We begin by introducing hereditary first-order logic. A structure $\mathbb{A}$ hereditarily satisfies $\phi$ if every substructure¹¹1Some authors use the term “induced substructure”; we follow the convention in model theory and omit the adjective ‘induced . $\mathbb{B}$ of $\mathbb{A}$ satisfies $\phi$ . We denote by $\operatorname{Her}(\phi)$ the class of finite structures that hereditarily satisfy $\phi$ . The hereditary model checking problem for a fixed sentence $\phi$ consists of deciding whether an input structure $\mathbb{A}$ belongs to $\operatorname{Her}(\phi)$ . Since verifying whether a finite structure $\mathbb{A}$ models a fixed first-order formula $\phi$ can be done in polynomial time, it follows that $\operatorname{Her}(\phi)$ is in coNP.

We say that a class $\mathcal{C}$ of finite $\tau$ -structures is hereditarily first-order definable if there is a first-order sentence $\phi$ such that $\mathcal{C}=\operatorname{Her}(\phi)$ . In this case, we also say that $\mathcal{C}$ is in $\operatorname{HerFO}$ . Clearly, every class in $\operatorname{HerFO}$ is hereditary, i.e., closed under taking substructures.

Three simple examples

Clearly, every hereditary class in $\operatorname{FO}$ is also in $\operatorname{HerFO}$ . The following graph and digraph classes are in $\operatorname{HerFO}$ , but not in $\operatorname{FO}$ .

Example 1 (Forests).

Consider a first-order formula $\phi$ stating that “there is a loopless vertex of degree at most $1$ ”. Clearly, every forest hereditarily satisfies $\phi$ . Conversely, suppose that $\mathbb{G}$ is a finite graph that hereditarily satisfies $\phi$ . Then $\mathbb{G}$ has a loopless vertex $v$ of degree at most $1$ . We inductively see that the subgraph with vertex set $(G\setminus\{v\})$ is a forest, i.e., has no cycles, and since $v$ has degree at most $1$ and does not have a loop, we conclude that $\mathbb{G}$ is a forest.²²2This example naturally generalizes to $k$ -degenerate graphs, i.e., the class of graphs $\mathbb{G}$ such that every subgraph of $\mathbb{G}$ contains a vertex of degree at most $k$ .

Example 2 (Chordal graphs).

A graph $\mathbb{G}$ is chordal if every cycle of $\mathbb{G}$ contains a chord; equivalently, if $\mathbb{G}$ contains no induced cycle of length $n\geq 4$ . Rose [22] proved that a graph $\mathbb{G}$ is chordal if and only if every induced subgraph contains a vertex whose neighbourhood induces a clique. Hence, if $\phi$ is a first-order sentence stating “there is a (loopless) vertex $v$ such that every two neighbours of $v$ are adjacent”, then $\operatorname{Her}(\phi)$ describes the class of chordal graphs. It is known that membership in this class can be decided in polynomial time [23].

Example 3 (Directed acyclic digraphs).

The class of acyclic digraphs belongs to $\operatorname{HerFO}$ as well. Indeed, it suffices to consider the first-order sentence $\exists x\forall y.\lnot E(x,y)$ , i.e., the first order sentence that states that there exists a sink, i.e., a vertex without outgoing edges. Equivalently, the constraint satisfaction problem for $(\mathbb{Q},<)$ (denoted by CSP $(\mathbb{Q},<)$ , see Section 2) is in $\operatorname{HerFO}$ . Also this computational problem can be solved in polynomial time (e.g., by depth-first-search).

We are interested in the expressive power of hereditary first-order logic, as well as complexity classification for the hereditary model checking problem. Regarding the former, we will see that $\operatorname{HerFO}$ is a particularly natural formalism when it comes to the description of constraint satisfaction problems (for the definition of CSPs, see Section 2). Regarding the latter, we will study complexity classifications based on the quantifier prefix of the fixed first-order sentence $\phi$ . This is motivated by similar classifications for universal and existential second-order logic [9, 14], which we now review.

Prefix classifications

It is straightforward to observe that $\operatorname{Her}(\phi)$ can be expressed in universal monadic second-order logic.

Observation 4.

Consider a first-order $\tau$ -formula $\phi:=Q_{1}x_{1}\dots Q_{n}x_{n}.\psi(x_{1},\dots,x_{n})$ and a finite structure $\mathbb{A}$ . If $S$ is a unary predicate not in $\tau$ , then $\mathbb{A}$ hereditarily satisfies $\phi$ if and only if $\mathbb{A}$ models

\forall S\;Q_{1}x_{1}\dots Q_{n}x_{n}\left(\exists z.S(z)\land\bigwedge_{i\in U% }S(x_{i})\implies\bigwedge_{i\in E}S(x_{i})\land\psi(x_{1},\dots,x_{n})\right),

where $U$ (respectively, $E$ ) is the set of indices $i\in\{1,\dots,n\}$ such that $Q_{i}$ is a universal (respectively, existential) quantifier.

The question whether a given existential second-order (ESO) sentence describes a polynomial-time solvable problem is easily seen to be undecidable (see, e.g., Theorem 1.4.2 in [2]). This motivates quantifier-prefix dichotomy results for existential second-order logic [9, 14]. For instance, the classification for monadic ESO is as follows [14, Figure 1(a)]. For every quantifier prefix $Q\in\{\exists,\forall\}^{\ast}$ the following holds:

$\blacksquare$

either $Q$ is of the form $\exists^{\ast}\forall$ , and in this case every monadic ESO sentence $\Phi$ whose first-order part has a quantifier-free prefix $Q$ is polynomial-time decidable, or
$\blacksquare$

$Q$ contains $\forall\forall$ or $\forall\exists$ as subwords, and in this case there is an ESO sentence $\Phi$ whose first-order part has quantifier prefix $Q$ and deciding $\Phi$ is NP-complete.

It follows from this classification, via Observation 4, that $\operatorname{Her}(\phi)$ is in P whenever $\phi$ is a first-order sentence with a quantifier prefix of the form $\forall^{*}\exists$ . However, as we will soon see, HerFO enjoys a richer polynomial-time solvable fragment.

Our contributions

We first study the expressive power of HerFO in the context of CSPs. We see that HerFO can express finite-domain CSPs note expressible in first-order logic (Example 25), that it can express coNP-complete infinite-domain CSPs (Theorem 8), and that every CSP expressible in HerFO is the CSP of an $\omega$ -categorical structure (Remark 6). We then turn to computational aspects of the hereditary model checking problem for fixed sentences $\phi$ . In particular, we show that if the signature of $\phi$ is monadic, then $\operatorname{Her}(\phi)$ is solvable in polynomial-time (Proposition 11).

Our first main results are two classifications of the computational complexity of problems in HerFO. The first one concerns sentences with at least one binary predicate (Theorem 20), and the second one concerns sentences $\phi$ such that $\operatorname{Her}(\phi)$ describes a CSP (Corollary 21). These classifications coincide, and are based on the quantifier prefix $Q\in\{\exists,\forall\}^{*}$ of the fixed first-order formula:

$\blacksquare$

either $Q$ is of the form $\forall^{*}\exists^{*}$ or the form $\forall^{*}\exists\forall^{*}$ , and in this case $\operatorname{Her}(\phi)$ is polynomial-time decidable for every first-order formula $\phi$ with quantifier prefix $Q$ , or
$\blacksquare$

$Q$ contains $\exists\exists\forall$ or $\exists\forall\exists$ as a subword, and in this case there are first-order sentences with quantifier prefix $Q$ such that $\operatorname{Her}(\phi)$ is $\operatorname{coNP}$ -complete.

Our final main result shows that more fine-grained classifications of the complexity are undecidable: there is no algorithm that tests for a given first-order sentence $\phi$ whether $\operatorname{Her}(\phi)$ can be solved in polynomial time (Theorem 23). Moreover, we show that this is also the case even if $\phi$ is restricted to having quantifier-prefix $Q=\exists\exists\exists\forall$ or $Q=\exists\forall\exists$ (Corollary 24). We leave open the decidability of this meta-problem for first-order sentences $\phi$ with quantifier prefix $\exists\exists\forall$ .

Outline

We begin by recalling some basic concepts from finite model theory (Section 2). We then list further examples of problems in HerFO, and prove that certain problems cannot be expressed in $\operatorname{HerFO}$ (Section 3); it will also become clear why hereditary model checking is quite natural in the context of constraint satisfaction. The classifications of the complexity of $\operatorname{HerFO}$ depending on the allowed quantifier prefix are the main results of Section 4. The undecidability of tractability of $\operatorname{HerFO}$ can be found in Section 5. A series of problems that are left open can be found in Section 6. In Appendix B we present a comparison between our complexity classifications, the complexity landscape for the parametrized version of HerFO from [12], and the general model checking problem for UMSO from [14].

2 Preliminaries

We assume basic familiarity with first-order logic and we follow standard notation from model theory, as, e.g., in [15]. We also use standard notions from complexity theory.

(First-order) structures

Given a relational signature $\tau$ and a $\tau$ -structure $\mathbb{A}$ , we denote by $R^{\mathbb{A}}$ the interpretation in $\mathbb{A}$ of a relation symbol $R\in\tau$ . Also, we denote relational structures with letters $\mathbb{A},\mathbb{B},\mathbb{C},\dots$ , and their domains by $A,B,C,\dots$ . In this article, structures have non-empty domains, and we only work with finite signatures $\tau$ .

If $\mathbb{A}$ and $\mathbb{B}$ are $\tau$ -structures, then a homomorphism from $\mathbb{A}$ to $\mathbb{B}$ is a map $f\colon A\to B$ such that for all $a_{1},\dots,a_{k}\in A$ and $R\in\tau$ of arity $k$ , if $(a_{1},\dots,a_{k})\in R^{\mathbb{A}}$ , then $R(f(a_{1}),\dots,f(a_{k}))\in R^{\mathbb{B}}$ . We write $\mathbb{A}\to\mathbb{B}$ if there exists a homomorphism from $\mathbb{A}$ to $\mathbb{B}$ , and we denote by $\operatorname{CSP}(\mathbb{B})$ the class of finite structures $\mathbb{A}$ such that $\mathbb{A}\to\mathbb{B}$ . Let ${\mathcal{C}}$ be a class of finite $\tau$ -structures. We say that ${\mathcal{C}}$ is

$\blacksquare$

closed under homomorphisms if for every $\mathbb{B}\in{\mathcal{C}}$ , if $\mathbb{B}\to\mathbb{A}$ , then $\mathbb{A}\in{\mathcal{C}}$ as well.
$\blacksquare$

closed under inverse homomorphisms if for every $\mathbb{B}\in{\mathcal{C}}$ , if $\mathbb{A}\to\mathbb{B}$ , then $\mathbb{A}\in{\mathcal{C}}$ as well (i.e., the complement of ${\mathcal{C}}$ in the class of all finite $\tau$ -structures is closed under homomorphisms).

Note that $\operatorname{CSP}(\mathbb{B})$ is closed under inverse homomorphisms.

If $\mathbb{A}$ and $\mathbb{B}$ are $\tau$ -structures with disjoint domains $A$ and $B$ , respectively, then the disjoint union $\mathbb{A}\uplus\mathbb{B}$ is the $\tau$ -structure $\mathbb{C}$ with domain $A\cup B$ and the relation $R^{\mathbb{C}}=R^{\mathbb{A}}\cup R^{\mathbb{B}}$ for every $R\in\tau$ . Note that $\operatorname{CSP}(\mathbb{B})$ is closed under disjoint unions, i.e., if $\mathbb{A}\in\operatorname{CSP}(\mathbb{B})$ and $\mathbb{B}\in\operatorname{CSP}(\mathbb{B})$ , then $\mathbb{A}\uplus\mathbb{B}\in\operatorname{CSP}(\mathbb{B})$ . It is well-known that a class of finite $\tau$ -structures ${\mathcal{C}}$ is of the form $\operatorname{CSP}(\mathbb{B})$ for some countably infinite $\tau$ -structure $\mathbb{B}$ if and only if ${\mathcal{C}}$ is closed under inverse homomorphisms and disjoint unions (see, e.g., [2, Lemma 1.1.8]).

For examples we will often use graphs and digraphs, and we will think of these as binary structures with signature $\{E\}$ . We follow and adapt standard notions from graph theory [6] to this setting. In particular, given a digraph $\mathbb{D}$ , we call $E^{\mathbb{D}}$ the edge set of $\mathbb{D}$ , and its elements we call edges. A graph is a digraph whose edge set is a symmetric relation, and an oriented graph is a digraph whose edge set is an anti-symmetric relation. Given a positive integer $n$ , we denote by $K_{n}$ the complete graph on $n$ vertices, and by $\vec{P_{n}}$ the directed path on $n$ vertices. An oriented path is an oriented graph whose symmetric closure is a path.

Fragments of first-order logic

A first-order $\tau$ -formula $\phi$ is called positive if it does not use the negation symbol $\neg$ (so it just uses the logical symbols $\forall,\exists,\wedge,\vee,=$ , variables and symbols from $\tau$ ). The negation of a positive formula is called negative; note that every negative formula is equivalent to a formula in prenex conjunctive normal form where every atomic formula appears in negated form, and all negation symbols are in front of atomic formulas; such formulas will also be called negative.

Consider a quantifier-free formula $\psi$ using only variables, the symbols $\land$ and $=$ , and symbols from $\tau$ , and let $\psi^{\prime}$ be the formula obtained from $\psi$ by iteratively removing each equality conjunct $x=y$ and substituting each occurrence of the variable $y$ by the variable $x$ . We now consider the structure $\mathbb{C}_{\psi}$ whose vertex set is the set of variables appearing in $\psi^{\prime}$ , and the interpretation of $R\in\tau$ consists of those tuples $\overline{x}$ such that $\psi^{\prime}$ contains the positive literal $R(\overline{x})$ . We say that a negative first-order sentence $\phi$ in prenex conjunctive normal form is connected if for every clause $\varphi$ of the quantifier-free part of $\phi$ , the structure $\mathbb{C}_{\lnot\varphi}$ is connected.

3 Hereditary model checking and CSPs

In this section we see that hereditary model checking naturally arises in the context of constraint satisfaction problems. We do so by providing several examples of $\operatorname{CSP}$ s in $\operatorname{HerFO}$ . We also include inexpressible examples of $\operatorname{HerFO}$ which help build intuition about hereditary model checking.

It is well-known that a universal first-order sentence $\phi$ in conjunctive normal form describes a $\operatorname{CSP}$ if $\phi$ is negative and connected (see, e.g., Theorem 5.6.2 in [2]). The following observation extends this to not necessarily universal sentences.

Observation 5.

The following statements hold for every first-order sentence $\phi$ in prenex conjunctive normal form.

$\blacksquare$

If $\phi$ is negative, then $\operatorname{Her}(\phi)$ is closed under inverse homomorphisms.
$\blacksquare$

If $\phi$ is negative and connected, then there is a structure $\mathbb{S}$ such that $\operatorname{Her}(\phi)=\operatorname{CSP}(\mathbb{S})$ .

Proof.

To prove the first itemized statement, suppose that there is a homomorphism $f\colon\mathbb{A}\to\mathbb{B}$ and $\mathbb{B}\in\operatorname{Her}(\phi)$ . Let $\mathbb{A}^{\prime}$ be a substructure of $\mathbb{A}$ . The substructure of $\mathbb{B}$ with vertex set $f[A^{\prime}]$ models $\phi$ . Suppose for contradiction that $\mathbb{A}^{\prime}$ does not satisfy $\phi$ . Then it would satisfy the sentence $\neg\phi$ , which is equivalent to a positive sentence. Since surjective homomorphisms preserve positive first-order formulas [15, Theorem 2.4.3], we obtain that $\mathbb{A}$ satisfies $\neg\phi$ , a contradiction.

It is straightforward to observe that if $\phi$ is negative and connected, then the class of finite models of $\phi$ is closed under disjoint unions. Hence, if every substructure of $\mathbb{A}$ and every substructure of $\mathbb{B}$ satisfies $\phi$ , then every substructure of $\mathbb{A}\uplus\mathbb{B}$ satisfies $\phi$ , i.e., $\operatorname{Her}(\phi)$ is closed under disjoint unions. By the first claim, $\operatorname{Her}(\phi)$ is also closed under inverse homomorphisms, and it thus follows that there is a structure $\mathbb{S}$ such that $\operatorname{CSP}(\mathbb{S})=\operatorname{Her}(\phi)$ – for any class ${\mathcal{C}}$ of $\tau$ -structures there exists a $\tau$ -structure $\mathbb{S}$ such that ${\mathcal{C}}=\operatorname{CSP}(\mathbb{S})$ if and only if ${\mathcal{C}}$ is closed under disjoint unions and inverse homomorphisms [2, Lemma 1.1.8]. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 6.

Every $\operatorname{CSP}$ in $\operatorname{HerFO}$ is the $\operatorname{CSP}$ of an $\omega$ -categorical structure (see [2] for the many consequences that the model theoretic property of $\omega$ -categoricity has for the study of the complexity of the CSP). This follows from a result in [5, Corollary 14], which states that every $\operatorname{CSP}$ in monadic second-order logic (MSO) is the $\operatorname{CSP}$ for an $\omega$ -categorical structure; clearly, $\operatorname{HerFO}$ is a fragment of monadic second-order logic (see, e.g., Observation 4). For a concrete application of this remark see Example 26.

Example 7.

Let $\tau=\{EQ,N\}$ be the signature where $E Q$ and $N$ are two binary relational symbols which will encode “equal” and “not equal”, respectively. Note that a $\tau$ -structure $\mathbb{A}$ belongs to $\operatorname{CSP}(\mathbb{N},=,\neq)$ if and only if the structure obtained from $\mathbb{A}$ by contracting all connected components of the edge relation $EQ^{\mathbb{A}}$ contains no loop $N(x,x)$ . Equivalently, $\mathbb{A}\in\operatorname{CSP}(\mathbb{N},=,\neq)$ if and only if $N^{\mathbb{A}}$ contains no loop $(x,x)$ and no contradicting cycle, i.e., vertices $x_{1},\dots,x_{n}$ such that $EQ(x_{1},x_{i+1})$ for all $i\in[n-1]$ and $N(x_{1},x_{n})$ . Despite the fact that the existence of such a cycle is not a first-order property, the problem $\operatorname{CSP}(\mathbb{N},=,\neq)$ is in $\operatorname{HerFO}$ . For a positive integer $k$ we write $d_{EQ}(x)=k$ for the first-order formula stating “ $x$ has exactly $k$ neighbors in the relation $E Q$ (different from $x$ )”, and $d_{EQ}(x)\neq k$ for its negation. Now, consider the formula

\phi:=\forall x,y\,\exists z\big(\lnot N(x,y)\lor d_{EQ}(x)\neq 1\lor d_{EQ}(y% )\neq 1\lor(d_{EQ}(z)\neq 2\land z\not\in\{x,y\})\big).

If $\mathbb{A}$ does not hereditarily model $\phi$ , then there is a subset $\{a_{1},\dots,a_{n}\}$ such that $N(a_{1},a_{n})$ and every $a_{i}$ has degree exactly $2$ in the relation $E Q$ except for $a_{1}$ and $a_{n}$ , and so $\mathbb{A}$ contains a contradicting cycle. Conversely, if $\mathbb{A}$ has a contradicting cycle one can find a substructure $\mathbb{B}$ of $\mathbb{A}$ that does not model $\phi$ , namely, any shortest contradicting cycle. Therefore, $\operatorname{CSP}(\mathbb{N},=,\neq)$ is hereditarily defined by the first-order sentence $\phi\land\forall x.\lnot N(x,x)$ .

Some further examples of polynomial-time solvable CSPs in HerFO include a finite-domain CSP in HerFO but not in FO (Example 25), and an infinite-domain CSP in HerFO but not even in Datalog (Example 27).

Hard examples

Here, we present an example of a coNP-complete CSP in HerFO that we will also use in Corollaries 24 and 21; to see another (possibly better-known) one see the full version of this paper.

Let $\tau$ consist of two binary symbols $E_{b}$ and $E_{r}$ ; we think of a $\tau$ -structure is a digraph with blue and red edges. For a positive integer $n\geq 2$ we denote by $\mathbb{TD}_{n}$ the structure with vertex set $[n]$ such that $([n],E_{b})$ is a directed cycle $1,\dots,n$ , and $([n],E_{r})$ is a complete (symmetric) graph. Let $\mathcal{T}$ be the set containing the one-element structure with a red loop, and the one-element structure with a blue loop, and all structures $\mathbb{TD}_{n}$ for $n\geq 2$ . Let $\operatorname{Forb}(\mathcal{T})$ be the class of finite $\tau$ -structures $\mathbb{A}$ for which there is no homomorphism $\mathbb{T}\to\mathbb{A}$ for any $\mathbb{T}\in\mathcal{T}$ . Clearly, $\operatorname{Forb}(\mathcal{T})$ is closed under inverse homomorphisms. Since all structures in $\mathcal{T}$ are connected, $\operatorname{Forb}(\mathcal{T})$ is also closed under disjoint unions, and hence $\operatorname{Forb}(\mathcal{T})=\operatorname{CSP}(\mathbb{B}_{\mathcal{T}})$ for some $\tau$ -structure $\mathbb{B}_{\mathcal{T}}$ (see, e.g., [2, Lemma 1.1.8]).³³3The reader familiar with Fraïsse limits [16] may notice that $\mathbb{B}_{\mathcal{T}}$ can be chosen to be a countable homogeneous structure, i.e., such that every isomorphism between finite substructures of $\mathbb{B}_{\mathcal{T}}$ can be extended to an automorphism of $\mathbb{B}_{\mathcal{T}}$ . We show that $\operatorname{CSP}(\mathbb{B}_{\mathcal{T}})$ is a coNP-complete CSP in $\operatorname{HerFO}$ . Consider the $\tau$ -sentence

\phi_{\mathcal{T}}:=\exists x,y\,\forall z\;\big(\lnot E_{b}(z,z)\land\lnot E_% {r}(z,z)\land(\lnot E_{b}(x,z)\lor(x\neq y\land\lnot E_{r}(x,y)))\big).

Clearly, no loop satisfies $\phi_{\mathcal{T}}$ . We now show that no structure $\mathbb{TD}_{n}$ , for $n\geq 2$ , satisfies $\phi_{\mathcal{T}}$ . Consider a pair of vertices $x,y\in\text{TD}_{n}$ . Firstly, there is some $z$ such that $(x,z)\in E_{b}^{\mathbb{TD}_{n}}$ , because the blue edges define a directed cycle in $\mathbb{TD}_{n}$ . Secondly, if $x\neq y$ , then $(x,y)\in E_{r}^{\mathbb{TD}_{n}}$ because the red edges induce a red clique. Hence, $\mathbb{TD}_{n}$ does not satisfy the last conjunct of $\phi_{\mathcal{T}}$ . Also, since $\phi_{\mathcal{T}}$ is negative and connected, it follows by Observation 5 that if $\mathbb{F}\to\mathbb{A}$ for some structure $\mathbb{F}\in\mathcal{T}$ , then $\mathbb{A}$ does not hereditarily satisfy $\phi_{\mathcal{T}}$ . On the other hand, observe that if a $\tau$ -structure $\mathbb{A}$ does not hereditarily satisfy $\phi_{\mathcal{T}}$ , then $\mathbb{A}$ contains a loop, or there is a subset $A^{\prime}\subseteq A$ such that $(A^{\prime},E_{r}^{\mathbb{A}^{\prime}})$ is a complete symmetric graph with at least two vertices, and every vertex $x\in A^{\prime}$ has a blue out-neighbour. So if $\mathbb{A}$ contains no loops, then the shortest directed blue cycle in $A^{\prime}$ induces a structure isomorphic to $\mathbb{TD}_{n}$ for some $n\geq 2$ . Therefore, $\operatorname{Her}(\phi_{\mathcal{T}})=\operatorname{Forb}(\mathcal{T})=% \operatorname{CSP}(\mathbb{B}_{\mathcal{T}})$ .

Theorem 8.

$\operatorname{Forb}(\mathcal{T})$ is a $\operatorname{coNP}$ -complete $\operatorname{CSP}$ hereditarily definable by an $\exists\exists\forall$ - and by an $\exists\forall\exists$ -sentence.

Proof.

It is easy to see that $\phi_{\mathcal{T}}$ is equivalent to the sentence $\phi_{\mathcal{T}}^{\prime}$ obtained from $\phi_{\mathcal{T}}$ by changing the prefix $\exists x,y\forall z$ to $\exists x\forall z\exists y$ . Hence, it follows from the discussion above that $\operatorname{Forb}(\mathcal{T})$ is hereditarily definable by an $\exists\exists\forall$ - and by an $\exists\forall\exists$ -sentence. We now show that $\operatorname{Forb}(\mathcal{T})$ is $\operatorname{coNP}$ -complete. Consider an instance $\psi$ of 3SAT with variables $V$ and clauses $C_{1},\dots,C_{m}$ , where $C_{i}=(c_{i}^{1},c_{i}^{2},c_{i}^{3})$ and $c_{i}^{k}\in\{v,\lnot v\}$ for some $v\in V$ . We construct a $\tau$ -structure $\mathbb{A}$ with vertices $a_{i}^{j}$ for each $i\in[m]$ and $j\in[3]$ . The blue edges of $\mathbb{A}$ consist of all pairs $(a_{i}^{j},a_{i+1}^{k})$ and $(a_{m}^{j},a_{1}^{k})$ , for $i\in[m-1]$ and $j,k\in[3]$ ; the red edges of $\mathbb{A}$ correspond to the relation $c_{i}^{k}\neq\lnot c_{j}^{l}$ with $i\neq j$ , i.e., $(a_{i}^{k},a_{j}^{l})\in E_{r}^{\mathbb{A}}$ if and only if the literal $c_{i}^{k}$ does not equal the negation of the literal $\lnot c_{j}^{l}$ – in particular, $E_{r}^{\mathbb{A}}$ is a symmetric relation without loops.

We claim that $\psi$ is satisfiable if and only if $\mathbb{A}\not\in\operatorname{Forb}(\mathcal{T})$ . Suppose there is a satisfying assignment for $\psi$ , and consider the vertices $a_{i}^{k_{i}}$ where $c_{i}^{k_{i}}$ is true in the clause $C_{i}$ . Then the substructure $\mathbb{A}^{\prime}$ with domain $a_{1}^{k_{1}},\dots,a_{m}^{k_{m}}$ satisfies that every vertex has a blue out-neighbour. Clearly, $c_{i}^{k_{i}}$ cannot be the negation of $c_{j}^{k_{j}}$ , so $(A^{\prime},E_{r}^{\mathbb{A}^{\prime}})$ is a complete red graph. This shows that if $\psi$ is satisfiable, then there is a homomorphism $\mathbb{TD}_{m}\to\mathbb{A}$ .

Conversely, suppose that $\mathbb{A}\notin\operatorname{Forb}(\mathcal{T})$ . Notice that if there is a substructure $\mathbb{A}^{\prime}$ of $\mathbb{A}$ that satisfies that every vertex has a blue out-neighbour, then $A^{\prime}$ contains a vertex $a_{i}^{k_{i}}$ for each $i\in[m]$ . Moreover, if $(A^{\prime},E_{r}^{\mathbb{A}^{\prime}})$ is a complete graph, then $A^{\prime}$ contains at most one vertex $a_{i}^{k_{i}}$ for each $i\in[m]$ . Then the evaluation $f\colon V\to\{0,1\}$ defined by $f(v)=1$ if there is some clause $C_{i}$ such that $v=c_{i}^{k}$ and $a_{i}^{k}\in A^{\prime}$ shows that $\psi$ is satisfiable. $\hfill\blacktriangleleft$

Inexpressible examples

In this section we study the limitations of the expressive power of HerFO. Clearly, a class $\mathcal{C}$ is first-order definable if and only if the complement of $\mathcal{C}$ is first-order definable. A structure $\mathbb{A}$ is a minimal obstruction of a hereditary class $\mathcal{C}$ if $\mathbb{A}\not\in\mathcal{C}$ but every proper substructure $\mathbb{A}^{\prime}$ of $\mathbb{A}$ belongs to $\mathcal{C}$ . We show that $\mathcal{C}\in\operatorname{HerFO}$ if and only if the complement of $\mathcal{C}$ contains a first-order definable subclass $\mathcal{F}^{\prime}$ that contains all minimal obstructions of $\mathcal{C}$ (Lemma 9).

We then apply this observation to show that the class of bipartite graphs is not in HerFO (Example 10). It is well-known that a graph is bipartite if and only if it does not contain an odd cycle, and that the class of odd cycles cannot be expressed by a first-order formula. However, this is not enough to show that the class of bipartite graphs is not in HerFO: there are properties $\mathcal{F}$ that are not first-order definable, but the class of all ${\mathcal{F}}$ -free structures is in $\operatorname{HerFO}$ ; see Example 7. To prove that the class of bipartite graphs is not in HerFO, we therefore need the following lemma which we prove in Appendix C.

Lemma 9.

Let $\mathcal{C}$ be a hereditary class of finite $\tau$ -structures and let $\mathcal{F}$ be the class of minimal obstructions of $\mathcal{C}$ . Then $\mathcal{C}$ is hereditarily first-order definable if and only if there is a first-order sentence $\psi$ such that

$\blacksquare$

if $\mathbb{F}\in\mathcal{F}$ , then $\mathbb{F}\models\psi$ , and
$\blacksquare$

if $\mathbb{A}$ is a finite $\tau$ -structure such that $\mathbb{A}\models\psi$ , then there is an embedding $\mathbb{F}\hookrightarrow\mathbb{A}$ for some $\mathbb{F}\in\mathcal{F}$ .

Building on this simple lemma we can now use standard Ehrenfeucht-Fraïssé arguments to show that certain hereditary classes are not in HerFO. If $\mathbb{A}$ and $\mathbb{A}^{\prime}$ are $\tau$ -structures, we write $\mathbb{A}\equiv_{k}\mathbb{A}^{\prime}$ if $\mathbb{A}$ and $\mathbb{A}^{\prime}$ satisfy the same first-order $\tau$ -sentences with at most $k$ variables.

Example 10 (Bipartite graphs not in $\operatorname{HerFO}$ ).

It is well known that the minimal obstructions of the class of bipartite graphs are all odd symmetric cycles and the non-symmetric edge. For every positive integer $k$ , there is a large enough odd cycle $\mathbb{C}$ and a large enough even cycle $\mathbb{C}^{\prime}$ such that $\mathbb{C}\equiv_{k}\mathbb{C}^{\prime}$ (this can be shown by an Ehrenfeucht-Fraïssé argument; see, e.g., [8]). Hence, we conclude via Lemma 9 that the class of bipartite graphs is not in $\operatorname{HerFO}$ . Moreover, note that $\operatorname{CSP}(K_{2})$ is the class of bipartite digraphs. So it also follows from the existence of such cycles $\mathbb{C}\equiv_{k}\mathbb{C}^{\prime}$ and Lemma 9 that $\operatorname{CSP}(K_{2})$ is not in $\operatorname{HerFO}$ .

In the appendix we use Lemma 9 to show that $\operatorname{CSP}(\mathbb{Q},<,=)$ is not in $\operatorname{HerFO}$ (Example 29). Another method for proving that certain CSPs are not expressible in HerFO is using $\omega$ -categoricity and Remark 6. We present an example in the appendix (Example 26).

4 Hereditary model checking and quantifier prefixes

A quantifier prefix is a word $Q\in\{\exists,\forall\}^{\ast}$ ; we say that a first-order formula $\phi$ in prenex normal form has quantifier prefix $Q$ if $\phi=Q_{1}x_{1}\dots Q_{n}x_{n}.\psi$ where $Q=Q_{1}\dots Q_{n}$ and $\psi$ is a quantifier-free formula. In this section we present the following dichotomy for quantifier prefixes: for every quantifier prefix $Q\in\{\exists,\forall\}^{\ast}$ either

$\blacksquare$

$\operatorname{Her}(\phi)$ is in $\operatorname{P}$ for every first-order formula $\phi$ with quantifier prefix $Q$ , or
$\blacksquare$

there exists a first-order formula $\phi$ with quantifier prefix $Q$ such that $\operatorname{Her}(\phi)$ is coNP-complete.

Moreover, we show that in the former case, $\operatorname{Her}(\phi)$ is expressible by an ESO sentence $\Psi$ whose first-order part is universal.

A relational signature $\tau$ is called monadic if all relation symbols in $\tau$ are monadic. It is easy to see that every problem in HerFO with a monadic signature is in FO, and so polynomial-time solvable. We postpone its simple proof to Appendix C.

Proposition 11.

Let $\tau$ be a finite monadic relational signature. For every first-order formula $\phi$ the class $\operatorname{Her}(\phi)$ is universally definable and hence in $\operatorname{P}$ .

From now on, we only consider the non-monadic case. The key components in the proof of our classification (Theorem 20) are Algorithm 1 (for one of the tractable cases) and the fact that the problem of deciding whether every directed cycle in an input digraph $\mathbb{D}$ induces a symmetric edge is coNP-complete (Theorem 18) and expressible in HerFO (Lemma 17).

The $\mathbf{\forall^{\ast}\exists^{\ast}}$ fragment

In this section we prove that for every $\forall^{\ast}\exists^{\ast}$ -formula $\phi$ there is a universal formula $\phi^{\prime}$ such that a structure $\mathbb{A}$ hereditarily satisfies $\phi$ if and only if $\mathbb{A}\models\phi^{\prime}$ .

Lemma 12.

Let $\phi$ be a $\forall^{\ast}\exists^{\ast}$ -formula with $k$ universally quantified variables. Then a structure $\mathbb{A}$ hereditarily models $\phi$ if and only if every $k$ -element substructure of $\mathbb{A}$ models $\phi$ .

Proof.

We prove the non-trivial (but straightforward) implication. Suppose that every substructure $\mathbb{B}$ of $\mathbb{A}$ with $|B|\leq k$ models $\phi$ , and let $\mathbb{A}^{\prime}$ be a substructure of $\mathbb{A}$ . If $|A^{\prime}|\leq k$ , then $\mathbb{A}^{\prime}\models\phi$ ; otherwise, for a $k$ -tuple $(a_{1},\dots,a_{k})\in(A^{\prime})^{k}$ , let $\overline{b}$ be a tuple such that the quantifier-free part $\psi$ of $\phi$ is true of $(a_{1},\dots,a_{k},\bar{b})$ in the substructure of $\mathbb{A}^{\prime}$ with vertex set $\{a_{1},\dots,a_{k}\}$ . It follows that $\mathbb{A}^{\prime}\models\psi(a_{1},\dots,a_{k},\bar{b})$ , and since such a $\bar{b}$ exists for every $\bar{a}\in(A^{\prime})^{k}$ , we conclude that $\mathbb{A}^{\prime}\models\phi$ , and therefore $\mathbb{A}\in\operatorname{Her}(\phi)$ . $\hfill\blacktriangleleft$

Corollary 13.

If $\phi$ is a $\forall^{\ast}\exists^{\ast}$ -sentence, then $\operatorname{Her}(\phi)$ is universally definable and hence polynomial-time solvable.

Proof.

If $\phi=\forall x_{1},\dots,x_{k}\exists y_{1},\dots,y_{l}.\,\psi$ where $\psi$ is quantifier-free, let $\phi^{\prime}$ be the formula

\forall x_{1},\dots,x_{k}\exists y_{1}\in\{x_{1},\dots,x_{k}\},\dots,y_{l}\in% \{x_{1},\dots,x_{k}\}.\,\psi.

By Lemma 12, a structure hereditarily satisfies $\phi$ if and only if it satisfies $\phi^{\prime}$ . $\hfill\blacktriangleleft$

The $\mathbf{\forall^{\ast}\exists\forall^{\ast}}$ fragment

An SNP $\tau$ -sentence (short for strict non-deterministic polynomial-time) is a sentence of the form

\exists R_{1},\dots,R_{k}\forall x_{1},\dots,x_{n}.\psi

where $\psi$ is a quantifier free $\tau\cup\{R_{1},\dots,R_{k}\}$ -formula [10, 19]. If a structure $\mathbb{A}$ satisfies the sentence $\Psi$ , we write $\mathbb{A}\models\Psi$ . We say that a class of finite $\tau$ -structures $\mathcal{C}$ is in SNP if there exists an SNP $\tau$ -sentence $\Phi$ such that $\mathbb{A}\models\Phi$ if and only if $\mathbb{A}\in{\mathcal{C}}$ . We show that if $\phi$ is a $\forall^{\ast}\exists\forall^{\ast}$ -formula, then $\operatorname{Her}(\phi)$ is in SNP $\cap$ P.

In the following we consider a fixed $\forall^{\ast}\exists\forall^{\ast}$ -formula

\phi=\forall x_{1},\dots,x_{l}\exists y\forall x_{l+1},\dots,x_{n}.\nobreak\ % \psi(x_{1},\dots,x_{l},y,x_{l+1},\dots,x_{n})

where $\psi$ is a quantifier-free $\tau$ -formula. We expand $\tau$ with an $(l+2)$ -ary relation symbol $L$ . We will interpret $L$ as a reflexive linear order with $l$ parameters, i.e., if the first $l$ arguments of $L$ are fixed, then the binary relation defined by the remaining two free variables is a linear order. It is straightforward to observe that there is a universal $\{L\}$ -formula $\operatorname{Lin}(x_{1},\dots,x_{l})$ such that $\operatorname{Lin}$ is true of an $l$ -tuple $\overline{a}$ in an $\{L\}$ -structure $\mathbb{A}$ if and only if the binary relation $L({\overline{a}},x,y)$ defines a reflexive linear order $x\leq_{\overline{a}}y$ on $A$ . Consider now the SNP sentence defined as follows.

	$\displaystyle\Phi:=\exists L\;\forall x_{1},\dots,x_{l},$	$\displaystyle y,x_{l+1},\dots,x_{n}.\nobreak\ \operatorname{Lin}(x_{1},\dots,x% _{l})$
	$\displaystyle\wedge$	$\displaystyle\left(\bigwedge_{i\in[n]}L(x_{1},\dots,x_{l},y,x_{i})\right)% \Rightarrow\psi(x_{1},\dots,x_{l},y,x_{l+1},\dots,x_{n}).$

Lemma 14.

A finite $\tau$ -structure $\mathbb{A}$ hereditarily models $\phi$ if and only if it models $\Phi$ .

Proof.

For the easy direction, suppose that $(\mathbb{A},L)$ models the first-order part of $\Phi$ . For all $a_{1},\dots,a_{l}\in A$ , let $b\in A$ be the minimum with respect to the linear order $\leq_{a_{1},\dots,a_{l}}$ , i.e., the element $b\in A$ such that $L(a_{1},\dots,a_{l},b,c)$ for all $c\in A$ . In particular, for all $a_{l+1},\dots,a_{n}\in A$ and $i\in[n]$ the atomic formula $L(a_{1},\dots,a_{l},b,a_{i})$ holds in $\mathbb{A}$ , and thus $\mathbb{A}\models\psi(a_{1},\dots,a_{l},b,a_{{l}+1},\dots,a_{n})$ . Since the first-order part of $\Phi$ is universal, every substructure $\mathbb{B}$ of $\mathbb{A}$ also models $\Phi$ , and by the previous argument we conclude that $\mathbb{B}$ models $\phi$ . Hence, $\mathbb{A}$ hereditarily models $\phi$ .

Conversely, suppose that $\mathbb{A}$ hereditarily satisfies $\phi$ . For every $l$ -tuple ${\overline{a}}=(a_{1},\dots,a_{l})$ of $A$ we define a reflexive linear order $\leq_{\overline{a}}$ such that the expansion

(\mathbb{A},\{(a_{1},\dots,a_{l},b,c)\colon b\leq_{(a_{1},\dots,a_{l})}c\})

models the first-order part of $\Phi$ . We define elements $b_{1},\dots,b_{m}$ inductively as follows. Let $b_{1}\in A$ be any element witnessing that $\mathbb{A}$ satisfies

\exists y\forall x_{{l}+1},\dots,x_{n}.\psi(\overline{a},y,x_{{l}+1},\dots,x_{% n}).

For $l>1$ , if no $b_{i}$ is a coordinate of $\overline{a}$ for $i<l$ , choose $b_{l}$ to be any element witnessing that the substructure of $\mathbb{A}$ with domain $A\setminus\{b_{1},\dots,b_{l-1}\}$ satisfies $\exists y\forall x_{{l}+1},\dots,x_{n}.\psi(\overline{a},y,x_{{l}+1},\dots,x_{% n})$ (such a vertex $b_{l}$ exists since $\mathbb{A}$ hereditarily satisfies $\phi$ ). Otherwise, if some $b_{i}$ equals some coordinate of ${\overline{a}}$ , then let $b_{l}$ be an arbitrary element of $A\setminus\{b_{1},\dots,b_{l-1}\}$ . We define the linear ordering $b_{i}\leq_{\overline{a}}b_{j}$ if and only if $i\leq j$ , and let $L:=\{(\overline{a},b,c)\in A^{{l}+2}\colon b\leq_{\overline{a}}c\}$ . It follows from the definition of $L$ and of $\operatorname{Lin}$ that $(\mathbb{A},L)\models\forall a_{1},\dots,a_{l}.\operatorname{Lin}(a_{1},\dots,% a_{l})$ .

Suppose that $(\mathbb{A},L)$ satisfies $\bigwedge_{i\in[n]}L(a_{1},\dots,a_{l},b,a_{i})$ for some $a_{1},\dots,a_{l},b,a_{{l}+1},\dots,a_{n}\in A$ . Let $b_{1},\dots,b_{m}$ be the enumeration of $A$ corresponding to the linear ordering $\leq_{(a_{1},\dots,a_{l})}$ , and suppose that $b=b_{l}$ . Since $(\mathbb{A},L)\models\bigwedge_{i\in[n]}L(a_{1},\dots,a_{l},b,a_{i})$ , i.e., $b\leq_{(a_{1},\dots,a_{l})}a_{i}$ for every $i\in[n]$ , it must be the case that every $a_{i}$ belongs to $A\setminus\{b_{1},\dots,b_{l-1}\}$ . It thus follows from the definition of $b_{l}$ that the substructure $\mathbb{B}$ of $\mathbb{A}$ with vertex set $A\setminus\{b_{1},\dots,b_{l-1}\}$ models $\psi(a_{1},\dots,a_{l},b_{l},a_{{l}+1},\dots,a_{n})$ , and thus $(\mathbb{A},L)\models\psi(a_{1},\dots,a_{l},b_{l},a_{{l}+1},\dots,a_{n})$ . This shows that $\mathbb{A}$ satisfies $\Phi$ . $\hfill\blacktriangleleft$

The proof of Lemma 14 suggests a polynomial-time algorithm that on input structure $\mathbb{A}$ finds parameterized linear orderings proving that $\mathbb{A}$ hereditarily satisfies $\phi$ , or finds a substructure $\mathbb{B}$ of $\mathbb{A}$ that does not model $\phi$ (which certifies that $\mathbb{A}$ does not hereditarily satisfy $\phi$ ). See Figure 1 for an illustration.

Certifying polynomial-time algorithm.

Consider a fixed first-order sentence

\phi:=\forall x_{1},\dots,x_{l}\exists y.\phi^{\prime}(x_{1},\dots,x_{l},y)

where $\phi^{\prime}$ is a universal formula.

Algorithm 1 Cert-Her-

\forall^{*}\exists\forall^{*}

.

Lemma 15.

For every first-order formula $\phi:=\forall x_{1},\dots,x_{l}\exists y.\phi^{\prime}(x_{1},\dots,x_{l},y)$ where $\phi^{\prime}$ is a universal formula $\forall x_{l+1},\dots,x_{n}.\psi$ for some quantifier-free formula $\psi$ , and for every $\tau$ -structure $\mathbb{A}$ with domain $A=\{a_{1},\dots,a_{m}\}$ the following statements hold.

$\blacksquare$

If Algorithm 1 returns a substructure $\mathbb{A}^{\prime}$ of $\mathbb{A}$ , then $\mathbb{A}^{\prime}\models\lnot\phi$ , and $\mathbb{A}\not\in\operatorname{Her}(\phi)$ .
$\blacksquare$

If Algorithm 1 returns an expansion $(\mathbb{A},L)$ of $\mathbb{A}$ , then $(\mathbb{A},L)$ satisfies the first-order part of $\Phi$ , and $\mathbb{A}\in\operatorname{Her}(\phi)$ .

Proof.

To prove the first claim, notice that (by finite induction) at the if statement in the repeat-until loop of the algorithm, the set $A^{\prime}$ contains all entries of $\bar{a}$ . Hence, if the algorithm returns $\mathbb{A}^{\prime}$ , then $\mathbb{A}^{\prime}$ does not satisfy $\exists y.\phi^{\prime}(\bar{a},y)$ and hence $\mathbb{A}$ does not hereditarily satisfy $\phi$ . Now we argue that the second itemized statement holds. It is straightforward to observe that $\leq_{\bar{a}}$ is a reflexive linear order for every $\bar{a}\in A^{l}$ . Hence, it follows from the definition of $L$ that $(\mathbb{A},L)\models\forall x_{1},\dots,x_{l}.\operatorname{Lin}(x_{1},\dots,% x_{l})$ . To see that $(\mathbb{A},L)$ models the second conjunct of $\Phi$ , let $\bar{b}\in A^{l}$ , $c\in A$ , and $b_{l+1},\dots,b_{n}\in A$ (so $(\bar{b},c,b_{l+1},\dots,b_{n})$ is an evaluation of the universally quantified variables of $\Phi$ in $A$ ). Further, suppose that

(\mathbb{A},L)\models\bigwedge_{i\in[n]}L(b_{1},\dots,b_{l},c,b_{i});

otherwise the second conjunct in the definition of $\Phi$ is vacuously true for the tuple $(b_{1},\dots,b_{l},c$ , $b_{l+1},\dots,b_{n})$ . By the definition of $L$ , this means that $c\leq_{\bar{b}}b_{i}$ for every $i\in[n]$ . Hence, there is some iteration of the repeat-until loop such that $c\in S$ . Let $S_{i}$ be the set $S$ and the end of this iteration $i$ of the loop, and $S_{0}:=\varnothing$ . It follows from the definition of $\leq_{\bar{b}}$ and the assumption that $c\leq_{\bar{b}}b_{j}$ for each $j\in[n]$ , that if $S_{i}=S_{i-1}\cup\{c\}$ , then $(\{b_{1},\dots,b_{n}\}\cap S_{i-1})=\varnothing$ . Since $c$ was added to $S$ in the $i$ -th iteration, it must be the case that in the $i$ -th iteration the if statement is not true for $s:=c$ , i.e., $\mathbb{A}^{\prime}\models\forall x_{1},\dots,x_{l}.\phi^{\prime}(x_{1},\dots,% x_{l},c)$ . Since $\{b_{1},\dots,b_{n}\}\subseteq A\setminus S_{i-1}$ , we conclude that in particular $\mathbb{A}^{\prime}\models\phi^{\prime}({\bar{b},c})$ where the universally quantified variables from $\phi^{\prime}$ are interpreted as $(b_{l+1},\dots,b_{n})$ . This means that

(\mathbb{A},L)\models\left(\bigwedge_{i\in[n]}L(b_{1},\dots,b_{l},c,b_{i})% \right)\Rightarrow\psi(b_{1},\dots,b_{l},c,b_{l+1},\dots,b_{n}).

Since this is true for any choice of elements $b_{1},\dots,b_{n}$ and $c$ in $A$ , we conclude that $(\mathbb{A},L)$ satisfies the first-order part of $\Phi$ , and by Lemma 14 we conclude that $\mathbb{A}\in\operatorname{Her}(\phi)$ . $\hfill\blacktriangleleft$

Clearly, Algorithm 1 runs in polynomial time in the representation size of $\mathbb{A}$ . Hence, the following statement is an immediate consequence of Lemma 15.

Theorem 16.

If $\phi$ is a $\forall^{\ast}\exists\forall^{\ast}$ -sentence, then there is an $\operatorname{SNP}$ sentence $\Phi$ such that a finite structure $\mathbb{A}$ satisfies $\Phi$ if and only if $\mathbb{A}\in\operatorname{Her}(\phi)$ . Moreover, $\Phi$ can be efficiently computed from $\phi$ , and there is a polynomial-time algorithm that either finds an expansion of $\mathbb{A}$ proving that $\mathbb{A}\models\Phi$ , or finds a substructure $\mathbb{A}^{\prime}$ of $\mathbb{A}$ such that $\mathbb{A}\models\lnot\phi$ .

Note that this theorem covers the first-order sentences that show that Example 1, Example 2, Example 3, and Example 27 are in $\operatorname{HerFO}$ , because they are $\exists\forall^{*}$ sentences. Hence, the polynomial-time tractability of each of these problems follows from Theorem 16.

Figure 1: Consider a first-order

\{E\}

-sentence

\phi

that states that

E

is a symmetric relation, and that for every vertex

x

there is a vertex

y

not adjacent to

x

such that the neighbourhood of

y

induces a clique. Clearly,

\phi

can be chosen to be an

\forall\exists\forall^{\ast}

formula. On the top, we depict a graph

\mathbb{G}

with two distinguished vertices

a

and

b

. At the bottom left, we depict the linear order

\leq_{a}

(from left to right) of

\mathbb{G}

obtained via Algorithm 1 (where the linear order between the vertices greater that

a

can be arbitrary), and that proves that

(\mathbb{G},a)

hereditarily satisfies

\phi(a,y,\bar{z})

. At the bottom right, we depict the partial linear order

<

and the subgraph

\mathbb{H}

(depicted with black vertices) of

\mathbb{G}

that Algorithm 1 finds when running the loop for

x=b

, which proves that

(\mathbb{G},b)

does not hereditarily satisfy

\phi

.

$\exists\forall\exists$ - and $\exists^{2}\forall$ -sentences

Theorem 8 already provides examples of first-order sentences $\phi$ and $\psi$ with quantifier prefix $\exists\forall\exists$ and $\exists^{2}\forall$ such that $\operatorname{Her}(\phi)$ and $\operatorname{Her}(\psi)$ are coNP-complete. Moreover, $\phi$ and $\psi$ are formulas with a binary signature (with two relation symbols). In this section we provide first-order sentences with the same quantifier prefixes over the signature of digraphs (they only use one binary symbol), which is the final ingredient needed to prove Theorem 20.

Consider the class of digraphs $\mathbb{D}$ such that for every directed cycle $d_{1},\dots,d_{n}$ of $\mathbb{D}$ there exist $i,j\in[n]$ such that $d_{i}d_{j}$ is a symmetric edge of $\mathbb{D}$ , i.e., $(d_{i},d_{j}),(d_{j},d_{i})\in\mathbb{D}$ . In this case, we say that every directed cycle of $\mathbb{D}$ ‘induces a symmetric edge’.

Lemma 17.

Every directed cycle of a finite digraph $\mathbb{D}$ induces a symmetric edge if and only if $\mathbb{D}$ hereditarily satisfies the sentence

\displaystyle\exists x,y\forall a\big(\lnot E(x,a)\lor[E(x,y)\land E(y,x)]\big).

(1)

Proof.

Suppose there is a directed cycle $d_{1},\dots,d_{n}$ of $\mathbb{D}$ that does not induce a symmetric edge. Then the substructure of $\mathbb{D}$ with vertex set $\{d_{1},\dots,d_{n}\}$ satisfies the formula

\forall x,y\exists a\big(E(x,a)\land[\lnot E(x,y)\lor\lnot E(y,x)]\big),

and so $\mathbb{D}$ does not hereditarily satisfy (1).

Conversely, suppose that every directed cycle of $\mathbb{D}$ induces a symmetric edge and let $B\subseteq D$ . If $\mathbb{B}$ contains a sink $b$ , then $\mathbb{B}\models\forall a\lnot E(b,a)$ , and so $\mathbb{B}$ satisfies (1). Otherwise, $\mathbb{B}$ contains a directed cycle, and by assumption this directed cycle induces a symmetric edge $u v$ , so by letting $x=u$ and $y=v$ we conclude that $\mathbb{B}$ satisfies $\exists x,y(E(x,y)\land E(y,x))$ . Again, $\mathbb{B}$ satisfies (1). $\hfill\blacktriangleleft$

Now, we prove that deciding whether every directed cycle of an input digraph $\mathbb{D}$ induces a symmetric edge is coNP-complete.

Theorem 18.

The problem of deciding whether every directed cycle in an input digraph $\mathbb{D}$ induces a symmetric edge is $\operatorname{coNP}$ -complete.

Proof.

Let $\mathcal{C}$ be the class of digraphs described in this theorem, i.e., the class of all finite digraphs such that every directed cycle induces a symmetric edge. Fix $\mathbb{X}$ to be a no-instance to this class, e.g., $\mathbb{X}=\vec{\mathbb{C}}_{3}$ . We reduce from the coNP-hard CSP in Theorem 8 (deciding membership in $\operatorname{Forb}(\mathcal{T})$ ) to deciding membership to $\mathcal{C}$ . First, on an input $\mathbb{A}$ to $\operatorname{Forb}(\mathcal{T})$ , we check whether $\mathbb{A}$ contains a blue loop, a red loop, or $\mathbb{T}\mathbb{D}_{2}$ (i.e., a pair of vertices connected by symmetric pairs of blue and red edges). If so, the reduction returns a $\mathbb{X}$ . Otherwise, the reduction returns the following digraph $\mathbb{D}=f(\mathbb{A})$ . The vertex set $D$ of $\mathbb{D}$ equals the domain $A$ of $\mathbb{A}$ , there are no loops $(u,u)\in E(\mathbb{D})$ , and for a pair of distinct vertices $u$ and $v$ we do the following.

$\blacksquare$

If at least one of $(u,v)$ or $(v,u)$ is not a red edge in $\mathbb{A}$ , then we connect $u$ and $v$ by a symmetric pair of edges $(u,v)$ and $(v,u)$ in $E(\mathbb{D})$ .
$\blacksquare$

If $(u,v),(v,u)$ is a symmetric pair of red edges in $\mathbb{A}$ , and $(u,v)$ is a blue edge in $\mathbb{A}$ , then we connect them by a non-symmetric edge $(u,v)$ in $E(\mathbb{D})$ .
$\blacksquare$

If $(u,v),(v,u)$ is a symmetric pair of red edges in $\mathbb{A}$ , and $u$ and $v$ are not connected by blue edges in $\mathbb{A}$ , we do not connect $u$ and $v$ by any edge in $\mathbb{D}$ .

Clearly, the edge relation $E(\mathbb{D})$ admits a quantifier-free definition in $\mathbb{A}$ , and so, if $\mathbb{A}$ is a substructure of $\mathbb{B}$ , then $f(\mathbb{A})$ is a substructure of $f(\mathbb{B})$ . Clearly, for every $\mathbb{T}\mathbb{D}_{n}$ with $n\geq 3$ , the digraph $f(\mathbb{T}\mathbb{D}_{n})$ is a directed cycle that does not induce any symmetric edge. Conversely, if $f(\mathbb{A})$ is a directed cycle on $n$ vertices, then $\mathbb{A}\cong\mathbb{T}\mathbb{D}_{n}$ . It is straightforward to observe that a loopless $\{E_{b},E_{r}\}$ -structure $\mathbb{A}$ with no $\mathbb{T}\mathbb{D}_{2}$ belongs to $\operatorname{Forb}(\mathcal{T})$ if and only if it does not embed any $\mathbb{T}\mathbb{D}_{n}$ for $n\geq 3$ . Hence, we obtained a polynomial-time reduction from deciding $\operatorname{Forb}(\mathcal{T})$ to deciding membership to $\mathcal{C}$ . Therefore, the $\operatorname{coNP}$ -hardness of $\mathcal{C}$ follows from Theorem 8. $\hfill\blacktriangleleft$

Corollary 19.

There are $\exists^{2}\forall$ and $\exists\forall\exists$ (digraph) formulas $\phi$ and $\psi$ such that $\operatorname{Her}(\phi)$ and $\operatorname{Her}(\psi)$ are $\operatorname{coNP}$ -complete.

Proof.

For $\phi$ consider the formula from Lemma 17 and for $\psi$ consider the quantifier reordering $\exists x\forall a\exists y$ of $\phi$ , and notice that $\phi$ and $\psi$ are logically equivalent. $\hfill\blacktriangleleft$

Prefix classification

The classification for general relational signatures follows from the lemmas proved earlier in this section.

Theorem 20.

Let $\tau$ be a relational signature which is not monadic. For every quantifier prefix $Q\in\{\exists,\forall\}^{\ast}$ one of the following statements hold:

$\blacksquare$

$Q$ is of the form $\forall^{\ast}\exists^{\ast}$ , or of the form $\forall^{\ast}\exists\forall^{\ast}$ , and in this case $\operatorname{Her}(\phi)$ is in $\operatorname{P}$ for every first-order $\tau$ -sentence $\phi$ with quantifier prefix $Q$ , or
$\blacksquare$

$Q$ contains a subword $\exists\exists\forall$ or $\exists\forall\exists$ , and in this case there is a first-order $\tau$ -sentence $\phi$ with quantifier prefix $Q$ such that $\operatorname{Her}(\phi)$ is $\operatorname{coNP}$ -complete.

Proof.

Clearly, both items describe disjoint and complementary cases. The claim in the first item follows from Corollary 13 and Theorem 16. If $\tau$ contains a binary relation symbol, then the claim in the second item follows from Corollary 19. Otherwise, $\tau$ must contain a relation $R$ of arity at least three; however, we can use $R$ to model a binary relation, so the claim also holds in this case. $\hfill\blacktriangleleft$

This classification also holds for the intersection of HerFO and CSPs (via Theorem 8).

Corollary 21.

For every quantifier prefix $Q\in\{\exists,\forall\}^{\ast}$ one of the following statements hold:

$\blacksquare$

$Q$ is of the form $\forall^{\ast}\exists^{\ast}$ , or of the form $\forall^{\ast}\exists\forall^{\ast}$ , and in this case if $\operatorname{CSP}(\mathbb{A})=\operatorname{Her}(\phi)$ for some structure $\mathbb{A}$ and some first-order sentence $\phi$ with quantifier prefix $Q$ , then $\operatorname{CSP}(\mathbb{A})$ is in $\operatorname{P}$ , or
$\blacksquare$

$Q$ contains a subword $\exists\exists\forall$ or $\exists\forall\exists$ , and in this case there is a structure $\mathbb{B}$ such that $\operatorname{CSP}(\mathbb{B})=\operatorname{Her}(\phi)$ for some first-order sentence $\phi$ with quantifier prefix $Q$ , and $\operatorname{CSP}(\mathbb{B})$ is $\operatorname{coNP}$ -complete.

5 Undecidability of the tractability problem

The tractability problem for $\operatorname{HerFO}$ asks whether $\operatorname{Her}(\phi)$ can be solved in polynomial time for a given first-order sentence $\phi$ . In this section we show that if $\textnormal{P}\neq\operatorname{NP}$ , then the tractability problem for $\operatorname{HerFO}$ is undecidable. We begin with the following simple observation.

Observation 22.

Consider a first-order $\tau$ -sentence $\phi:=Q_{1}x_{1}\dots Q_{n}x_{n}.\psi(x_{1},\dots,x_{n})$ . If $\xi(x)$ is a first-order $\tau$ -formula, then there is a $\tau$ -sentence $\phi_{\xi}$ such that a $\tau$ -structure $\mathbb{A}$ satisfies $\phi_{\xi}$ if and only if there is no element $a\in A$ that satisfies $\xi$ or the substructure of $\mathbb{A}$ with domain $\{a\in A\colon\mathbb{A}\models\xi(a)\}$ satisfies $\phi$ . Namely, if $Q_{1}=\dots=Q_{n}=\exists$ , then

\phi_{\xi}:=\forall y.\lnot\xi(y)\lor\exists x_{1},\dots,x_{n}(\bigwedge_{i\in% [n]}\xi(x_{i})\land\psi(x_{1},\dots,x_{n})).

Otherwise,

\phi_{\xi}:=Q_{1}x_{1}\dots Q_{n}x_{n}\left(\bigwedge_{i\in U}\xi(x_{i})% \implies\bigwedge_{i\in E}\xi(x_{i})\land\psi(x_{1},\dots,x_{n})\right)

where $U$ (respectively, $E$ ) is the set of indices $i\in\{1,\dots,n\}$ such that $Q_{i}$ is a universal (respectively, existential) quantifier.

Similarly, if $U$ is a monadic predicate and $\phi$ is a first-order sentence, then $\phi_{U}:=\phi_{U(x)}$ denotes the relativization of $\phi$ to the vertices in the set $U$ , and $\phi_{\lnot U}:=\phi_{\neg U(x)}$ the relativization of $\phi$ to the complement of $U$ .

Theorem 23.

If $\textnormal{P}\neq\operatorname{coNP}$ , then it is undecidable to test whether the hereditary model-checking problem for a given first-order sentence $\phi$ is solvable in polynomial time.

Proof.

We use Trakhtenbrot’s theorem, which states that there is no algorithm that decides whether a given first-order formula $\phi$ has a finite model [24]. We reduce this decision problem to our problem.

Let $\phi$ be a first-order $\tau$ -sentence, let $U$ be a monadic predicate not in $\tau$ , and let $E$ a binary predicate also not in $\tau$ . Let $\psi$ be a first-order $\{E\}$ -sentence such that the hereditary model-checking problem for $\psi$ in $\operatorname{coNP}$ -complete, e.g., $\psi$ can be chosen to be the sentence hereditarily describing the CSP from Corollary 19. Building on the relativizations $\psi_{\lnot U}$ and $(\lnot\phi)_{U}$ we define the following first-order $\tau\cup\{U,E\}$ -sentence

\chi:=(\lnot\phi)_{U}\lor\psi_{\lnot U}.

We claim that if $\phi$ does not have a finite model, then $\operatorname{Her}(\chi)$ is polynomial-time solvable, and if $\phi$ has a finite model, then $\operatorname{Her}(\chi)$ is $\operatorname{coNP}$ -complete. We first observe that if $\phi$ does not have a finite model, then $\chi$ is valid on all finite $\tau\cup\{U,E\}$ -structures. To see this, let $\mathbb{A}$ be a $\tau\cup\{U,E\}$ -structure. If $U^{\mathbb{A}}=\varnothing$ , then $\mathbb{A}$ satisfies the first disjunct $(\lnot\phi)_{U}$ of $\chi$ (Observation 22), and if $U^{\mathbb{A}}\neq\varnothing$ , then the substructure induced by $U^{\mathbb{A}}$ also satisfies $(\lnot\phi)_{U}$ , because $\phi$ has no finite models. In particular, this implies that $\operatorname{Her}(\chi)$ can be solved in polynomial-time, because every instance is a yes-instance.

Now suppose that $\phi$ has a finite model. Let $\mathbb{S}$ be a minimal model of $\phi$ , i.e., every proper substructure of $\mathbb{S}$ satisfies $\lnot\phi$ . We present a polynomial-time reduction from $\operatorname{Her}(\psi)$ to $\operatorname{Her}(\chi)$ , which implies that $\operatorname{Her}(\chi)$ is coNP-complete. Given an $\{E\}$ -structure $\mathbb{A}$ we consider the $\tau\cup\{U,E\}$ -structure $\mathbb{B}$ defined as follows:

$\blacksquare$

the domain $B$ of $\mathbb{B}$ is the disjoint union $A\cup S$ ,
$\blacksquare$

the interpretation of $U$ in $\mathbb{B}$ is $S$ ,
$\blacksquare$

the interpretation of $E$ in $\mathbb{B}$ equals $E^{\mathbb{A}}$ , and
$\blacksquare$

for every $R\in\tau$ , the interpretation of $R$ in $\mathbb{B}$ is $R^{\mathbb{S}}$ .

The structure $\mathbb{B}$ can be computed from the structure $\mathbb{A}$ in polynomial time (the structure ${\mathbb{S}}$ is constant). We now show that every substructure of $\mathbb{A}$ satisfies $\psi$ if and only if every substructure of $\mathbb{B}$ satisfies $\chi$ . First, note that if a substructure $\mathbb{C}$ of $\mathbb{B}$ does not contain $\mathbb{S}$ , then $\mathbb{C}$ satisfies $\chi$ . Indeed, if $C\subseteq A$ , then there is no element of $\mathbb{C}$ that models $U(x)$ , so by Observation 22 it follows that $\mathbb{C}\models(\lnot\phi)_{U}$ and hence $\mathbb{C}\models\chi$ . Otherwise, if $\varnothing\neq C\cap S\neq S$ , then the substructure $\mathbb{C}^{\prime}$ of $\mathbb{C}$ with domain $U^{\mathbb{C}}$ satisfies $\lnot\phi$ , because $\mathbb{C}^{\prime}$ is a proper substructure of $\mathbb{S}$ , and $\mathbb{S}$ is the smallest model of $\phi$ . Hence, $\mathbb{C}\models(\lnot\phi)_{U}$ , and so $\mathbb{C}\models\chi$ . These observations imply that every substructure $\mathbb{C}$ of $\mathbb{B}$ satisfies $\chi$ if and only if every substructure $\mathbb{D}$ of $\mathbb{B}$ with $S\subseteq D$ satisfies $\chi$ . If $S=D$ , then $U^{\mathbb{D}}=D$ , so no element $d$ of $\mathbb{D}$ satisfies $\lnot U(d)$ , and similarly as above, we conclude that $\mathbb{D}\models\chi$ because $\mathbb{D}\models\psi_{\lnot U}$ . Finally, we assume that $S\subseteq D$ and $D\neq S$ , and so $D\cap A\neq\varnothing$ . Since $S\subseteq D$ and $\mathbb{S}\models\phi$ , we have that $\mathbb{D}$ does not satisfy $(\lnot\phi)_{U}$ . Hence, $\mathbb{D}\models\chi$ if and only if $\mathbb{D}\models\psi_{\lnot U}$ , and the latter holds if and only if the substructure of $\mathbb{A}$ with domain $D\cap A$ satisfies $\psi$ . We thus conclude that $\mathbb{B}\in\operatorname{Her}(\chi)$ if and only if $\mathbb{A}\in\operatorname{Her}(\psi)$ .

All together this shows that if $\textnormal{P}\neq\operatorname{coNP}$ , then $\phi$ has a finite model if and only if $\operatorname{Her}(\chi)$ is not solvable in polynomial time. $\hfill\blacktriangleleft$

We say that two quantifier prefixes are dual to each other if one can be obtained from the other by exchanging the symbols $\forall$ and $\exists$ .

Corollary 24.

Consider a quantifier prefix $Q\in\{\exists,\forall\}^{\ast}$ , and assume $\textnormal{P}\neq\operatorname{NP}$ . If the finite satisfiability problem for first-order sentences whose quantifier prefix $Q$ is undecidable, then the tractability problem for $\operatorname{HerFO}$ is undecidable for first-order sentences whose quantifier prefix is dual to $Q$ . In particular, we obtain that the tractability problem for $\operatorname{HerFO}$ is undecidable if the quantifier prefix of the input may contain $\exists\forall\exists$ or $\exists^{3}\forall$ as subwords.

Proof.

Denote by $Q^{\prime}$ the dual of $Q$ . It follows from [7, Theorem 3.0.1] that if the finite satisfiability problem for first-order sentences with quantifier prefix $Q$ is undecidable, then $Q$ contains $\forall\exists\forall$ or $\forall^{3}\exists$ as a subword. Dually, $Q^{\prime}$ contains $\exists\forall\exists$ or $\exists^{3}\forall$ as a subword, and so, by Theorem 8, there is a FO sentence $\psi$ with quantifier prefix $Q^{\prime}$ such that $\operatorname{Her}(\psi)$ is $\operatorname{coNP}$ -complete. Now, we can reduce from the finite satisfiability, because the finite satisfiability problem for the fragments of FO with quantifier prefix $Q=\forall\exists\forall$ or $Q=\forall^{3}\exists$ is undecidable [7, Theorem 3.0.1]. $\hfill\blacktriangleleft$

6 Conclusion and Open Problems

We introduced the hereditary first-order model checking problem $\operatorname{HerFO}$ , and presented a complexity classification for $\operatorname{HerFO}$ based on allowed quantifier prefixes. A number of open problems are left for future research.

1.

Are there first-order sentences $\phi$ such that $\operatorname{Her}(\phi)$ is coNP-intermediate (assuming $\textnormal{P}\neq\operatorname{NP}$ )? We conjecture that there are.
2.

Is every finite-domain CSP which is in $\operatorname{HerFO}$ also in P? If $\operatorname{coNP}\neq\operatorname{NP}$ , then it follows from the P vs. NP-complete finite-domain CSP dichotomy that this answer has a positive question. We ask for a proof which does not use any complexity-theoretic assumptions.
3.

Which finite-domain CSPs are in $\operatorname{HerFO}$ ?
4.

Is every CSP in $\operatorname{HerFO}$ also of the form $\operatorname{Her}(\phi)$ for some negative connected sentence $\phi$ ?
5.

Is it true that the tractability problem for $\operatorname{HerFO}$ is undecidable even for first-order sentences with quantifier prefix $\exists\exists\forall$ (assuming $\textnormal{P}\neq\operatorname{NP}$ )? This is the only quantifier-prefix for which the decidability of the tractability problem for $\operatorname{HerFO}$ remains open (see Corollary 24 and the first item of Theorem 20).

References

[1] Max Bannach, Florian Chudigiewitsch, and Till Tantau. On the descriptive complexity of vertex deletion problems. In Rastislav Královic and Antonín Kucera, editors, 49th International Symposium on Mathematical Foundations of Computer Science, MFCS 2024, August 26-30, 2024, Bratislava, Slovakia, volume 306 of LIPIcs, pages 17:1–17:14, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.MFCS.2024.17.
[2] Manuel Bodirsky. Complexity of Infinite-Domain Constraint Satisfaction. Lecture Notes in Logic (52). Cambridge University Press, Cambridge, United Kingdom; New York, NY, 2021. doi:10.1017/9781107337534.
[3] Manuel Bodirsky and Santiago Guzmán-Pro. Hereditary First-Order Logic: the tractable quantifier prefix classes. Preprint arXiv:2411.10860, 2024. doi:10.48550/arXiv.2411.10860.
[4] Manuel Bodirsky and Jan Kára. A fast algorithm and datalog inexpressibility for temporal reasoning. ACM Trans. Comput. Log., 11(3):15:1–15:21, 2010. doi:10.1145/1740582.1740583.
[5] Manuel Bodirsky, Simon Knäuer, and Sebastian Rudolph. Datalog-expressibility for monadic and guarded second-order logic. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 120:1–120:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. Preprint available at https://arxiv.org/abs/2010.05677. doi:10.4230/LIPIcs.ICALP.2021.120.
[6] J. Adrian Bondy and Uppaluri S. R. Murty. Graph Theory. Graduate Texts in Mathematics. Springer, Berlin, 2008. doi:10.1007/978-1-84628-970-5.
[7] Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.
[8] Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, Berlin, Heidelberg, New York, 1995. Second edition.
[9] Thomas Eiter, Georg Gottlob, and Thomas Schwentick. The model checking problem for prefix classes of second-order logic: A survey. In Andreas Blass, Nachum Dershowitz, and Wolfgang Reisig, editors, Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, pages 227–250, Berlin, Heidelberg, 2010. Springer. doi:10.1007/978-3-642-15025-8_13.
[10] Tomás Feder and Moshe Y. Vardi. The computational structure of monotone monadic SNP and constraint satisfaction: A study through datalog and group theory. SIAM J. Comput., 28(1):57–104, 1998. doi:10.1137/S0097539794266766.
[11] Tomás Feder and Moshe Y. Vardi. Homomorphism closed vs. existential positive. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, pages 311–320. IEEE Computer Society, 2003. doi:10.1109/LICS.2003.1210071.
[12] Fedor V. Fomin, Petr A. Golovach, and Dimitrios M. Thilikos. On the parameterized complexity of graph modification to first-order logic properties. Theory Comput. Syst., 64(2):251–271, 2020. doi:10.1007/s00224-019-09938-8.
[13] Toshihiro Fujito. A unified approximation algorithm for node-deletion problems. Discret. Appl. Math., 86(2-3):213–231, 1998. doi:10.1016/S0166-218X(98)00035-3.
[14] Georg Gottlob, Phokion G. Kolaitis, and Thomas Schwentick. Existential second-order logic over graphs: Charting the tractability frontier. J. ACM, 51(2):312–362, 2004. doi:10.1145/972639.972646.
[15] Wilfrid Hodges. Model theory, volume 42 of Encyclopedia of mathematics and its applications. Cambridge University Press, Cambridge, 1993.
[16] Wilfrid Hodges. A shorter model theory. Cambridge University Press, Cambridge, 1997.
[17] Mukkai S. Krishnamoorthy and Narsingh Deo. Node-deletion np-complete problems. SIAM J. Comput., 8(4):619–625, 1979. doi:10.1137/0208049.
[18] John M. Lewis and Mihalis Yannakakis. The node-deletion problem for hereditary properties is np-complete. J. Comput. Syst. Sci., 20(2):219–230, 1980. doi:10.1016/0022-0000(80)90060-4.
[19] Christos H. Papadimitriou and Mihalis Yannakakis. Optimization, approximation, and complexity classes. J. Comput. Syst. Sci., 43(3):425–440, 1991. doi:10.1016/0022-0000(91)90023-X.
[20] Venkatesh Raman, Saket Saurabh, and C. R. Subramanian. Faster fixed parameter tractable algorithms for finding feedback vertex sets. ACM Trans. Algorithms, 2(3):403–415, July 2006. doi:10.1145/1159892.1159898.
[21] Bruce A. Reed, Kaleigh Smith, and Adrian Vetta. Finding odd cycle transversals. Oper. Res. Lett., 32(4):299–301, 2004. doi:10.1016/j.orl.2003.10.009.
[22] Donald J. Rose. A note on consistent ordering and zero circulation. J. ACM, 18(4):573–575, 1971. doi:10.1145/321662.321671.
[23] Donald J. Rose, Robert Endre Tarjan, and George S. Lueker. Algorithmic aspects of vertex elimination on graphs. SIAM J. Comput., 5(2):266–283, 1976. doi:10.1137/0205021.
[24] Boris A. Trakhtenbrot. Understanding basic automata theory in the continuous time setting. Fundam. Informaticae, 62(1):69–121, 2004. (in Russian). URL: http://content.iospress.com/articles/fundamenta-informaticae/fi62-1-04.

Appendix A Examples

Polynomial-time solvable examples

Example 3 shows that $\operatorname{CSP}(\mathbb{Q},<)$ is in $\operatorname{HerFO}$ but not in FO. There are also finite-domain CSPs that are in $\operatorname{HerFO}$ , but not in $\operatorname{FO}$ , as the following examples show. First, recall that the algebraic length of an oriented walk $P$ is the absolute value of the difference between the number of forward edges and the number of backward edges in $P$ . It is well-known (and straightforward to observe) that a digraph $D$ homomorphically maps to the directed path of length $2$ if and only if every oriented walk in $D$ has algebraic length at most $2$ .

Example 25.

The problem $\operatorname{CSP}(\vec{P_{3}})$ is in $\operatorname{HerFO}$ . Consider a first-order formula $\phi$ saying that there is a loop, or there are (directed) edges $(x,y)$ and $(a,b)$ such that the following hold:

$\blacksquare$

$y$ has exactly one out-neighbour different from $b$ , and $x$ is the unique in-neighbour of $y$ ;
$\blacksquare$

$a$ has exactly one in-neighbour different from $x$ , and $b$ is the unique out-neighbour of $a$ ;
$\blacksquare$
every $z\not\in\{x,y,a,b\}$ either
- –
  
  has no in-neighbours and exactly two out-neighbours, and they are different from $b$ , or
- –
  
  has no out-neighbours and exactly two in-neighbours, and they are different from $x$ .

Suppose that a loopless digraph $\mathbb{D}$ satisfies $\phi$ , and let $a,b,x,y\in D$ be witnesses that show that $\phi$ holds in $\mathbb{D}$ . By using the first bullet, we find $z_{1}\in D\setminus\{b\}$ such that $(y,z_{1})\in E(\mathbb{D})$ , and by using the third point iteratively, we find an alternating oriented path $z_{1},z_{2},\dots,z_{k}$ for some $k\geq 3$ , i.e., $(z_{2},z_{1}),(z_{2},z_{3}),(z_{4},z_{3}),\ldots\in E(\mathbb{D})$ , and $z_{k}\in\{a,b,x,y\}$ . We claim that we can find an oriented walk of the form

x\to y\to z_{1}\leftarrow z_{2}\rightarrow\dots\leftarrow z_{k}\text{, where }% z_{k}=b\text{, or of the form}

x\to y\to z_{1}\leftarrow z_{2}\to\dots\rightarrow z_{k}\text{, where }z_{k}% \in\{x,a\}.

We may choose $z_{k}$ so that $z_{k}\in\{a,b,x,y\}$ and $z_{i}\not\in\{a,b,x,y\}$ for $i\in[k-1]$ . We first consider the case where $z_{k}$ is an in-neighbour of $z_{k-1}$ . In this case, we know by the first item that $z_{k}\neq y$ , because $k\geq 3$ and $y$ has exactly one out-neighbour different from $b$ , namely $z_{1}\neq z_{k-1}$ . We also know that $z_{k}\neq a$ because the unique out-neighbour of $a$ is $b\neq z_{k-1}$ (second bullet). Finally, $z_{k}\neq x$ , because $z_{k-1}$ has exactly two in-neighbours, and they are different from $x$ , and so, $z_{k}=b$ . In the case where $z_{k}$ is an out-neighbour of $z_{k-1}$ , then $z_{k}\neq y$ because the unique in-neighbour of $y$ is $x\neq z_{k-1}$ . Similarly as before, we see that $z_{k}\neq b$ by applying the third bullet to $z_{k-1}$ .

Using the existence of such paths we can easily find an oriented path of algebraic length three in $\mathbb{D}$ . Indeed, in the case where the path ends with an edge $z_{k-1}\leftarrow z_{k}$ , and $z_{k}=b$ , we use the unique in-neighbour $a^{\prime}$ of $a$ to construct a path of length three $a^{\prime},a,b,z_{k-1}$ . Now, consider the case when the path ends with an edge $z_{k-1}\to z_{k}$ . If $z_{k}=x$ , then $z_{k-1},x,y,z_{1}$ is a directed walk of length three, and if $z_{k}=a$ , then $x,y,z_{1},\dots,z_{k-1},a,b$ is an oriented walk of algebraic length three. Hence, if $\mathbb{D}\not\in\operatorname{Her}(\lnot\phi)$ , then either $\mathbb{D}$ contains a loop or a walk of algebraic length $3$ , and so $\mathbb{D}\not\to\vec{P_{3}}$ .

Conversely, if $\mathbb{D}\not\to\vec{P_{3}}$ , then either $\mathbb{D}$ contains a loop or it has an oriented path of algebraic length $3$ . In the former case, $\mathbb{D}$ clearly satisfies $\phi$ , and in the latter, by choosing the shortest such path $v_{1},\dots,v_{n}$ we find a substructure of $\mathbb{D}$ that models $\phi$ ; namely, the substructure with vertex set $\{v_{1},\dots,v_{n}\}$ . Therefore, if $\mathbb{D}\not\to\vec{P_{3}}$ , then $\mathbb{D}\not\in\operatorname{Her}(\lnot\phi)$ .

Inexpressible examples and $\omega$ -categoricity

A digraph $\mathbb{D}$ is balanced if every oriented cycle in $\mathbb{D}$ has the same number of forward and of backward edges. Clearly, the class of balanced digraphs is hereditary, and so, it could a priory be expressible in HerFO. Here, we the notion of $\omega$ -categoricity (Remark 6) to prove that the class of balanced digraphs is not expressible in HerFO.

Example 26.

It is folklore that a digraph $\mathbb{D}$ maps homomorphically to some directed path if and only $\mathbb{D}$ is balanced. Equivalently, if $s u c c$ is the successor relation in $\mathbb{Z}$ , then $\mathbb{D}\to(\mathbb{Z},succ)$ if and only if $\mathbb{D}$ is a balanced digraph. Hence, the class of balanced digraphs is in HerFO iff $\operatorname{CSP}(\mathbb{Z},succ)$ is in HerFO. It is known that there is no $\omega$ -categorical structure $\mathbb{A}$ whose CSP equals the CSP of $(\mathbb{Z},succ)$ [2, Proposition 5.8.2]. Therefore, $\operatorname{CSP}(\mathbb{Q},succ)$ (equivalently, the class of balanced digraphs) is not expressible in $\operatorname{HerFO}$ .

HerFO and Datalog

Datalog can be seen as the subclass of SNP where we require that the first-order part $\psi$ of the SNP sentence

$\blacksquare$

is Horn, i.e., written in conjunctive normal form such that each clause contains at most one positive literal, and
$\blacksquare$

is such that every positive literal in $\psi$ is existentially quantified.

A class ${\mathcal{C}}$ of finite models is in Datalog if there exists an SNP sentence $\Phi$ of the form described above such that a finite structure is in ${\mathcal{C}}$ if and only if it does not satisfy $\Phi$ . Note that if a class is in Datalog, then it is closed under homomorphisms⁴⁴4Our definition is standard, but different from the terminology of Feder and Vardi [10, 11], who defined that $\operatorname{CSP}(\mathbb{B})$ is in Datalog if its complement is in Datalog in the standard sense. and in P.

A simple example of a CSP which is solved by a Datalog program is $\operatorname{CSP}(K_{2})$ . In Example 10 we showed that this class is not in $\operatorname{HerFO}$ . There are also CSPs that are in $\operatorname{HerFO}$ and in P, but not in Datalog.

Example 27.

For any positive integer $k$ consider a $(k+1)$ -ary relation symbol $R$ . The problem $\operatorname{CSP}(\mathbb{Q},\{(x,y_{1},\dots,y_{k})\colon x<\max\{y_{1},% \dots,y_{k}\})$ is in P, but not in Datalog [4]. Notice that the problem is in $\operatorname{HerFO}$ : consider the formula

\exists x\forall y_{1},\dots,y_{k}.\lnot R(x,y_{1},\dots,y_{k}).

Corollary 28.

The classes of $\operatorname{CSP}$ s in Datalog and in $\operatorname{P}\cap\operatorname{HerFO}$ are incomparable.

HerFO and pp definitions

A primitive positive formula is an existential positive formula whose quantifier-free part only uses variables and symbols from $\{\land,=\}\cup\tau$ (i.e., disjunction is forbidden). Given a structure $\mathbb{A}$ we say that a relation $R\subseteq A^{r}$ is primitively positively definable (pp-definable) in $\mathbb{A}$ if there is a primitive positive formula $\phi(x_{1},\dots,x_{r})$ such that $\bar{a}\in R$ if and only if $\mathbb{A}\models\phi(\bar{a})$ . A class of structures $\mathcal{C}$ is preserved by primitive positive definitions if for every $\mathbb{A}\in\mathcal{C}$ , and every pp-definable relation $R$ in $\mathbb{A}$ , the structure $(\mathbb{A},R)$ belongs to $\mathcal{C}$ . In Example 3 we showed that $\operatorname{CSP}(\mathbb{Q},<)$ is expressible in $\operatorname{HerFO}$ . The following example shows that $\operatorname{CSP}(\mathbb{Q},<,=)$ is not expressible in $\operatorname{HerFO}$ , and so, the class of structures whose CSP in $\operatorname{HerFO}$ is not preserved by primitive positive definitions.

Example 29.

The problem $\operatorname{CSP}(\mathbb{Q},<,=)$ is not hereditarily definable. Consider the family of structures $\mathbb{C}_{n}$ and $\mathbb{D}_{n}$ illustrated below (where undirected blue edges represent the (symmetric) binary relation $=$ , and directed black edges represent the binary relation $<$ ). It is not hard to see that for every positive integer $n$ ,

$\blacksquare$

$\mathbb{C}_{n}$ is a minimal obstruction of $\operatorname{CSP}(\mathbb{Q},<,=)$ , and
$\blacksquare$

$\mathbb{D}_{n}\in\operatorname{CSP}(\mathbb{Q},<,=)$ .

Now, for every $k\in{\mathbb{N}}$ one can choose $n, m$ appropriately so that $\mathbb{C}_{n}\equiv_{k}\mathbb{D}_{m}$ , and it thus follows by Lemma 9 that this CSP is not expressible in HerFO.

Appendix B Comparison of complexity classifications

As we discussed in the introduction, for every first-order sentence $\phi$ , there is a UMSO sentence $\Phi$ such that $\operatorname{Her}(\phi)$ is described by $\Psi$ , and the first-order part of $\Phi$ has the same quantifier-prefix as $\phi$ . Hence, if every problem expressible by a UMSO sentence with quantifier prefix $Q$ can be solved in polynomial time, then $\operatorname{Her}(\phi)$ can be solved in polynomial time for $\phi$ with quantifier prefix $Q$ .

We also discussed the vertex deletion problem (parametrized version of HerFO): for a fixed first-order sentence $\phi$ , decide whether an input structure $\mathbb{A}$ satisfies $\phi$ after deleting at most $k$ vertices. In Table 1, we present a comparison between our complexity classification based on the quantifier prefix and similar known classifications for UMSO and for the parametrized version. We restrict these classification to digraphs, because, as far as we are aware, complexity classifications for the vertex deletion problem have only been considered for digraphs.

Table 1: Complexity landscape for the model checking problems for UMSO, for HerFO, and for the vertex deletion problem (all restricted to digraphs). In the HerFO column, “Always in P” means that

\operatorname{Her}(\phi)

is polynomial-time solvable whenever

\phi

has quantifier prefix

Q

; in the UMSO column, it means that the model checking problem can be solved in polynomial time for every UMSO sentence

\Phi

whose first-order part has quantifier prefix

Q

. “Hard” in the HerFO and UMSO columns means that the corresponding fragments can express coNP-complete problems. On the last column, FPT means that for every first-order sentence

\phi

with quantifier prefix

Q

, the vertex deletion problem to

\phi

is fixed-parameter tractable; and “hard” means that there are W

[2]

-hard problems in that fragment.

Quantifier prefix	HerFO	UMSO	Vertex deletion
$Q$	(Theorem 20)	[14, Figure 1(a)]	[12, Theorem 1]
$\forall^{\ast}\exists\exists$	Always in P	Always in P	Always FPT
$\forall^{\ast}\exists^{\ast}$	Always in P	Hard	Always FPT
$\forall^{\ast}\exists\forall^{\ast}$	Always in P	Hard	Hard
$\exists\exists\forall$	Hard	Hard	Always FPT
$\exists\forall\exists$	Hard	Hard	Always FPT
$\forall^{\ast}\exists^{\ast}\forall^{\ast}$	Hard	Hard	Hard

Appendix C Two missing proofs

Proof of Lemma 9.

Suppose that $\mathcal{C}=\operatorname{Her}(\phi)$ for some first-order formula $\phi$ . We claim that $\psi:=\neg\phi$ satisfies both itemized statements. Firstly, note that if $\mathbb{F}\in{\mathcal{F}}$ , then $\mathbb{F}\notin\operatorname{Her}(\phi)$ , so some substructure of $\mathbb{F}$ does not satisfy $\phi$ . Moreover, all substructures of $\mathbb{F}$ belong to $\operatorname{Her}(\phi)$ , so we have that $\mathbb{F}$ itself does not satisfy $\phi$ , and hence satisfies $\psi$ . If $\mathbb{A}$ is a finite $\tau$ -structure such that $\mathbb{A}\models\psi$ , then $\mathbb{A}\notin{\mathcal{C}}$ , and hence there exists $\mathbb{F}\in{\mathcal{F}}$ which embeds into $\mathbb{A}$ . This shows the forward implication of the statement. Conversely, if there exists a formula $\psi$ that satisfies both items of the statement, then it is similarly straightforward to show that ${\mathcal{C}}=\operatorname{Her}(\neg\psi)$ . $\hfill\blacktriangleleft$

Proof of Proposition 11.

We claim that $\mathbb{A}$ hereditarily models $\phi$ if and only if every substructure $\mathbb{B}$ of $\mathbb{A}$ with at most $2^{|\tau|}$ many elements satisfies $\phi$ . One direction follows from definition of hereditary satisfiability. For the converse implication, let $\mathbb{B}$ be a substructure of $\mathbb{A}$ and consider a minimal subset $C\subseteq B$ such that for every $b\in B$ there is a $c\in C$ such that $U(b)\Leftrightarrow U(c)$ for all $U\in\tau$ . Clearly, $|C|\leq 2^{|\tau|}$ and it is straightforward to observe that $\mathbb{B}\models\phi$ if and only if $\mathbb{C}\models\phi$ , and the claim follows. $\hfill\blacktriangleleft$

[bib.bib1] [1] Max Bannach, Florian Chudigiewitsch, and Till Tantau. On the descriptive complexity of vertex deletion problems. In Rastislav Královic and Antonín Kucera, editors, 49th International Symposium on Mathematical Foundations of Computer Science, MFCS 2024, August 26-30, 2024, Bratislava, Slovakia, volume 306 of LIPIcs, pages 17:1–17:14, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.MFCS.2024.17.

[bib.bib2] [2] Manuel Bodirsky. Complexity of Infinite-Domain Constraint Satisfaction. Lecture Notes in Logic (52). Cambridge University Press, Cambridge, United Kingdom; New York, NY, 2021. doi:10.1017/9781107337534.

[bib.bib3] [3] Manuel Bodirsky and Santiago Guzmán-Pro. Hereditary First-Order Logic: the tractable quantifier prefix classes. Preprint arXiv:2411.10860, 2024. doi:10.48550/arXiv.2411.10860.

[bib.bib4] [4] Manuel Bodirsky and Jan Kára. A fast algorithm and datalog inexpressibility for temporal reasoning. ACM Trans. Comput. Log., 11(3):15:1–15:21, 2010. doi:10.1145/1740582.1740583.

[bib.bib5] [5] Manuel Bodirsky, Simon Knäuer, and Sebastian Rudolph. Datalog-expressibility for monadic and guarded second-order logic. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 120:1–120:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. Preprint available at https://arxiv.org/abs/2010.05677. doi:10.4230/LIPIcs.ICALP.2021.120.

[bib.bib6] [6] J. Adrian Bondy and Uppaluri S. R. Murty. Graph Theory. Graduate Texts in Mathematics. Springer, Berlin, 2008. doi:10.1007/978-1-84628-970-5.

[bib.bib7] [7] Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.

[bib.bib8] [8] Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, Berlin, Heidelberg, New York, 1995. Second edition.

[bib.bib9] [9] Thomas Eiter, Georg Gottlob, and Thomas Schwentick. The model checking problem for prefix classes of second-order logic: A survey. In Andreas Blass, Nachum Dershowitz, and Wolfgang Reisig, editors, Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, pages 227–250, Berlin, Heidelberg, 2010. Springer. doi:10.1007/978-3-642-15025-8_13.

[bib.bib10] [10] Tomás Feder and Moshe Y. Vardi. The computational structure of monotone monadic SNP and constraint satisfaction: A study through datalog and group theory. SIAM J. Comput., 28(1):57–104, 1998. doi:10.1137/S0097539794266766.

[bib.bib11] [11] Tomás Feder and Moshe Y. Vardi. Homomorphism closed vs. existential positive. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, pages 311–320. IEEE Computer Society, 2003. doi:10.1109/LICS.2003.1210071.

[bib.bib12] [12] Fedor V. Fomin, Petr A. Golovach, and Dimitrios M. Thilikos. On the parameterized complexity of graph modification to first-order logic properties. Theory Comput. Syst., 64(2):251–271, 2020. doi:10.1007/s00224-019-09938-8.

[bib.bib13] [13] Toshihiro Fujito. A unified approximation algorithm for node-deletion problems. Discret. Appl. Math., 86(2-3):213–231, 1998. doi:10.1016/S0166-218X(98)00035-3.

[bib.bib14] [14] Georg Gottlob, Phokion G. Kolaitis, and Thomas Schwentick. Existential second-order logic over graphs: Charting the tractability frontier. J. ACM, 51(2):312–362, 2004. doi:10.1145/972639.972646.

[bib.bib15] [15] Wilfrid Hodges. Model theory, volume 42 of Encyclopedia of mathematics and its applications. Cambridge University Press, Cambridge, 1993.

[bib.bib16] [16] Wilfrid Hodges. A shorter model theory. Cambridge University Press, Cambridge, 1997.

[bib.bib17] [17] Mukkai S. Krishnamoorthy and Narsingh Deo. Node-deletion np-complete problems. SIAM J. Comput., 8(4):619–625, 1979. doi:10.1137/0208049.

[bib.bib18] [18] John M. Lewis and Mihalis Yannakakis. The node-deletion problem for hereditary properties is np-complete. J. Comput. Syst. Sci., 20(2):219–230, 1980. doi:10.1016/0022-0000(80)90060-4.

[bib.bib19] [19] Christos H. Papadimitriou and Mihalis Yannakakis. Optimization, approximation, and complexity classes. J. Comput. Syst. Sci., 43(3):425–440, 1991. doi:10.1016/0022-0000(91)90023-X.

[bib.bib20] [20] Venkatesh Raman, Saket Saurabh, and C. R. Subramanian. Faster fixed parameter tractable algorithms for finding feedback vertex sets. ACM Trans. Algorithms, 2(3):403–415, July 2006. doi:10.1145/1159892.1159898.

[bib.bib21] [21] Bruce A. Reed, Kaleigh Smith, and Adrian Vetta. Finding odd cycle transversals. Oper. Res. Lett., 32(4):299–301, 2004. doi:10.1016/j.orl.2003.10.009.

[bib.bib22] [22] Donald J. Rose. A note on consistent ordering and zero circulation. J. ACM, 18(4):573–575, 1971. doi:10.1145/321662.321671.

[bib.bib23] [23] Donald J. Rose, Robert Endre Tarjan, and George S. Lueker. Algorithmic aspects of vertex elimination on graphs. SIAM J. Comput., 5(2):266–283, 1976. doi:10.1137/0205021.

[bib.bib24] [24] Boris A. Trakhtenbrot. Understanding basic automata theory in the continuous time setting. Fundam. Informaticae, 62(1):69–121, 2004. (in Russian). URL: http://content.iospress.com/articles/fundamenta-informaticae/fi62-1-04.

Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Hereditary first-order logic

Three simple examples

Example 1 (Forests).

Example 2 (Chordal graphs).

Example 3 (Directed acyclic digraphs).

Prefix classifications

Observation 4.

Our contributions

Outline

2 Preliminaries

(First-order) structures

Fragments of first-order logic

3 Hereditary model checking and CSPs

Observation 5.

Proof.

▶ Remark 6.

Example 7.

Hard examples

Theorem 8.

Proof.

Inexpressible examples

Lemma 9.

Example 10 (Bipartite graphs not in HerFO).

4 Hereditary model checking and quantifier prefixes

Proposition 11.

The ∀∗∃∗ fragment

Lemma 12.

Proof.

Corollary 13.

Proof.

The ∀∗∃∀∗ fragment

Lemma 14.

Proof.

Certifying polynomial-time algorithm.

Lemma 15.

Proof.

Theorem 16.

∃∀∃- and ∃𝟐∀-sentences

Lemma 17.

Proof.

Theorem 18.

Proof.

Corollary 19.

Proof.

Prefix classification

Theorem 20.

Proof.

Corollary 21.

5 Undecidability of the tractability problem

Observation 22.

Theorem 23.

Proof.

Corollary 24.

Proof.

6 Conclusion and Open Problems

References

Appendix A Examples

Polynomial-time solvable examples

Example 25.

Inexpressible examples and 𝝎-categoricity

Example 26.

HerFO and Datalog

Example 27.

Corollary 28.

HerFO and pp definitions

Example 29.

Appendix B Comparison of complexity classifications

Hereditary First-Order Logic:
the Tractable Quantifier Prefix Classes

$\blacktriangleright$ Remark 6.

Example 10 (Bipartite graphs not in $\operatorname{HerFO}$ ).

The $\mathbf{\forall^{\ast}\exists^{\ast}}$ fragment

The $\mathbf{\forall^{\ast}\exists\forall^{\ast}}$ fragment

$\exists\forall\exists$ - and $\exists^{2}\forall$ -sentences

Inexpressible examples and $\omega$ -categoricity