Past exam of the mathematics course of the University of Cambridge / 2002 / iii / Paper 23 (Infinite and Finite Model Theory)

The compactness theorem for first-order logic says that a set $\Sigma$ of first-order sentences has a model if and only if every finite subset of $\Sigma$ has a model. It applies to arbitrary languages, including expansions by arbitrarily many new constants. Equivalently, if $\Sigma$ entails a sentence, some finite subset already entails it. We will use both formulations with the diagram of a structure.

Name every element $a\in A$ by a new constant $c_a$, distinct from the symbols already in $L^{\prime }$. Let $\mathrm{Diag}(A)$ be its full atomic and negated atomic diagram of a structure. A model of this diagram contains an isomorphic copy of $A$ as an $L$-substructure. We claimis satisfiable.

Otherwise compactness theorem gives a finite diagram conjunction $\delta (c_{a_1},\dots ,c_{a_m})$ inconsistent with $T^{\prime }$. Replace these new constants by variables. Since $T^{\prime }$ says nothing about the new names, it then entails the universal sentenceThe conjunction $\delta$ uses only symbols of $L$, so this is one of the universal $L$-consequences assumed true in $A$. But $A$ satisfies $\delta (a_1,\dots ,a_m)$, a contradiction. A model of the consistent enlarged theory gives an embedding of $A$ into the $L$-reduct of a model of $T^{\prime }$. Negated atomic facts and disequalities in the diagram ensure that this is a structure embedding, not merely a homomorphism.

Let $U$ be all universal sentences true in $C$. The theory $T\cup U$ is consistent. Indeed, if a finite conjunction $u$ of sentences from $U$ were inconsistent with $T$, then $T\models \neg u$. A finite conjunction of universal sentences is universal, so its negation is equivalent to an existential sentence. By the hypothesis $C$ would satisfy $\neg u$, whereas it satisfies $u$.

Choose $A\models T\cup U$. Now expand the language by names for every element of $C$ and consider its elementary diagram $\mathrm{ElDiag}(C)$. Its universal consequences in the original language are exactly $U$: any such consequence is true in the named copy of $C$, while any original-language sentence true in $C$ already belongs to its elementary diagram. Part (b), applied to $A$ and this expanded theory, gives a structure embedding of $A$ into a model $D$ of $\mathrm{ElDiag}(C)$. The named copy of $C$ is an elementary substructure of $D$. Identifying that copy with $C$, we obtainThus the required target is an elementary extension of $C$, although $C$ itself need not be a model of $T$.

Let $S$ be the set of all existential sentences entailed by $T$. Certainly every model of $T$ satisfies $S$. Conversely, take $C\models S$. Part (c) gives $A\models T$ embedded in an elementary extension $D$ of $C$. After identifying $A$ with its image, $D$ is a superstructure of a model of $T$. The assumed closure under superstructures implies $D\models T$. Since $C\preccurlyeq D$, it follows that $C\models T$ as well. HenceThis supplies an existential axiomatization. Conversely, an existential sentence is preserved under embeddings because its finite tuple of witnesses and the quantifier-free facts about them persist, explaining why this is the appropriate syntactic class.

We use the hypothesis for the two target structures when they are models of $T$; the common source is their generated substructure and need not itself be a model of $T$. If the hypothesis is read as applying to all target structures, it is stronger and the same proof applies.

Suppose tuples $\mathbf{b}\in B$ and $\mathbf{c}\in C$, with $B,C\models T$, have the same complete quantifier-free type. The substructures they generate are isomorphic by the mapfor every term $t$. Equality of the quantifier-free types makes this map well defined and injective and makes it preserve and reflect all relations. Identify these generated substructures with one common structure. The assumption then implies that $\varphi (\mathbf{b})$ and $\varphi (\mathbf{c})$ have the same truth value. Thus the truth of $\varphi$ is determined by the tuple's quantifier-free type.

