2 Preliminaries

We denote by $\mathbb N$ the set of natural numbers greater or equal to 0. For $n\in \mathbb N$ let $[n]:= \{1, 2, \ldots , n\}$ .

2.3 Universal sentences and forbidden induced substructures

An FO-formula is universal if it is built up from atomic and negated atomic formulas by means of the connectives $\wedge $ and $\vee $ and the universal quantifier $\forall $ . Often we say that a formula containing, for example, the connective $\to $ is universal if by replacing $\varphi \to \psi $ by $\neg \varphi \vee \psi $ (and “simple manipulations”) we get an equivalent universal formula. Every universal sentence $\mu $ is equivalent to a sentence $\mu '$ of the form $\forall x_1\ldots \forall x_k\, \mu ^{\prime }_0$ for some $k\ge 1$ and some quantifier-free $\mu ^{\prime }_0$ ; moreover the length $|\mu '|$ of $\mu '$ is at most $|\mu |$ . If in the definition of universal formula we replace the universal quantifier by the existential one, we get the definition of an existential formula.

One easily verifies that the class of models of a set of universal sentence is closed under induced substructures. As already mentioned in the Introduction for classes of graphs, Łoś [Reference Łoś19] and Tarski [Reference Tarski26] proved the following theorem:

Theorem 2.1 (Łoś–Tarski Theorem).

Let $\tau $ be a vocabulary and $\varphi $ an ${\mathrm{FO}}[\tau ]$ -sentence. Then is closed under induced substructures if and only if $\varphi $ is equivalent to a universal sentence.

We first recall the relationship between the axiomatizability of a class of structures by a universal sentence and its definability by a finite set of forbidden finite induced substructures. We fix a vocabulary $\tau $ . Let $\mathscr {F}$ be a set of $\tau $ -structures and denote by and the class of structures (of finite structures) that do not contain an induced substructure isomorphic to a structure in $\mathscr {F}$ . Clearly for sets $\mathscr {F}$ and $\mathscr {F}'$ of $\tau $ -structures we have

(2)

Furthermore, for a class $\mathscr {C}$ of $\tau $ -structures closed under induced substructures one easily verifies that

(3)

We have put the corresponding $\mathscr {F}$ ’s in brackets as they are not sets but classes. However for $\mathscr {C}_{\text {fin}} $ we can repair this by considering only structures whose universe is an initial segment of natural numbers, i.e.,

So we see that for every class of finite structures a denumerable set $ \mathscr {F}$ suffices. When is a finite $ \mathscr {F}$ enough?

We say that a class $\mathscr {C}$ of $\tau $ -structures (of finite $\tau $ -structures) is definable by a finite set of forbidden induced finite substructures if there is a finite set $\mathscr {F}$ of finite structures such that . Recall that $\tau _E= \{E\}$ with binary E. The sentences

axiomatize the classes of directed graphs and of graphs, respectively. Define the $\tau _E$ -structures $H_0=\big (V(H_0), E(H_0)\big )$ and $H_1= \big (V(H_1), E({H_1})\big )$ by

$$ \begin{align*} V(H_0):= \{1\}, \ E(H_0):= \big\{(1, 1)\big\} \ \text{and} \ V(H_1):= \{1, 2\}, \ E(H_1):= \big\{(1, 2)\big\}. \end{align*} $$

Then and are the class of directed graphs and the class of graphs, respectively, i.e., and .

The following result (Proposition 2.2) generalizes this simple fact and establishes the equivalence between axiomatizability by a universal sentence and definability by a finite set of forbidden induced finite substructures. For an arbitrary vocabulary $\tau $ , an ${\text {FO}}[\tau ]$ -sentence $\varphi $ , and $k\ge 1$ let

Thus, $\mathscr {F}_k(\varphi )$ is, up to isomorphism, the class of structures with at most k elements that fail to be a model of $\varphi $ . Note that $\mathscr {F}_1(\varphi _{\text {DG}})= \{H_0\}$ . By (2) and (3) we have

(4)

Proposition 2.2. For a class $\mathscr {C}$ of $\tau $ -structures and $k\ge 1$ the statements (i) and (ii) are equivalent.

1. (i) for some universal sentence $\mu := \forall x_1\ldots \forall x_k\, \mu _0$ with quantifier-free $\mu _0$ .

2. (ii) for some finite set $\mathscr {F}$ of structures, all of at most k elements.

If (i) holds for $\mu $ , then .

The main step of the proof of (ii) $\Rightarrow $ (i) is contained in the following lemma.

Lemma 2.3. Let $\mathcal A$ be a finite $\tau $ -structure and $k:= |A|$ . There is a universal sentence $\mu _{\mathcal A\not \to }= \forall x_1\ldots \forall x_k\, \mu _0$ with quantifier-free $\mu _0$ such that for every $\tau $ -structure $\mathcal B$ ,

$$\begin{align*}\mathcal B\models \mu_{\mathcal A\not\to}\iff \mathcal B\ \text{has no induced substructure isomorphic to}\ \mathcal A, \end{align*}$$

i.e.,

(5)

Proof Let $A= \{a_1,\ldots , a_k\}$ . Let $\delta (x_1,\ldots , x_k)$ be the conjunction of all literals (i.e., atomic or negated atomic formulas) $\lambda (x_1, \ldots , x_k)$ such that $\mathcal A\models \lambda (a_1, \ldots , a_k)$ . Then for every $\tau $ -structure $\mathcal B$ and $b_1, \ldots , b_k\in B$ we have

$$ \begin{align*} \mathcal B\models \delta(b_1, \ldots, b_k) \iff & \text{ the clauses}\ \pi(a_i)= b_i\ \text{for}\ i\in[k]\ \text{define} \\ & \qquad \text{an isomorphism from}\ \mathcal A\ \text{onto}\ [b_1,\ldots, b_k]^{\mathcal B} \end{align*} $$

(recall that $[b_1,\ldots , b_k]^{\mathcal B}$ denotes the substructure of $\mathcal B$ induced on $\{b_1,\ldots , b_k \}$ ). Thus we can set

$$\begin{align*}\mu_{\mathcal A\not\to}:= \forall x_1\ldots \forall x_k\neg\delta(x_1,\ldots, x_k).\\[-32pt] \end{align*}$$

Proof of Proposition 2.2

(ii) $\Rightarrow $ (i): Let for some finite set $\mathscr {F}$ of structures, all of at most k elements. If $\mathscr {F}$ is empty, then . Otherwise, by (ii) and (5),

As the conjunction of finitely many universal sentences of the form $\forall x_1\ldots \forall x_\ell \,\mu _0$ with quantifier-free sentence $\mu _0$ and with $\ell \le k$ is equivalent to such a sentence, we get the desired result.

