Past exam of the computer science course of the University of Oxford / 2015 / Logic and proof / 2

A first-order theory in a fixed first-order signature is a set of first-order sentences. Under the closed-theory convention used in the question, it contains all its semantic entailments: $T\models \theta$ implies $\theta \in T$. One can equivalently begin with a set of axioms and take its closure under consequence.

A complete theory is a consistent first-order theory that decides every first-order sentence $\theta$ in its first-order signature:Consistency ensures that exactly one of these alternatives holds.

A decidable theory is one for which an algorithm always terminates and determines whether a given first-order sentence is a consequence:If the first-order theory is already closed under consequence, this is its membership problem. It is a condition on the consequences, not merely on whether the chosen set of axioms has a decidable membership test.

A first-order theory $T$ admits quantifier elimination when every first-order formula $\phi (\bar{x})$ has a quantifier-free formula $\psi (\bar{x})$, in the same first-order signature and with no additional free variables, such thatThus all first-order models of $T$ agree that the two first-order formulas define the same tuples. This definition concerns first-order formulas with free variables, as well as first-order sentences; merely deciding closed assertions would be weaker. The existence of an effective procedure is an additional issue, supplied by the explicit construction in part (d).

Use the Rado graph on the natural numbers. Interpret the binary relation byThe relation is symmetric by its definition, and $E(i,i)$ is always false. Thus this first-order structure satisfies $F_1$ and $F_2$.

To verify an extension axiom, take distinct $x_1,\dots ,x_n$. Choose a natural number $k$ larger than every $x_i$ and putThe powers are distinct, so there are no carries in this binary representation. In particular $y>x_i$ for every $i$, and the bit in position $x_i$ is one exactly when $i<m$. Therefore $y$ is different from all the given vertices, is adjacent to $x_1,\dots ,x_{m-1}$, and is not adjacent to the others. If the $x_i$ are not distinct, the antecedent of the extension axiom is false, so it places no restriction. The case $n=0$, if included in the convention for natural numbers, simply asks for a nonempty domain, which this first-order structure has.

For example, prescribing adjacency to $1$ and $3$ and nonadjacency to $2$ permits $k=4$ and $y=16+2+8=26$, whose binary representation is $11010$. This explicitly realizes the required pattern. HenceReordering a tuple makes the extension axioms applicable to any two disjoint finite sets of vertices, with any desired adjacency and nonadjacency pattern. This is the extension property defining the theory of the random graph.

It suffices to eliminate one existential quantifier from a quantifier-free formula $\theta (y,\bar{x})$. Indeed, logical connectives preserve equivalence, and a universal quantifier can be rewritten using $\forall y\alpha \equiv \neg \exists y\neg \alpha$. An induction on the construction of a first-order formula then eliminates all its quantifiers from the inside out.

Convert $\theta$ to disjunctive normal form. Since existential quantification distributes over a finite logical disjunction, consider a single logical conjunction of atomic first-order formulas and their negations. There are no function or constant symbols in this first-order signature, so its atoms are equalities between variables and instances of $E$ between variables.

For a tuple $\bar{x}=(x_1,\dots ,x_r)$, enumerate its possible complete atomic diagrams $\delta (\bar{x})$. Such a quantifier-free formula specifies which variables are equal and, between distinct equality classes, exactly which pairs are adjacent. Keep only the diagrams in which first-order equality is an equivalence relation and $E$ is symmetric and irreflexive. There are finitely many diagrams for each $r$, and every tuple in a first-order model of $T$ satisfies exactly one of them. Every retained diagram is realizable: insert one vertex for each equality class successively, using the extension axioms to prescribe its adjacency to earlier vertices.

Fix one diagram $\delta$. A potential existential witness for $y$ has one of two forms.

All first-order formulas involving only $\bar{x}$ are already decided by $\delta$. Therefore, for each diagram, the existence of a suitable $y$ has a definite answer, determined by a finite syntactic test. Let $\mathcal{D}$ be the set of diagrams for which at least one disjunct and at least one of the two witness cases succeeds. ThenThe right side is a quantifier-free formula. An empty logical disjunction means false, and for an empty tuple the empty atomic diagram means true. These logical truth constants also handle closed first-order sentences in this constant-free first-order signature.

For a concrete illustration of the fresh-witness case,If $x_1=x_2$, the edge requirements conflict. Otherwise the extension property supplies a vertex outside the finite set of parameters with the desired pattern; the extra avoidance of $x_3$ causes no obstruction. The general diagram construction handles all such equality coincidences systematically and proves quantifier elimination.

By part (c), $T$ has a first-order model, so it is consistent. By part (d), every first-order sentence is equivalent modulo $T$ to a quantifier-free sentence. In the first-order signature consisting only of $E$ and first-order equality, there are no constant symbols, no ground first-order terms, and no nullary predicates. Thus a closed quantifier-free formula reduces to true or false, using the logical truth constants. All first-order models of $T$ therefore agree on every first-order sentence:

The construction in part (d) is effective. Conversion to disjunctive normal form, enumeration of finite equality partitions and adjacency patterns, and testing the finitely many witness cases are all terminating operations. Apply them recursively to a given first-order sentence and evaluate the final truth constant. This decides whether the first-order sentence belongs to $T$, givingNo useful bound on the running time is needed for decidability; the potentially large enumeration still always terminates.

Use the back-and-forth method. Enumerate the two domains without repetitions as $a_0,a_1,\dots$ and $b_0,b_1,\dots$. We construct a sequence of finite maps, each a partial isomorphism of structures,starting with the empty function. Each $f_s$ is a bijection between finite subsets of the domains and preserves both adjacency and nonadjacency on its domain.

At a forth step, choose the first $a_i$ outside the current domain. List the finitely many domain vertices as $u_1,\dots ,u_r$. In $\mathcal{B}$, prescribe that the new image $b$ be adjacent to $f_s(u_j)$ exactly when $a_i$ is adjacent to $u_j$ in $\mathcal{A}$. Since the image vertices are distinct, an extension axiom in $\mathcal{B}$ supplies such a $b$ outside the entire current range. Extend $f_s$ by $a_i\mapsto b$. This preserves injectivity, adjacency and nonadjacency, including the absence of loops.

At a back step, choose the first $b_i$ outside the current range. Apply the same argument to the inverse partial isomorphism of structures in $\mathcal{A}$, finding a fresh preimage with the required adjacency pattern to the current domain. Extend $f_s$ by this new pair. Alternate forth and back steps indefinitely.

DefineBecause each finite function extends the preceding one, this is a well-defined injective function. The forth steps eventually include every $a_i$ in its domain, and the back steps eventually include every $b_i$ in its range, so $f$ is a bijection. Given any $u,v$, both lie in the domain of some finite $f_s$, where the edge equivalence already holds. It therefore also holds for $f$:Thus the two first-order structures are isomorphic. Alternating the steps is essential for surjectivity: repeatedly extending only the domain would merely construct an embedding into $\mathcal{B}$.