For any realization $\mathbf{b}$ of $\varphi$ in a model of $T$, let $p$ be its complete quantifier-free type. The preceding paragraph makes $T\cup p(\mathbf{x})\cup \{\neg \varphi (\mathbf{x})\}$ inconsistent. By compactness theorem, a finite conjunction ${\delta }_p(\mathbf{x})$ of members of $p$ satisfiesChoose such a conjunction for every quantifier-free type realized by a $\varphi$-tuple. These conjunctions cover every realization of $\varphi$. Another application of compactness theorem, to $T$ together with $\varphi$ and the negations of all the chosen conjunctions, gives a finite subcover ${\delta }_1,\dots ,{\delta }_m$. ThereforeThe right side is a quantifier-free formula. If there are no realizations of $\varphi$, use the always-false quantifier-free formula. This proves the common-substructure test for quantifier elimination for the given formula; it does not assume that the source structures are models of the theory.

In the language of a single edge relation $E$, axiomatize an undirected loop-free graph byFor every pair of nonnegative integers $r,s$, add the extension axiom demanding, for any distinct $u_1,\dots ,u_r,v_1,\dots ,v_s$, a new vertex $z$ such thatThese axioms form the theory of the random graph. Repetition of the fresh-vertex requirement also forces infinitude.

To prove quantifier elimination, first eliminate one existential quantifier from a quantifier-free formula. Put that formula into disjunctive normal form, so it suffices to consider a conjunction of literals in a new variable $z$ and the parameter variables. There are two possibilities for a witness: $z$ equals one of the parameters, in which case substitution gives a quantifier-free condition; or $z$ is distinct from all of them. In the latter case, the graph axioms reduce all requirements involving $z$ to specified adjacency or nonadjacency to the distinct parameter vertices. A requirement $E(z,z)$ is impossible, and conflicting requirements at equal parameter vertices are impossible. Every other consistent adjacency pattern is realized by the extension axiom.

There are only finitely many equality patterns of the given parameter tuple. For each, consistency of the literals is a quantifier-free condition, including the unchanged relations among the parameters. Their finite disjunction describes exactly when a witness exists. Thus $\exists z\theta (z,\mathbf{x})$ is equivalent to a quantifier-free formula whenever $\theta$ is quantifier-free. Mathematical induction on formulas now eliminates all quantifiers, using $\forall z\theta \equiv \neg \exists z\neg \theta$. Hence the random-graph theory eliminates quantifiers. The extension axioms also yield the usual countable random graph by a back-and-forth construction.

A 1-embedding, or existential embedding, is a structure embedding $\alpha :A\to B$ satisfyingfor every quantifier-free $\theta$ and every parameter tuple $\mathbf{a}$ from $A$. The forward direction is automatic for an embedding; reflection of existential formulas is the extra property. For an inclusion this says that $A$ is simply closed in $B$. This is weaker than requiring an elementary embedding, which preserves all formulas.

Identify $A$ with its image under $\alpha$. In a language naming every element of $B$, use the same names for elements of $A$ in the two sets of sentencesThis union is consistent. To see finite satisfiability, conjoin the finitely many diagram facts about $B$ into a quantifier-free formula $\delta (\mathbf{a},\mathbf{b})$ and the finitely many elementary-diagram facts about $A$ into $\psi (\mathbf{a})$, where the elements in $\mathbf{b}$ have names outside $A$. Since $B\models \exists \mathbf{y}\delta (\mathbf{a},\mathbf{y})$, the 1-embedding property gives a witnessing tuple in $A$. Interpret the finitely many new names by that tuple. The resulting expansion of $A$ satisfies $\delta$ as well as $\psi$.

By compactness theorem, a model $C$ of this union exists. Its named copy of $B$ gives an embedding $\beta :B\to C$, while its named copy of $A$ is elementary. ConsequentlyThe naming ensures that the two maps agree on the original copy of $A$.

Here ${\forall }_2$ denotes universal-existential sentences, with quantifier-free matrix and possibly empty blocks. Add constants for $A$ and considerWe show that $\Sigma$ is consistent. Suppose a finite subset is inconsistent. Combine its diagram facts as $\delta (\mathbf{c})$ and its finitely many negative existential facts as $\neg \exists {\mathbf{y}}_j{\theta }_j(\mathbf{c},{\mathbf{y}}_j)$. Replacing the new constants by a variable tuple gives the consequenceThis is equivalent to a universal-existential sentence: move all the existential blocks to the front of the disjunction, using the usual nonempty-domain convention. If there are no negative existential facts, the consequence is simply $\forall \mathbf{x}\neg \delta$. By hypothesis $A$ satisfies the displayed consequence. Its named tuple satisfies $\delta$ but none of the existential alternatives, a contradiction.