(i) $\Rightarrow $ (ii): Let for $\mu $ as in (i). Then is closed under induced substructures and hence, by (4). Now assume that $\mathcal A\notin \mathscr {C}$ . Then $\mathcal A\models \neg \mu $ and hence there are $a_1, \ldots , a_k\in A$ with $\mathcal A\models \neg \mu _0(a_1, \ldots , a_k)$ . For $\mathcal B:= [a_1, \ldots , a_k]^{\mathcal A}$ we have $\mathcal B\models \neg \mu _0(a_1,\ldots , a_k)$ (as $\mu _0$ is quantifier-free) and thus, $\mathcal B\models \neg \mu $ . Therefore, $\mathcal B$ is isomorphic to a structure in $\mathscr {F}_k(\mu )$ and therefore, .

Corollary 2.4. Let $\varphi $ be a $\tau $ -sentence and $k\ge 1$ . Then

By (2) and (4) we get the following corollaries:

Corollary 2.5. If for some universal $\mu $ and some $k\ge 1$ , then for all $\ell \ge k$ .

Corollary 2.6. It is decidable whether two universal sentences are equivalent.

Proof Let $\mu $ and $\mu '$ be universal sentences. W.l.o.g. we may assume that $\mu = \forall x_1\ldots \forall x_k\, \mu _0$ and $\mu '= \forall x_1\ldots \forall x_\ell \, \mu ^{\prime }_0$ with $1\le k\le \ell $ and quantifier-free $\mu _0$ and $\mu ^{\prime }_0$ . By Corollaries 2.4 and 2.5, we have

Thus $\mu $ and $\mu '$ are equivalent if and only if $\mathscr {F}_\ell (\mu )= \mathscr {F}_\ell (\mu ')$ . The right-hand side of this equivalence is clearly decidable.

The last equivalence of the preceding proof shows the following:

Corollary 2.7. For universal sentences $\mu $ and $\mu '$ we have

$$\begin{align*}\mu\ \text{and}\ \mu'\ \text{are equivalent} \iff\ \mu\ \text{and}\ \mu'\ \text{are finitely equivalent.} \end{align*}$$

The next result generalizes this corollary.

Lemma 2.8. Let $\Phi $ be a set of universal sentences and $\nu $ a $\Pi _2$ -sentence, i.e., a sentence of the form $\forall x_1\ldots \forall x_k\exists y_1\ldots \exists y_\ell \, \nu _0$ for some $k, \ell \in \mathbb N$ and some quantifier-free $\nu _0$ .

If $\Phi \models _{\text {fin}} \nu $ , then $\Phi \models \nu $ and thus there exists a finite $\Phi _0\subseteq \Phi $ with $\Phi _0\models _{\text {fin}} \nu $ .

Proof If not $\Phi \models \nu $ , then there is a (finite or infinite) structure $\mathcal A$ with $\mathcal A\models \Phi \cup \{\neg \nu \}$ . Note that $\neg \nu $ is equivalent to a sentence of the form

$$\begin{align*}\exists x_1\ldots \exists x_k\,\mu \end{align*}$$

with universal $\mu $ . Choose elements $a_1,\ldots , a_k$ with $\mathcal A \models \mu (a_1,\ldots , a_k)$ . Then $\mathcal B:=[a_1,\ldots , a_k]^{\mathcal A}$ is a model of $\Phi \cup \{\neg \nu \}$ and thus shows $\Phi \not \models _{\text {fin}} \nu $ .

As the class of all at most countable $\tau $ -structures shows, not every class closed under induced substructures is the class of models of a set of universal sentences. In contrast, for classes of finite structures, we have the following:

Lemma 2.9. Let $\mathscr {C}$ be a class of finite $\tau $ -structures closed under induced substructures and define the set of universal sentences $\Phi _{\mathscr {C}}$ by

Then,

Proof The first equality immediately follows from (3) using the closure of $\mathscr {C}$ under induced substructures and the second equality follows from (5).

We use the two preceding results to prove (see [Reference Gurevich17]):

Theorem 2.10 (Compton’s Theorem).

Let $\mathscr {C}$ be a class of finite $\tau $ -structures closed under induced substructures and $\mathrm{FO}$ -axiomatizable by a $\Pi _2$ -sentence $\nu $ . Then $\mathscr {C}$ is already axiomatizable by a universal sentence.

Proof By assumption and the preceding lemma, we have , in particular, $\Phi _{\mathscr {C}}\models _{\text {fin}}\nu $ . By Lemma 2.8 there is a finite subset $\Phi _0$ of $\Phi _{\mathscr {C}}$ such that $\Phi _0\models _{\text {fin}} \nu $ . Thus,

Hence, $\mathscr {C}$ is axiomatizable by the conjunction of the sentences in $\Phi _0$ , a universal sentence.

Recall that our main goal is to find a class of finite graphs with the properties (a)–(c).

1. (a) The class is closed under induced subgraphs.

2. (b) The class is FO-axiomatizable (by a single sentence).

3. (c) The class is not FO-axiomatizable by a universal sentence.

Compton’s Theorem tells us that w.r.t. the quantifier prefix the simplest possible FO-axiomatization of such a class is by a $\Sigma _2$ -sentence, i.e., by a sentence of the form $\exists x_1\ldots \exists x_k\forall y_1\ldots \forall y_\ell \, \rho $ with $k,\ell \in \mathbb N$ and quantifier-free $\rho $ .

The following consequence of Corollary 2.2 will be used in the next section.

Corollary 2.11. Let $m,k\in \mathbb N$ with $m> k$ and let $\psi _0$ and $\psi _1$ be ${\mathrm{FO}}[\tau ]$ -sentences. Assume that $\mathcal A$ is a finite model of $\psi _0\wedge \psi _1$ with at least m elements and all its induced substructures with at most k elements are models of $\psi _0\wedge \neg \psi _1$ . Then $\psi _0\wedge \neg \psi _1$ is not finitely equivalent to a universal sentence of the form $\mu := \forall x_1\ldots \forall x_k\,\mu _0$ with quantifier-free $\mu _0$ .

Proof As there is no universal sentence $\mu $ as above for $k= 0$ , we can assume $k\ge 1$ . For a contradiction assume for $\mu := \forall x_1\ldots \forall x_k\,\mu _0$ with quantifier-free $\mu _0$ . As by Proposition 2.2, we get (applying the finite equivalence of $\psi _0\wedge \neg \psi _1$ and $\mu $ to obtain the last equality)

However, by the assumptions the structure $\mathcal A$ is not contained in but in the class .

Remark 2.12. Let $\mathscr {C}$ be a class of $\tau $ -structures closed under induced substructures. For an ${\text {FO}}[\tau ]$ -sentence $\varphi $ we set . We say that the Łoś-Tarski Theorem holds for $\mathscr {C}$ if for every ${\text {FO}}[\tau ]$ -sentence $\varphi $ such that the class is closed under induced substructures there is a universal sentence $\mu $ such that . The following holds:

Let $\mathscr {C}$ and $\mathscr {C}'$ be classes of $\tau $ -structures closed under induced substructures with $\mathscr {C}'\subseteq \mathscr {C}$ . Furthermore assume that there is a universal sentence $\mu _0$ such that . If the Łoś–Tarski Theorem holds for $\mathscr {C}$ , then it holds for $\mathscr {C}'$ , too.

In fact, for every ${\text {FO}}[\tau ]$ -sentence $\varphi $ we have . Hence, if is closed under induced substructures, then by assumption there is a universal $\mu $ such that . Therefore, .

However, as examples mentioned in the Introduction show, in general the failure of the Łoś–Tarski Theorem on a class does not imply its failure on every subclass.

3 Basic ideas underlying the classical results

This section contains a proof of Tait’s Theorem telling us that the analogue of the Łoś–Tarski-Theorem fails if we only consider finite structures. Afterwards we refine the argument to derive a generalization, namely Proposition 3.11, which is a key result to get Gurevich’s Theorem.

Our counterexample to the Łoś–Tarski-Theorem on finite structures essentially is the one given by Alechina and Gurevich in [Reference Alechina and Gurevich1], which in turn simplifies the one given by Gurevich and Shelah in [Reference Gurevich17]. All these counterexamples use the main idea of the original counterexample due to Tait [Reference Tait25].

We consider the vocabulary $\tau _0:= \{<, U_{\text {min}}, U_{\text {max}}, S\}$ , where $<$ and S (the “successor relation”) are binary relation symbols and $U_{\text {min}}$ and $U_{\text {max}}$ are unary.

Let $\varphi _0$ be the conjunction of the universal sentences:

• – $\forall x \neg x< x$ , $\forall x\forall y (x<y\vee x=y\vee y<x)$ , $\forall x\forall y\forall z ((x<y\wedge y<z)\to x<z)$ , i.e., “ $<$ is an ordering.”

• – $\forall x\forall y\big (U_{\text {min}}\, x\to (x=y\vee x<y)\big )$ , i.e., “every element in $U_{\text {min}}$ is a minimum w.r.t. $<$ .”

• – $\forall x\forall y\big (U_{\text {max}}\, x\to (x=y\vee y<x)\big )$ , i.e., “every element in $U_{\text {max}}$ is a maximum w.r.t. $<$ .”

• – $\forall x\forall y(Sxy\to x<y).$

• – $\forall x\forall y\forall z((x<y\wedge y<z)\to \neg Sxz)$ .

Note that in models of $\varphi _0$ there is at most one element in $U_{\text {min}}$ , at most one in $U_{\text {max}}$ , and that S is a subset of the successor relation w.r.t. $<$ . We call the models of $\varphi _0\ \tau _0$ -orderings.

For a vocabulary $\tau $ with $<\in \tau $ and $\tau $ -structures $\mathcal A$ and $\mathcal B$ we write $\mathcal B\subseteq _< \mathcal A$ and say that $\mathcal B$ is a $<$ -substructure of $\mathcal A$ if $\mathcal B$ is a substructure of $\mathcal A$ with $<^{\mathcal B}= <^{\mathcal A}\cap \, (B\times B)$ .

We remark that the relation symbols $U_{\text {min}}, \ U_{\text {max}}$ , and S are negative in $\varphi _0$ . Therefore we have the following:

Let

(6) $$ \begin{align} \varphi_1:=\exists x\, U_{\text{min}}\, x \wedge \exists x U_{\text{max}}\, x\wedge \forall x\forall y(x<y \to \exists z Sxz). \end{align} $$

We call models of $\varphi _0\wedge \varphi _1$ complete $\tau _0$ -orderings. Clearly, for every $k\ge 1$ there is a unique, up to isomorphism, complete $\tau _0$ -ordering with exactly k elements. The next lemma shows that all its proper $<$ -substructures are models of $\varphi _0\wedge \neg \varphi _1$ .

Proof By the previous lemma we know that $\mathcal B\models \varphi _0$ . Let $B:= \{b_1, \ldots , b_n\}$ . As $<^{\mathcal B}$ is an ordering, we may assume that

$$\begin{align*}b_1<^{\mathcal B} b_2<^{\mathcal B}\dots <^{\mathcal B} b_{n-1}<^{\mathcal B} b_n. \end{align*}$$

As $\mathcal B\models (\varphi _0\wedge \varphi _1)$ , we have $U_{\text {min}}^{\mathcal B} b_1$ , $U_{\text {max}}^{\mathcal B} b_n$ , and $S^{\mathcal B} b_ib_{i+1}$ for $i\in [n-1]$ . As $\mathcal B\subseteq \mathcal A$ , everywhere we can replace the upper index $^{\mathcal B}$ by $^{\mathcal A}$ .

We show $A= B$ (then $\mathcal A= \mathcal B$ follows from $\mathcal A\models \varphi _0$ ): Let $a\in A$ . By $\mathcal A\models \varphi _0$ , we have $b_1\le ^{\mathcal A} a\le ^{\mathcal A} b_n$ . Let $i\in [n]$ be maximal with $b_i \le ^{\mathcal A} a$ . If $i= n$ , then $b_n= a$ . Otherwise, $b_i\le ^{\mathcal A} a<^{\mathcal A} b_{i+1}$ . As $S^{\mathcal A} b_ib_{i+1}$ , we see that $b_i= a$ (by the last conjunct of $\varphi _0$ ).

The Łoś–Tarski Theorem does not remain valid when restricted to finite structures. In fact, the class of finite $\tau _0$ -orderings that are not complete is closed under induced substructures but not axiomatizable by a universal sentence:

By Compton’s Theorem (Theorem 2.10) the sentence $\varphi _0\wedge \neg \varphi _1$ is not even equivalent to a $\Pi _2$ -sentence. However, note that $\varphi _0\wedge \neg \varphi _1$ is (equivalent to) a $\Sigma _2$ -sentence.

We turn to a refinement of Theorem 3.4 that will be helpful to get Gurevich’s Theorem.

For a $\tau $ -structure $\mathcal B$ with $\mathcal B\models \varphi _{0\tau }\wedge \varphi _{1\tau }$ we have

$$\begin{align*}\mathcal B\models\bigwedge_{R \text{ standard}} \Big(\forall \bar x(\neg R\bar x\vee \neg R^{{\text{comp}}}\bar x) \wedge \forall \bar x(R\bar x\vee R^{{\text{comp}}}\bar x)\Big). \end{align*}$$

Hence, for standard $R\in \tau $ of arity r, we have

(7) $$ \begin{align} \text{if}\ \mathcal B\models \varphi_{0\tau}\wedge \varphi_{1\tau}, \text{then}\ (R^{{\text{comp}}})^{\mathcal B}=B^r\setminus R^{\mathcal B}. \end{align} $$

Now we derive the analogues of Lemma 3.1—Theorem 3.4 essentially by the same proofs. In all these results the vocabulary $\tau $ is obtained from $\tau _0$ by adding pairs and $\varphi _{0\tau }$ is an extension of $\varphi _0$ .

By replacing in the proof of Tait’s Theorem the use of Lemma 3.1, Lemma 3.2, and Corollary 3.3 by Lemma 3.7, Lemma 3.8, and Corollary 3.9, respectively, we get the following:

Perhaps the reader will ask why we do not introduce for $<$ the “complement relation symbol” $<^{\text {comp}}$ and add the corresponding conjuncts to $\varphi _{0\tau }$ and $\varphi _{1\tau }$ (or, to $\varphi _0$ and $\varphi _1$ ) in order to get a result of the type of Lemma 3.8 (or already of the type of Lemma 3.2) where we can replace “ $ <$ -substructure” by “substructure.” The reader will realize that corresponding proofs of $B= A$ break down.