A model $B$ of $\Sigma$ contains a diagram copy of $A$. Every existential formula false in $A$ is still false in $B$; every one true in $A$ is preserved by the embedding. ThusBoth preservation and reflection are required here; the atomic diagram alone would give only an ordinary embedding.

Let $S$ consist of all universal-existential sentences entailed by $T$, and take $A_0\models S$. By (c), there is an existential embedding of $A_0$ into $B_0\models T$. By (b), $B_0$ embeds in $A_1$ with $A_0\preccurlyeq A_1$. After replacing structures by isomorphic copies, arrange these maps as inclusions. Since $A_1\equiv A_0$, it also satisfies $S$ and the construction can be repeated. This producesThe two interleaved chains have the same union $D$. The elementary chain theorem gives $A_0\preccurlyeq D$. The $B_i$ are an ordinary chain of models of $T$, so the assumed closure under unions of chains gives $D\models T$. Therefore $A_0\models T$. This provesConversely, universal-existential axioms are preserved in such unions: a finite universal tuple occurs in one stage, which already supplies its existential witnesses. The quantifier-free matrix has the same truth value in that stage and in the union. This also explains the inductive first-order theory characterization.

The local omission of a partial type $\Gamma (\mathbf{x})$ by a consistent first-order theory $T$ means that, for every formula $\theta (\mathbf{x})$ consistent with $T$, there is some $\gamma \in \Gamma$ such thatis consistent. Equivalently, no formula consistent with $T$ implies every member of $\Gamma$. Thus every possible local condition has a compatible refinement excluding at least one proposed type formula.

The omitting types theorem states: in a countable first-order language, if $T$ is consistent and locally omits each of countably many finite-arity families ${\Gamma }_j$, then it has a countable model omitting them all. Omission means that no tuple satisfies every formula in the family. In the case of a complete type, local omission is equivalent to the type being nonisolated. Countability of the language and of the list of omission requirements is essential to this formulation.

An atomic model is a model in which every finite tuple's complete type over the empty set is isolated by a formula. An omega-saturated model realizes every complete type in finitely many variables over every finite parameter set; equivalently it realizes all one-variable types over finite parameter sets, then successive realizations give the finite-tuple version.

Suppose $M$ is countable and omega-saturated. Every type in $S_n(T)$ is realized by a tuple in $M$, so $S_n(T)$ is countable. This is a compact Hausdorff Stone space with a clopen basis. Its isolated points are dense. Indeed, if a nonempty clopen subset had no isolated point, split it into two disjoint nonempty clopen subsets and recursively split every resulting subset. Such splits exist because each subset has at least two points and the space is zero-dimensional. Compactness supplies a point in each nested sequence along an infinite binary branch, while disjoint siblings make different branches yield different points. This would give uncountably many points, contradicting countability.

For each $n$, let ${\Gamma }_n(\mathbf{x})$ consist of the negations of all formulas that isolate complete $n$-types. Density of isolated types means that every consistent formula has a consistent refinement to an isolating formula $\delta$; this refinement excludes the member $\neg \delta$ of ${\Gamma }_n$. Thus $T$ locally omits every ${\Gamma }_n$. The omitting types theorem gives a countable model $A$ omitting them all. Every tuple in $A$ therefore satisfies some isolating formula, so $A$ is atomic. If some ${\Gamma }_n$ is itself inconsistent, its omission is automatic and does not obstruct this argument.

The converse about existence is false. Here is a countable atomic model without a countable saturated model. Take a countable set $M$ with unary predicates $P_i$, $i\in \mathbb{N}$, such that every finite Boolean pattern of the predicates occurs infinitely often. For example, use finite binary words paired with a natural number, with $P_i$ recording the $i$th bit when it exists and false otherwise. Add a constant naming each element, and put $T=\mathrm{Th}(M)$ in this countable language. Every tuple of $M$ has its type isolated by equations to its named coordinates, so $M$ is a countable atomic model.

For each infinite binary sequence $\eta$, the familyis finitely satisfiable in $M$: realize its finitely many predicate requirements while avoiding finitely many named elements. By compactness theorem, it extends to a complete one-type. Different sequences give different types, so $S_1(T)$ is uncountable. Any omega-saturated model must realize all these empty-parameter types, which a countable model cannot do. This disproves the existence converse, rather than merely exhibiting an atomic model that is itself nonsaturated.