The next proposition, the core of the proof of Gurevich’s Theorem, provides a uniform way to construct FO-sentences that are only equivalent to universal sentences of large size.

Proposition 3.11. Again let $\tau $ be obtained from $\tau _0$ by adding pairs and $\varphi _{0\tau }$ be an extension of $\varphi _0$ . Let $m\ge 1$ and $\gamma $ be an ${\mathrm{FO}}[\tau ]$ -sentence such that

(8) $$ \begin{align} \varphi_{0\tau}\wedge \varphi_{1\tau}\wedge \gamma\ \text{has no infinite model but a finite model with at least}\ m\ \text{elements}. \end{align} $$

For $ \chi := \varphi _{0\tau }\wedge (\varphi _{1\tau }\to \neg \gamma ) $ the statements (a) and (b) hold.

1. (a) The class is closed under $<$ -substructures.

2. (b) If $\mu :=\forall x_1\ldots \forall x_k\,\mu _0$ with quantifier-free $\mu _0$ is finitely equivalent to $\chi $ , then $k\ge m$ .

4 The general machinery: strongly existential interpretations

We show that appropriate interpretations preserve the validity of Tait’s theorem and of the statement of Proposition 3.11. Later on these interpretations will allow us to get versions of the results for graphs.

Let $\tau _E:= \{E\}$ with binary E. As already remarked in the Preliminaries for all $\tau _E$ -structures we use the notation $G= (V(G), E(G))$ common in graph theory.

Let $\tau $ be obtained from $\tau _0$ by adding pairs. Furthermore, let $I:=(\varphi _{\text {uni}}, (\varphi _T)_{T\in \tau })$ be an interpretation of width $2$ (we only need this case) of $\tau $ -structures in $\tau _E$ -structures. This means that $\varphi _{\text {uni}}$ and the $\varphi _T $ ’s are ${\text {FO}}[\tau _E]$ -formulas with $\varphi _{\text {uni}} =\varphi _{\text {uni}}(x_1, x_2)$ , $\varphi _T= \varphi _T(x_1, x_2)$ for every unary relation symbol $T\in \tau $ , and ${\varphi _T=\varphi _T(x_1, x_2, y_1, y_2)}$ for every binary relation symbol $T\in \tau $ .

Then for every $\tau _E$ -structure G we set

$$\begin{align*}O_I(G):= \big\{\bar a\in V(G)\times V(G) {\;\big|\;} G\models \varphi_{\text{uni}}(\bar a) \big\}. \end{align*}$$

If $O_I(G)\ne \emptyset $ , i.e., if $G\models \exists \bar x\varphi _{\text {uni}}(\bar x)$ , then the interpretation I assigns to G a $\tau $ -structure with universe $O_I(G)$ , which we denote by $\mathcal O_I(G)$ Footnote ² , given by:

• – $T^{O_I(G)}:= \big \{\bar a\in O_I(G) {\;\big |\;} G \models \varphi _T(\bar a) \big \}$ for unary $T\in \tau .$

• – $T^{O_I(G)}:= \big \{(\bar a,\bar b)\in O_I(G)\times O_I(G) {\;\big |\;} G \models \varphi _T(\bar a, \bar b)\big \}$ for binary $T\in \tau $ .

As the interpretation I is of width $2$ , we have

(9) $$ \begin{align} |O_I(G)|\le |V(G)|^2. \end{align} $$

Recall that for every sentence $\varphi \in {\text {FO}}[\tau ]$ there is a sentence $\varphi ^I \in {\text {FO}}[\tau _E]$ such that for all $\tau _E$ -structures G with $G\models \exists \bar x\varphi _{\text {uni}}(\bar x)$ we have

(10) $$ \begin{align} \mathcal O_I(G)\models \varphi \iff G\models \varphi^I. \end{align} $$

For example, for the sentence $\varphi = \forall x\forall y\, Txy$ we have

$$\begin{align*}\varphi^I= \forall \bar x \Big(\varphi_{{\text{uni}}}(\bar x) \to \forall \bar y \big(\varphi_{{\text{uni}}}(\bar y) \to \varphi_T(\bar x, \bar y)\big)\Big). \end{align*}$$

Furthermore there is a constant $c_I\in \mathbb N$ such that for all $\varphi \in {\text {FO}}[\tau ]$ ,

(11) $$ \begin{align} |\varphi^I|\le c_I\cdot |\varphi|. \end{align} $$

From time to time we will make use of the following lemma.

Lemma 4.1. Let $I:= \big (\varphi _{\text {uni}}, (\varphi _T)_{T\in \tau }\big )$ be an interpretation of $\tau $ -structures in $\tau _E$ -structures. For $\tau $ -sentences $\psi _1$ and $\psi _2$ ,

(12)

and the same implication holds if we restrict to finite structures, i.e.,

(13)

If for every finite $\tau $ -structure $\mathcal A$ there is a finite graph G with $\mathcal O_I(G)\cong \mathcal A$ , then

(14)

Proof The claim holds as all relation symbols distinct from $<$ are negative in $\varphi _{0\tau }$ . For example, for $\varphi := \forall x\forall y \big (U_{\text {min}}\, x\to (x=y\vee x<y)\big )$ , we have

$$\begin{align*}\varphi^I=\forall \bar x \Big(\varphi_{\text{uni}}(\bar x)\to \forall \bar y \big(\varphi_{\text{uni}}(\bar y) \to (\varphi_{U_{\text{min}}}(\bar x)\to ((x_1= y_1\wedge x_2= y_2) \vee \varphi_<(\bar x,\bar y)))\big)\Big). \end{align*}$$

The following result shows that strongly existential interpretations transform induced subgraphs into $<$ -substructures; this will be crucial to transfer the results of the preceding section to graphs.

Proof As $\varphi _{\text {uni}}$ is existential, we have $O_I(H)\subseteq O_I(G)$ . Let $T\in \tau $ be distinct from $<$ and $\bar b\in T^{\mathcal O_I(H)}$ . Then $H\models \varphi _T(\bar b)$ . As $\varphi _T$ is existential, $G\models \varphi _T(\bar b)$ and thus, $\bar b\in T^{\mathcal O_I(G)}$ . Moreover, for $\bar b, \bar b'\in O_I(H)$ we have

$$ \begin{align*} \bar b<^{\mathcal O_I(H)}\bar b' & \iff H\models \varphi_<(\bar b,\bar b') \\ & \iff G\models \varphi_<(\bar b,\bar b') \qquad \text{(as}\ H\subseteq_{\text{ind}} G\ \text{and}\ \varphi_<\ \text{is quantifier-free)} \\ & \iff \bar b<^{\mathcal O_I(G)}\bar b'. \end{align*} $$

Putting all together we see that $\mathcal O_I(H)\subseteq _< \mathcal O_I(G)$ .

We obtain from Lemma 3.8 the corresponding result in our framework.

We now prove for strongly existential interpretations two results, Proposition 4.7 corresponds to Tait’s Theorem (Theorem 3.4) and Proposition 4.8 corresponds to Proposition 3.11 (relevant to Gurevich’s Theorem).

Proposition 4.7. Assume that the interpretation I of $\tau _0$ -structures in $\tau _E$ -structures is strongly existential. Furthermore, assume that for every finite complete $\tau _0$ -ordering $\mathcal A$ , i.e., $\mathcal A\models \varphi _0\wedge \varphi _1$ , there is a finite graph G with $\mathcal O_I(G)\cong \mathcal A$ . Then for

$$\begin{align*}\varphi:= \forall \bar x\neg \varphi_{\text{uni}}(\bar x) \vee \big(\varphi_0\wedge \neg \varphi_1\big)^I \end{align*}$$

the class is closed under induced subgraphs, but $\varphi $ is not equivalent to a universal sentence in finite graphs.

Proposition 4.8. Let $\tau $ be obtained from $\tau _0$ by adding pairs and let $\varphi _{0\tau }$ be an extension of $\varphi _0$ . Assume that I is a strongly existential interpretation of $\tau $ -structures in $\tau _E$ -structures with the property that for every finite $\tau $ -structure $\mathcal A$ that is a model of $\varphi _{0\tau }\wedge \varphi _{1\tau }$ there is a finite graph G with $\mathcal O_I(G)\cong \mathcal A$ and $G\models \psi $ .

Let $m\ge 1$ and $\gamma $ be an ${\mathrm{FO}}[\tau ]$ -sentence such that

(15) $$ \begin{align} \varphi_{0\tau}\wedge \varphi_{1\tau}\wedge \gamma\ \text{has no infinite model but a finite model with at least}\ m\ \text{elements}. \end{align} $$

For

$$ \begin{align*} \rho:= \forall \bar x\neg \varphi_{\text{uni}}(\bar x) \vee \big(\varphi_{0\tau}\wedge (\varphi_{1\tau}\to \neg \gamma)\big)^I, \end{align*} $$

the statements (a) and (b) hold.

1. (a) The class is closed under induced subgraphs.

2. (b) If $\mu := \forall x_1\ldots \forall x_k\,\mu _0$ with quantifier-free $\mu _0$ is equivalent in finite graphs to $\rho $ , then $k^2\ge m$ .

5 Tait’s Theorem for finite graphs

We present strongly existential interpretations that allow us to get Tait’s Theorem for graphs in this section and Gurevich’s Theorem for graphs in Section 6.

We first introduce a further concept. Let G be a graph and $a,b\in V(G)$ . For $r,s\ge 3$ a path from vertex a to vertex b of length r with an s-ear is a path between a and b with a cycle of length s; one vertex of this cycle is adjacent to the vertex adjacent to b on the path; path and cycle have no vertex in common. Figure 1 is a path from a to b of length $6$ with a $4$ -ear.

Figure 1

A path of length 6 with a $4$ -ear.

Proof (a) We can take as $\varphi _{c,r}(x, z_1,\ldots , z_r)$ the formula

$$ \begin{align*} \bigwedge_{1\le i<r} Ez_iz_{i+1} \wedge Ez_rz_1 \wedge \bigwedge_{1\le i<j\le r}\neg z_i= z_j \wedge \bigvee_{i\in[r]} x=z_i. \end{align*} $$

(b) We can take as $\varphi _{pe,r,s}(x, y, z_0,\ldots , z_r, w_1, \ldots , w_s)$ the formula

$$ \begin{align*} x= z_0 \wedge y=z_r\wedge \bigwedge_{0\le i<r-1}Ez_iz_{i+1} \wedge \bigwedge_{0\le i< j\le r}&\neg z_i= z_j \wedge \bigwedge_{0\le i\le r,\ j\in[s]}\neg z_i=w_j \\ & \wedge\bigvee_{i\in [s]} (\varphi_{c,s}(w_i,w_1,\ldots, w_s) \wedge Ez_{r-1}w_i). \end{align*} $$

To understand better how we obtain the desired interpretation we first assign to every complete $\tau _0$ -ordering $\mathcal A$ , i.e., to every model of $\varphi _0\wedge \varphi _1$ , a $\tau _E$ -structure $G:= G(\mathcal A)$ that is a graph.

In a first step we extend $\mathcal A$ to a $\tau ^*_0$ -structure $\mathcal A^*$ , where $\tau ^*_0:= \tau _0\cup \{B,C, L, F\}$ in the following way. Here $B,C$ are unary and $L,F$ are binary relation symbols.

For every original (or, basic) element a, i.e., for every $a\in A$ , we introduce a new element $a'$ , the companion of a. We set

• – $A^*:= A\cup \{a' \mid a\in A\}$ ,

• – $B^{\mathcal A^*}:= A$ , $C^{\mathcal A^*}:= \{a' \mid a\in A\}$ ,

• – $L^{\mathcal A^*}:= \big \{(a,a'){\;\big |\;} a\in A\big \}, \qquad F^{\mathcal A^*}:= \big \{(a',b),(b,a') {\;\big |\;} a,b\in A,\ a<^{\mathcal A} b\big \}$ .

Note that the relation F is irreflexive and symmetric, i.e., $\big (A^*,F^{\mathcal A^*}\big )$ is already a graph, which is illustrated by Figure 2. Observe that F contains the whole information of the ordering $<^{\mathcal A}$ up to isomorphism.

Figure 2

Turning an ordering to the relation F.

We use $\mathcal A^*$ to define the desired graph $G= G(\mathcal A)$ . The vertex set $V(G)$ contains the elements of $A^*$ and the edge relation $E(G)$ contains $F^{\mathcal A^*}$ . Furthermore G contains just all the vertices and edges required by the “gadgets” introduced by the following clauses:

• – To $a\in U_{\text {min}}^{\mathcal A}$ we add a cycle of length $5$ through a, all the other vertices of the cycle are new, i.e., not in $A^*$ .

• – To $a\in U_{\text {max}}^{\mathcal A}$ we add a cycle of length $7$ through a, all the other vertices of the cycle are new.

• – To $a\in B^{\mathcal A^*}$ we add a cycle of length $9$ through a, all the other vertices of the cycle are new.

• – To $a\in C^{\mathcal A^*}$ we add a cycle of length $11$ through a, all the other vertices of the cycle are new.

• – To $(a,b)\in S^{\mathcal A}$ we add a path from a to b of length $17$ with a $13$ -ear consisting of new vertices (besides a and b).

• – To $(a,a')\in L^{\mathcal A^*}$ we add a path from a to $a'$ of length $17$ with a $15$ -ear consisting of new vertices (besides a and $a'$ ).

Hereby we meant by “add a cycle” or “add a path with an ear” that we only add the edges required by the corresponding formulas in Lemma 5.1.

To ease the discussion, we divide cycles in $G\ (= G(\mathcal A))$ into four categories.

[F-cycle] These are the cycles in $\big (A^*,F^{\mathcal A^*}\big )$ , i.e., the cycles using only edges of $F^{\mathcal A^*}$ .

[T-cycle] For every $T\in \big \{U_{{\text {min}}}, U_{{\text {max}}}, B, C\big \}$ and $a\in T^{\mathcal A}$ the cycle introduced for a is a T-cycle.

[ear-cycle] These are the cycles that are the ears on the gadgets introduced for the pairs of the relations $S^{\mathcal A^*}$ and $L^{\mathcal A^*}$ .

[mixed-cycle] All the other cycles are mixed.

For example, we get a mixed cycle if we start with $a_2$ , $a^{\prime }_0$ , $a_1$ in Figure 2 and then add the path introduced for $(a_1, a_2)\in S^{\mathcal A}$ (ignoring the ear).

A number of observations for these types of cycles are in order.

We want to recover $\mathcal A$ (up to isomorphism) from $G(\mathcal A)$ by means of a strongly existential interpretation. Let G be any graph. First we define a $\tau _0$ -structure $\mathcal O(G)$ , possibly the “empty structure” (and then we show that $\mathcal O(G)=\mathcal O_I(G)$ for some strongly existential interpretation I). For the definitions of “cycle” and of “path with ear” see Lemma 5.1.

• – $O(G):= \big \{(a_1,a_2)\in V(G)\times V(G) {\;\big |\;} a_1\ \text {is a member of a cycle of length}\ 9, a_2\ \text {is a member} \text {of a cycle of length}\ 11, \text {and there is a path from}\ a_1\ \text{to}\ a_2\ \text {of}\\ \text{length}\ 17\ \text {with a}\ 15\text {-ear}\big \}$

• – $<^{\mathcal O(G)}:= \big \{((a_1,a_2), (b_1,b_2)) \in O(G)\times O(G) {\;\big |\;} \{a_2,b_1\}\in E(G)\big \}$

• – $U_{\text {min}}^{\mathcal O(G)}:= \big \{(a_1,a_2)\in O(G){\;\big |\;} a_1\ \text {is a member of a cycle of length}\ 5 \big \}$

• – $U_{\text {max}}^{\mathcal O(G)}:= \big \{(a_1,a_2) \in O(G){\;\big |\;} a_1\ \text {is a member of a cycle of length}\ 7\big \}$

• – $S^{\mathcal O(G)}:= \big \{((a_1,a_2),(b_1,b_2))\in O(G)\times O(G) \mid \text {there is a path from}\ a_1\ \text {to}\ b_1 \text {of length}\ 17\ \text {with a}\ 13\text {-ear} \big \}$ .

Proof Let $G:= G(\mathcal A)$ and $\mathcal A^+:= \mathcal O(G)$ . We claim that the mapping $h: A\to A^+$ defined by

$$\begin{align*}h(a):= (a,a') \quad \text{for}\ a\in A \end{align*}$$

is an isomorphism from $\mathcal A$ to $\mathcal A^+$ . To that end, we first prove that

$$\begin{align*}A^+= \big\{(a, a'){\;\big|\;} a\in A\big\}, \end{align*}$$

which implies that h is well defined and a bijection. For every $a\in A$ it is easy to see that $(a, a')\in O(G) \ (= A^+)$ . For the converse, let $(a_1, a_2)\in O(G)$ . In particular, $a_1$ is a member of a cycle of length $9$ . By Lemma 5.2, this must be a B-cycle that contains some $a\in A$ . Using the same argument, $a_2$ is a member of a C-cycle that contains a vertex $b'$ being the companion of some $b\in A$ . Furthermore, there is a path from $a_1$ to $a_2$ of length $17$ with a $15$ -ear. The $15$ -ear is a cycle of length $15$ . Again by Lemma 5.2 this cycle is an ear-cycle that belongs to the gadget we introduced for some $(c,c')\in L^{\mathcal A^*}$ with $c\in A$ . Then it is easy to see that $a= c= b$ . This finishes the proof that h is a bijection from A to $A^+$ .

Similarly, we can prove that h preserves all the relations.

We show that we can obtain $\mathcal O(G)$ from G by a strongly existential FO-interpretation I of width 2. We set

$$\begin{align*}\varphi_{\text{uni}}(x,x'):= \exists \bar x\exists \bar x'\exists \bar z\exists \bar w \, \eta(x,x',\bar x,\bar x',\bar z, \bar w). \end{align*}$$

Here $\eta (x,x',\bar x,\bar x',\bar z, \bar w)$ is the formula

$$\begin{align*}\varphi_{c,9}(x,\bar x)\wedge\varphi_{c,11}(x',\bar x') \wedge \varphi_{pe,17,15}(x,x'\bar z, \bar w) \end{align*}$$

that expresses “ $\bar x$ is a cycle of length $9$ containing x, $\bar x'$ is a cycle of length $11$ containing $x'$ , and $\bar z$ is a path from x to $x'$ of length $17$ with the $15$ -ear $\bar w$ .” Furthermore we define:

• – $\varphi _<(x,x',y,y'):= Ex'y$ ,

• – $\varphi _{U_{\text {min}}}(x,x'):= \exists \bar z\, \varphi _{c,5}(x,\bar z)$ ,

• – $\varphi _{U_{\text {max}}}(x,x'):= \exists \bar z\, \varphi _{c,7}(x,\bar z)$ ,

• – $\varphi _S(x,x',y,y'):= \exists \bar z \exists \bar w \varphi _{pe,17,13}(x,y,\bar z,\bar w)$ .

Then we have the following:

Lemma 5.4. $I:= (\varphi _{\text {uni}}, \varphi _<, \varphi _{U_{\text {min}}}, \varphi _{U_{\text {max}}}, \varphi _S)$ is a strongly existential interpretation of $\tau _0$ -structures in $\tau _E$ -structures. For every complete $\tau _0$ -ordering $\mathcal A$ we have $\mathcal O_I(G(\mathcal A))= \mathcal O(G(\mathcal A))$ and hence, by Lemma 5.3,

$$\begin{align*}\mathcal O_I(G(\mathcal A))\cong \mathcal A. \end{align*}$$

We get from Proposition 4.7:

In this section we presented a strongly existential interpretation of $\tau _0$ -structures in $\tau _E$ -structures (more precisely, in graphs) and applied it to finite complete $\tau _0$ -orderings, i.e., to models of $\varphi _0\wedge \varphi _1$ . A straightforward generalization of the preceding proofs allows us to show the following result for vocabularies obtained from $\tau _0$ by adding pairs. We shall use it in Section 6.

Remark 5.7. (a) Let be the class of finite directed graphs. Then , the class of finite graphs, is a subclass of $\mathscr {C}$ closed under induced substructures and definable in $\mathscr {C}$ by the universal sentence $\forall x \forall y(Exy\to Eyx)$ . As the Łoś–Tarski Theorem fails for the class of finite graphs, it fails for the class of directed graphs by Remark 2.12.

(b) Let be the class of finite planar graphs, a subclass of closed under induced subgraphs. As mentioned in the Introduction, in [Reference Atserias, Dawar and Grohe2] it is shown that the Łoś–Tarski Theorem fails for . As is not axiomatizable in by a universal sentence, not even by a first-order sentence, we do not get the failure of the Łoś–Tarski Theorem for the class of finite graphs (i.e., Theorem 5.5) by applying the result of Remark 2.12. We show that for a finite set $\mathscr {F}$ of finite graphs (or, equivalently, for a universal $\mu $ ) leads to a contradiction. Let k be the maximum size of the set of vertices of graphs in $\mathscr {F}$ . Let G be the graph obtained from the clique $K_5$ of five vertices by subdividing each edge $k+1$ times. Clearly, . However, every subgraph of G induced on at most k vertices is planar. Hence, .

(c) Let $\tau $ be any vocabulary with at least one at least binary relation T. Then the Łoś–Tarski Theorem fails for the class , the class of all finite $\tau $ -structures. By Remark 2.12 it suffices to show the existence of a universally definable subclass $\mathscr {C}'$ of $\mathscr {C}$ which “essentially is the class of graphs.” We set

$$\begin{align*}\mu:=\forall x\forall \bar u\neg Txx\bar u \wedge\forall x\forall y \forall\bar u\forall\bar v (Txy\bar u\to Tyx\bar v) \wedge\bigwedge_{R\in\tau,\ R\ne T}\forall \bar u \neg R\bar u \end{align*}$$

and let $\mathscr {C}'$ be .

If $\tau $ only contains unary relation symbols, the Łoś–Tarski Theorem holds for . It is easy to see for an ${\text {FO}}(\tau )$ -sentence $\varphi $ that the closure under induced substructures of implies that of .

6 Gurevich’s Theorem

The following discussion will eventually lead to a proof of Gurevich’s Theorem, i.e., Theorem 1.5. Our proof essentially follows Gurevich’s proof in [Reference Gurevich17], but it contains some elements of Rossman’s proof of the same result in [Reference Rossman22].Footnote ³ Afterwards we show that it remains true if we restrict ourselves to graphs.

Our main tool is Proposition 3.11: the goal is to construct a formula $\gamma $ satisfying (8) and whose size is much smaller than the number m. Basically $\gamma $ will describe a very long computation of a Turing machine on a short input. We fix a universal Turing machine M operating on a one-way infinite tape, the tape alphabet is $\{0, 1\}$ , where $0$ is also considered as blank and Q is the set of states of M. The initial state is $q_0$ and $q_h$ is the halting state; thus $q_0, q_h\in Q$ and we assume that $q_0\ne q_h$ . An instruction of M has the form

$$\begin{align*}qapbd, \end{align*}$$

where $q, p\in Q$ , $a,b\in \{0, 1\}$ and $d\in \{-1, 0, 1\}$ . It indicates that if M is in state q and the head of M reads an a, then M changes to state p, the head replaces a by b and moves to the left (if $d= -1$ ), stays still (if $d= 0$ ), or moves to the right (if $d= 1$ ). In order to describe computations of M by FO-formulas we introduce binary predicates $H_q(x,t)$ for $q\in Q$ to indicate that at time t the machine M is in state q and the head scans cell x, and a binary predicate $C_0(x,t)$ to indicate that the content of cell x at time t is 0.

The vocabulary $\tau _M$ is obtained from $\tau _0$ by adding pairs (see Definition 3.6(a)),

$$\begin{align*}\tau_M:= \tau_0\cup \big\{H_q, H_q^{\text{comp}} {\;\big|\;} q\in Q\big\} \cup \big\{C_0, C_0^{\text{comp}}\big\}. \end{align*}$$

Intuitively, $H_q^{\text {comp}}(x,t)$ says that “at time t the machine is not in state q or the head does not scan cell x;” and $C_0^{\text {comp}}(x,t)$ says that “at time t the content of cell x is (not 0 and thus is) 1.” Sometimes we write $C_1$ instead of $C_0^{\text {comp}}$ (e.g., below in $\varphi _2$ if $a= 1$ or $b= 0$ ).

Let $\varphi _0$ and $\varphi _1$ be the sentences already introduced in Section 3. For $w\in \{0, 1\}^*$ the sentence $\varphi _{0w}$ will be an extension of $\varphi _0$ (compare Definition 3.6(b)). Hence, $\varphi _{0w}$ will be a universal sentence and all relations symbols besides $<$ are negative in $\varphi _{0w}$ ; in particular, it contains as conjuncts $\varphi _0$ and

$$\begin{align*}\forall x\forall t \big(\neg C_0(x,t) \vee \neg C^{\text{comp}}_0(x,t)\big) \wedge \bigwedge_{q\in Q} \forall x\forall t \big(\neg H_q(x,t)\vee \neg H_q^{\text{comp}}(x,t)\big). \end{align*}$$

Finally, $\varphi _{0w}$ will contain the following sentences $\varphi _2$ and $\varphi _w$ as conjuncts. The sentence $\varphi _2$ describes one computation step. It contains for each instruction of M one conjunct. For example, the instruction $qapb1$ contributes the conjunct

$$ \begin{align*} \forall x \forall x'\forall t \forall t' \forall y \Big(\big(H_{q}&(x,t) \wedge C_a (x,t) \wedge S(x,x')\wedge S(t,t')\big) \\ \to \Big( &(\neg C_{1-b}(x,t') \wedge \neg H^{\text{comp}} _{p}(x',t')) \\ & \wedge (y\ne x'\to \bigwedge_{r\in Q}\neg H_r(y,t')) \\ & \wedge (y\ne x\to((C_0(y,t)\to \neg C^{\text{comp}}_0(y,t')) \wedge (C^{\text{comp}}_0(y,t)\to\neg C_0(y,t'))))\Big)\Big). \end{align*} $$

For $w\in \{0, 1\}^*$ the sentence $\varphi _w$ describes the initial configuration of M with input w (if $w= w_1\ldots w_{|w|}$ , the first $|w|$ cells (if present) contain $w_1, \ldots , w_{|w|}$ , the remaining cells contain $0$ , and the head scans the first cell in the starting state $q_0$ ). Taking into account that models of $\varphi _0\wedge \varphi _1$ might contain less than $|w|$ elements, as $\varphi _w$ we can take the conjunction of

• – $\forall x_1\ldots \forall x_{|w|}\big ((U_{\text {min}}\, x_1\to \neg C_{1-w_1}(x_1,x_1)) \\[2mm] {\hspace {2.3cm}}\wedge \bigwedge _{i\in [|w|-1]}(S{x_i}x_{i+1} \to \neg C_{1-w_{i+1}}(x_{i+1},x_1)) \big )$

• – $\forall x_1\ldots \forall x_{|w|}\forall x\big ((U_{\text {min}}\, x_1\wedge \bigwedge _{i\in [|w|-1]}S{x_i}x_{i+1}\wedge x_{|w|}<x)\to \neg C^{\text {comp}}_{0}(x,x_1)\big )$

• – $\forall x\forall y\big (U_{\text {min}}\, x\to (\neg H_{q_0}^{\text {comp}}(x,x)\wedge (y\ne x\to \bigwedge _{q\in Q}\neg H_q(y,x)))\big )$ .

Note that besides $<$ all relation symbols of $\tau _M$ are negative in $\varphi _{0w}$ . We set $\varphi _{1M}:=\varphi _{1\tau _M}$ ; recall that by Definition 3.6(c),

(16) $$ \begin{align} \varphi_{1M}= \varphi_1\wedge\forall x\forall t \big(C_0(x,t)\vee C^{\text{comp}}_0(x,t)\big) \wedge \bigwedge_{q\in Q}\forall x\forall t \big(H_q(x,t)\vee H_q^{\text{comp}}(x,t)\big). \end{align} $$

Let $w\in \{0,1\}^*$ and $r\in \mathbb N$ . Furthermore, let $\mathcal A$ be a $\tau _M$ -structure where $<^{\mathcal A}$ is an ordering and $|A|\ge r+1$ . Let $a_0, \ldots , a_r$ be the first $r+1$ elements of $<^{\mathcal A}$ . Assume that M on the input $w\in \{0, 1\}^*$ runs at least r steps. We say that $\mathcal A$ correctly encodes r steps of the computation of M on w if for $i,j$ with $0\le i,j\le r$ ,

(17) $$ \begin{align} (a_i,a_j)\in C_0^{\mathcal A} \iff \text{the content of cell}\ i\ \text{after}\ j\ \text{steps is 0} \end{align} $$

and for $q\in Q$ ,

(18) $$ \begin{align} (a_i,a_j)\in H_q^{\mathcal A} \iff \text{after}\ j\ \text{steps}\ M\ \text{is in state}\ q\ \text{and the head scans cell}\ i. \end{align} $$

Proof (a) holds by the definitions of $\varphi _{0w}$ and $\varphi _{1M}$ . For (b) let $A=\{a_0, \ldots , a_r\}$ with pairwise distinct $a_i$ ’s. Assume first that M on w runs at least r steps. We can interpret (17) and (18) as defining relations $C_0^{\mathcal A}$ and $H_q^{\mathcal A}$ on A equipped with the “natural” ordering and its corresponding relations $U_{{\text {min}}}$ , $U_{{\text {max}}}$ , and S. If furthermore we let $(C^{\text {comp}}_0)^{\mathcal A}$ and $(H_q^{\text {comp}})^{\mathcal A}$ be the complements in $A\times A$ of $C_0^{\mathcal A}$ and $H_q^{\mathcal A}$ , respectively, we get a model of $\varphi _{0w}\wedge \varphi _{1M}$ with $r+1$ elements. By (a), this model is unique up to isomorphism.

If M on input w halts, say in $h(w)$ steps, with $h(w)< r$ , we get a model $\mathcal A$ of $\varphi _{0w}\wedge \varphi _{1M}$ with $A= \{0, 1, \ldots , r\}$ , for example “by repeating the configuration reached after $h(w)$ steps”. This means, if T is any of the relations $C_0,H_q,C_0^{\text {comp}}, H_q^{\text {comp}}$ , we set for j with $h(w)<j\le r$ and $i=0,\ldots , r$ ,

$$\begin{align*}(i,j)\in T^{\mathcal A}\iff (i,h(w))\in T^{\mathcal A}.\\[-35pt] \end{align*}$$

Let $\gamma _M$ be a sentence expressing that “M reaches the halting state $q_h$ in exactly ‘ ${\text {max}}$ ’ steps,” e.g., we let $\gamma _M$ be

(19) $$ \begin{align} \exists t\exists x \big(U_{\text{max}} t \wedge H_{q_h}(x,t)\wedge \forall t'\forall y (t'< t\to \neg H_{q_h}(y,t'))\big). \end{align} $$

As a consequence of the preceding lemma, we obtain the following:

Corollary 6.2. Let $w\in \{0,1\}^*$ and set

$$ \begin{align*} \pi_w:=\varphi_{0w}\wedge \varphi_{1M}\wedge \gamma_M. \end{align*} $$

1. (a) If M on w does not halt, then $\pi _w$ has no finite model.

2. (b) Assume M on w eventually halts, say in $h(w)$ steps. Then $\pi _w$ has a unique model up to isomorphism. This model is finite and has exactly $h(w)+1$ elements.

We set

(20) $$ \begin{align} \chi_w:=\varphi_{0w}\wedge (\varphi_{1M}\to\neg \gamma_M). \end{align} $$

Applying Proposition 3.11 to part (b) of the preceding corollary, we get the following:

Now we show the following version of Gurevich’s Theorem.

Note that by Corollary 2.7 the conclusion of this theorem is only apparently stronger than “ $\chi _w$ is not equivalent to a universal sentence of length less than $f(|\chi _w|)$ .” A similar remark applies to Theorem 6.6.

Proof of Theorem 6.4

By the previous lemma it suffices to find a $w\in \{0,1\}^*$ such that M on input w halts in $h(w)$ steps with

$$\begin{align*}h(w)\ge f( |\chi_w|). \end{align*}$$

W.l.o.g. we assume that f is increasing. An analysis of the formula $\chi _{w}$ shows that for some $c_M\in \mathbb N$ we have for all $w\in \{0,1\}^*$ ,

(21) $$ \begin{align} |\chi_w|\le c_M\cdot |w|. \end{align} $$

We define $g:\mathbb N\to \mathbb N$ by

$$ \begin{align*} g(k):= f(5\cdot c_M\cdot k). \end{align*} $$

Let $M_0$ be a Turing machine computing g, more precisely, the function $1^k\mapsto 1^{g(k)}$ . We code $M_0$ and $1^k$ by a $\{0, 1\}$ -string $\textit {code}(M_0,1^k)$ such that M on $\textit {code}(M_0,1^k)$ simulates the computation of $M_0$ on $1^k$ .

Choose the least k such that for $w:= \textit {code}(M_0,1^k)$ we have

(22) $$ \begin{align} |w|\le 5k. \end{align} $$

The universal Turing machine M on input w computes $1^{g(k)}$ and thus runs at least $g(k)$ steps, say, exactly $h(w)$ steps. By (21) and (22)

$$\begin{align*}h(w)\ge g(k)= f(5\cdot c_M\cdot k)\ge f(c_M\cdot |w|)\ge f(|\chi_w|).\\[-34pt] \end{align*}$$

Finally we prove Gurevich’s Theorem for graphs. For $\tau := \tau _M$ let I be an interpretation according to Lemma 5.6. For $w\in \{0, 1\}^*$ we consider the sentence

(23) $$ \begin{align} \rho_w:= \forall \bar x\neg \varphi_{\text{uni}}(\bar x) \vee (\varphi_{0w}\wedge (\varphi_{1M}\to \neg \gamma_M))^I = \forall \bar x\neg \varphi_{\text{uni}}(\bar x)\vee {\chi_w}^I. \end{align} $$

That is, for $G\models \rho _w$ , either the graph G interprets an “empty $\tau _M$ -structure,” or a $\tau _M$ -structure that is a model of $\chi _w$ . If M halts in $h(w)$ steps on input w, then $\varphi _{0w}\wedge \varphi _{1M}\wedge \gamma _M$ has no infinite model but a finite model with $h(w)+1$ elements by Corollary 6.2(b). Hence, by Proposition 4.8 we get the following analogue of Lemma 6.3.