The Ehrenfeucht theory of an increasing named sequence is complete and has quantifier elimination: the usual one-point cut argument for dense linear orders without endpoints works with the finitely many constants occurring in a formula. Complete types are consequently determined by order relations to the named constants and to any additional parameters.

In the model where the sequence is unbounded above, every finite tuple lies below some $c_N$. Its order relations to $c_0,\dots ,c_N$, together with its internal equality and order pattern, determine its relations to every later constant as well. This finite condition isolates its complete type. Thus model (ii) is an atomic model. It is not omega-saturated, because the finitely satisfiable type $\{c_i<x:i\in \mathbb{N}\}$ has no realization.

In either bounded model, a point above every $c_i$ realizes the typeThis type is not isolated. Any formula belonging to it uses only finitely many constants after quantifier elimination, and its order condition can also be realized below a sufficiently late $c_j$. That realization fails one of the later inequalities in $p_{\infty }$. Hence neither bounded model is atomic.

In model (i), let $d$ be the least upper bound. The type $\{c_i<x:i\in \mathbb{N}\}\cup \{x<d\}$ over the single parameter $d$ is finitely satisfiable by density but unrealized, so this model is not omega-saturated.

In model (iii), the upper tail $U=\{x:c_i<x\text{ for all }i\}$ has no least element. Every consistent one-type over finitely many parameters is realizable. Indeed, it is either an equality type, a cut below or between some of the named constants, or a cut in $U$. The first two cases are realized by equality or by density in the relevant interval. In $U$, finitely many parameters divide the tail into finitely many intervals, each relevant nonempty interval having points by density, absence of a least element in $U$, and absence of a last element in the order. This realizes the third case too. There is no other cut among the increasing sequence: a proper initial segment of its indices is finite. Successive one-variable realizations give all finite-tuple types. ThereforeA least upper bound is thus precisely the obstruction to filling the additional finite-parameter cut in model (i).

We work with the usual infinite-model convention for an omega-categorical theory: it has a unique countably infinite model up to isomorphism. The three conditions are the type-space and automorphism formulations of the Ryll-Nardzewski theorem; the following arguments prove them rather than invoke that theorem. The standard hypothesis that $T$ has infinite models is understood. If finite models are allowed instead, uniqueness among models of size at most countable is the matching convention for condition (i).

We first prove (i) implies (ii). Suppose some type space $S_n(T)$ were infinite. An infinite compact space cannot have every point isolated: its cover by singleton open sets would have no finite subcover. Thus it has a nonisolated complete type $p$. The omitting types theorem gives a countable model omitting $p$. On the other hand, compactness theorem gives a model realizing $p$, and the Downward Lowenheim-Skolem theorem gives a countable elementary submodel containing its realizing tuple. These countable models cannot be isomorphic, since an isomorphism preserves realization of $p$. This contradicts omega-categoricity. Hence every $S_n(T)$ is finite.

Assume every $S_n(T)$ is finite. Each of its points is isolated: choose, for every other type, a formula separating it from the given one, and conjoin the finitely many choices. Thus every finite tuple in every model has an isolated complete type. Moreover every complete type is realized in every model: its isolating formula is consistent with the complete theory, so the theory entails that the formula has a realization.

For clarity, here is the one-point extension argument needed for both remaining assertions. If tuples $\mathbf{a}$ and $\mathbf{b}$ in two models have the same complete type and $c$ is any new element in the first, let $\theta (\mathbf{x},y)$ isolate $\mathrm{tp}(\mathbf{a},c)$. The formula $\exists y\theta (\mathbf{x},y)$ belongs to the type of $\mathbf{a}$, hence also to that of $\mathbf{b}$. Choose $d$ with $\theta (\mathbf{b},d)$. This extends the tuple map to a partial elementary map. If $c$ is different from all earlier entries, the isolating type includes these disequalities, so $d$ is new as well.

Apply this argument alternately to the two enumerations of any two countable models. The resulting back-and-forth map is an isomorphism. Thus (ii) implies (i).

Choose any countable model $A$. The same back-and-forth argument, now within $A$, shows that any two tuples of the same complete type are related by an automorphism of a first-order structure. Conversely an automorphism preserves the type. Hence the orbits of $\mathrm{Aut}(A)$ on $A^n$ are exactly its complete $n$-types. There are finitely many of them for every $n$, so the automorphism group is an oligomorphic permutation group. Therefore (ii) also implies (iii).

Assume $A$ is a countable model of $T$ and its automorphism group is an oligomorphic permutation group. Complete types are constant on automorphism orbits, so only finitely many complete $n$-types are realized in $A$, for each $n$.

These realized types are dense in the Stone topology on a type space $S_n(T)$. Indeed, any nonempty basic clopen set $[\theta ]$ is given by a formula consistent with $T$. Completeness implies $T\models \exists \mathbf{x}\theta$, and thus some tuple in $A$ realizes a type in $[\theta ]$. A finite set of points is closed in a Hausdorff space; if it is also dense, it is the whole space. Therefore $S_n(T)$ equals the finite set of types realized in $A$. This proves (iii) implies (ii), and the previous part then yields (i). We have establishedIn particular, the argument does not assume that an arbitrary countable model is saturated or that its type-orbits coincide before that coincidence has been proved.

For a relational first-order structure $A$, form its Gaifman graph: distinct elements are adjacent when they occur together in a tuple of some interpreted relation. Let $d_A$ be graph distance, with distance infinite between different components. For a tuple $\mathbf{a}=(a_1,\dots ,a_m)$, its radius-$r$ neighbourhood has universeThe neighbourhood structure is the induced relational structure on this set, expanded by constants marking the entries of $\mathbf{a}$ in their original order. Its isomorphism type thus records the centres, not just the unmarked ball. For one binary graph relation, this is the usual union of the radius-$r$ graph balls. This formulation assumes the finite relational signatures used in the finite-model setting.

An exact-count form of the Hanf locality lemma is as follows. For every quantifier rank $q$, put $r=3^q$. If finite relational structures $A,B$ admit a bijection $f:A\to B$ such thatthen $A$ and $B$ agree on every first-order sentence of quantifier rank at most $q$. Equivalently, they have the same number of occurrences of every marked radius-$r$ one-point neighbourhood type. The individual local isomorphisms need not be restrictions of $f$.

A bounded-degree threshold version permits the type counts to be different when both exceed a sufficiently large bound depending on the degree bound and $q$. We need only the exact-count form. Its locality content is that sufficiently large matching neighbourhoods and their multiplicities determine all sentences up to the prescribed quantifier rank.

Suppose a first-order sentence $\theta$ defined the bipartite graphs, equivalently the 2-colourable graphs. Let $q$ be its quantifier rank and $r=3^q$. Choose an odd integer $N>2r+1$, and compareBoth have $2N$ vertices. Every marked radius-$r$ neighbourhood in either graph is a path with $2r+1$ vertices and its middle vertex marked: the choice of $N$ prevents the ball from wrapping around a cycle. Thus every vertex has exactly the same neighbourhood type in both graphs, and that type occurs $2N$ times in each. Any bijection of their universes meets the Hanf locality lemma hypothesis.

Therefore $A$ and $B$ agree on $\theta$. But $A$ is an even cycle and is bipartite, whereas $B$ contains odd cycles and is not bipartite. This contradiction provesThe equal total size is useful here: no large-count threshold or comparison of unequal multiplicities is needed.

Fagin's theorem states that, for a finite relational signature, an isomorphism-invariant class of finite structures has its standard encoding language in NP if and only if it is definable by an existential second-order logic sentencewhere $\psi$ is first-order and the relation variables have fixed finite arities. The forward implication includes the substantive encoding of a polynomially bounded accepting computation by relations. In the reverse implication the relations are polynomial-length certificates and the fixed first-order sentence can be checked in polynomial time. This is a finite-structure characterization; no order need be named in the input signature.

Here equivalence means equivalence on all finite structures of the chosen signature, and an existential sentence means an existential second-order sentence. Suppose, towards a contradiction, that P equals NP. We use that P is closed under complementation, that fixed first-order model checking is polynomial-time, and that guessing a polynomial-length string followed by a polynomial-time test is in NP.

Under this equality, evaluating any fixed second-order logic sentence is in P. Prove this by induction through its quantifiers and Boolean operations. The first-order part is already polynomial-time. If an inner formula can be evaluated in P, existentially quantifying a relation of fixed arity guesses at most $n^k$ bits and then performs the inner polynomial-time test. This gives an NP procedure and hence, under the assumption, a P procedure. A universal relation quantifier is handled by complementing the corresponding existential test. Boolean combinations remain polynomial-time as well. A fixed formula has only finitely many such steps and fixed arities, so the resulting time bound is polynomial.

Consequently every second-order definable class lies in P, hence in NP. By Fagin's theorem it has an equivalent existential second-order sentence. This contradicts the posited second-order sentence with no such equivalent. ThereforeThe proof uses the equality assumption to collapse quantifier alternation; it does not assume an unproved strictness statement about the polynomial hierarchy.

Every fixed second-order logic sentence is evaluable in PSPACE. On a universe of size $n$, a relation of arity $k$ is stored using $n^k$ bits. Enumerate its possible interpretations with a counter of the same polynomial length, recursively evaluate the inner formula and reuse the storage. Universal quantifiers require checking all interpretations; existential ones stop at the first success. The fixed quantifier depth and fixed arities bound total space by a polynomial, even though time can be exponential. First-order quantifiers and Boolean operations require no larger bound.

If $NP=PSPACE$, this places the class defined by the assumed second-order sentence in NP. Fagin's theorem would give an equivalent existential second-order sentence, again contradicting the hypothesis. HenceFor completeness, $NP\subseteq PSPACE$: a polynomial-time nondeterministic computation can be searched deterministically depth first, retaining a polynomial-length computation branch and reusing space. Thus the inequality is a strict containment under the stated hypothesis.

Fix a partial fixed-point logic formula $\varphi (R,\mathbf{x})$, with $R$ of arity $k$. On a finite ordered structure, an interpretation of $R$ is a bit string of length $n^k$. To decide whether some interpretation makes $\varphi$ true at a given tuple, enumerate all these strings and evaluate $\varphi$ for each. Evaluation uses polynomial space by the permitted characterization of PFP, and the enumerating counter also has polynomial length. Storage is reused between interpretations. Thus the resulting pointed-structure property is decidable in PSPACE.

Apply the assumed PFP characterization of PSPACE on ordered structures to this property. It gives a PFP formula $\psi (\mathbf{x})$ such thatTo justify the formula version from a sentence characterization, temporarily name the tuple by finitely many new constants, apply the characterization in that expanded finite signature, and replace those constants by the free variables, renaming bound variables to avoid capture. This does not introduce a new order assumption: the input already interprets $<$ as a linear order. Multiple quantified relations are handled by repeated application.

As usual, a class of structures here is closed under isomorphism and uses standard finite-structure encodings. First suppose $K$ is defined by $\exists R\varphi$, with $\varphi$ in partial fixed-point logic. Deterministically enumerate the polynomial-length encodings of $R$ and evaluate $\varphi$ on each expansion. PFP evaluation is in PSPACE even without a supplied order: a relation of fixed arity requires polynomially many bits, iteration has at most exponentially many states, and a polynomial-length counter suffices to stop after that many stages. If no consecutive stages agree before a repeat must have occurred, the partial fixed point is empty. Nested fixed points have fixed syntactic depth and can be evaluated with reused polynomial storage. Thus the encoding language of $K$ is in PSPACE.

Conversely, suppose that encoding language is decidable in PSPACE. Expand each structure by a freely chosen linear order $R$. On such ordered expansions, the assumed characterization gives a PFP sentence $\psi (R)$ deciding whether the reduct belongs to $K$. Since $K$ is isomorphism-invariant, the answer is independent of the particular chosen order. HenceThe expression inside the second-order quantifier is PFP, since the assertion that $R$ is a linear order is first-order. Every finite universe has a linear order. This proves both directions, using an existentially supplied order when the original signature has none. The construction is also the order-independent consequence of part (a), which shows that existential relation quantification does not increase PFP's power on an already ordered structure.

For an unrestricted binary relation $R$, the extension axioms permit arbitrary directed edges and loops. For each $m\ge 0$ and each choice of bits ${ϵ}_i,{\delta }_i,\eta \in \{0,1\}$, require that every tuple of distinct $x_1,\dots ,x_m$ has a fresh element $y$ withHere $P^1$ denotes $P$ and $P^0$ denotes $\neg P$; the notation is a literal abbreviation, not exponentiation of a relation. Incoming and outgoing choices are independent, and the loop bit is also specified. These are the extension axioms for an unrestricted binary relation. If one instead restricts to undirected loop-free graphs, the allowable patterns reduce to the random-graph extension axioms of Question 2; no such restriction is imposed here.

Let $T_e$ be the theory of the extension axioms for an unrestricted binary relation. It has quantifier elimination. To prove this, consider a conjunction of literals $\theta (y,\mathbf{x})$. A witness $y$ equal to one of the parameters is handled by substitution. A witness distinct from them is governed entirely by a finite pattern of incoming edges, outgoing edges and its loop. For each equality pattern of the parameter tuple, incompatible literals make the pattern impossible, and every compatible pattern is supplied by the appropriate extension axiom. Thus existence of a witness is a finite disjunction of quantifier-free conditions on the parameters. Disjunctive normal form and induction on formulas eliminate all remaining quantifiers.

Given any formula $\varphi (\mathbf{x})$, choose a quantifier-free $\psi (\mathbf{x})$ withBy compactness theorem, finitely many extension axioms ${\sigma }_1,\dots ,{\sigma }_s$ already entail this particular universally quantified equivalence. Each has asymptotic probability one by the assumption. The union bound givesTherefore the universal equivalence also has asymptotic probability one. We obtain asymptotic equivalence to a quantifier-free formula, uniformly over every tuple in each structure satisfying those finitely many axioms. An infinite conjunction of probability-one events is not used; the finite consequence supplied by compactness is essential.

Use only the variable names $x,y$. Define mutually renamed formulas bywhere $D_m^y$ is obtained from $D_m^x$ by globally interchanging $x$ and $y$, including their bound occurrences. By induction, $D_m^x(a)$ means that an increasing chain of $m$ elements starts at $a$. Henceholds exactly when the linear order has at least $n$ elements. Inner quantifiers may bind the name $x$ again, but their scope is only the nested subformula; the comparison $x<y$ still refers to the preceding point. This finite-variable logic construction works on finite and infinite linear orders.

Choose a variable name $y\ne x$ among the $k$ available names and defineThe formula $C_m^y$ is obtained by interchanging the names $x,y$ throughout $C_m^x$, including bound occurrences. Its only free variable is $y$. A permutation of variable names preserves membership in $L^k$, so every formula in this recursion still uses at most the original $k$ names. In particular, bound variables inside a copy of $\varphi$ do not accidentally capture the previous comparison: their scope stays inside that copy.

Induction proves that $C_m^x(a)$ holds exactly when there is an increasing $m$-tuple of satisfying elements whose first entry is $a$. Any set of $m$ distinct points in a linear order can be put in increasing order. Therefore the variable-recycling count on a linear orderis the required sentence. This does not use counting quantifiers or additional variable names, and it applies equally to infinite linear orders.

We use the finite-structure convention of Section B. Express that $<$ is a strict linear order by irreflexivity, transitivity and comparability of distinct points. Express that $E$ is an equivalence relation by reflexivity, symmetry and transitivity. All these assertions use at most the three variable names $x,y,z$.

In a finite linearly ordered structure, every equivalence class has a unique least element. The two-variable formulaselects exactly those least elements. Apply part (b) to this formula, using $k=3$, to obtain ${\mathrm{Rep}}_n\in L^3$ saying that at least $n$ representatives exist. The required sentence isThis gives the least representatives of finite equivalence classes construction. Under the two structural axioms, counting representatives is exactly counting equivalence classes.

Finiteness is essential to the assertion as written in this section. If it were interpreted as applying to all infinite structures, the general claim would fail, not merely this choice of representatives. Partition the rational order into three dense classes, or into four dense classes, and let $E$ mean belonging to the same class. In the three-pebble version of the Ehrenfeucht-Fraïssé game, the duplicator can play indefinitely between these structures: after one pebble is moved, at most two old classes remain represented; a new point can be placed in the required interval in its corresponding old class, or in a class different from both. Density makes every required placement possible in either structure. Thus the structures agree on all $L^3$ sentences although one has three classes and the other four. The finite reading of the printed request is therefore necessary for $n=4$.