Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2007 / B / 8

Here $\mathcal{B}\subseteq \mathcal{A}$ means a substructure, so the smaller carrier contains all named constants, is closed under every function symbol, and has each relation restricted from the larger first-order structure. First-order term evaluation on tuples from $B$ agrees in the two first-order structures. Consequently atomic formulas agree, and induction on Boolean connectives makes every quantifier-free formula agree as well.

Write an arbitrary universal sentence of $T$ as $\forall \vec{x}\theta (\vec{x})$ with quantifier-free matrix. Every tuple from $B$ is also a tuple from $A$, so $\theta$ holds at that tuple in $\mathcal{A}$. Quantifier-free agreement transfers it to $\mathcal{B}$. Since the tuple was arbitrary, $\mathcal{B}$ satisfies the universal sentence. ThusAn arbitrary subset without the substructure operations and relation restrictions would not be the hypothesis used by this formal proof.

The set of closed-term values is nonempty because the first-order language has a constant. It contains the value of every constant. If $f$ is an $r$-ary function symbol and $t_1,\dots ,t_r$ are closed terms, thenwhich is another closed-term value. Hence the set is closed under every operation. Restrict the operations and relations of $\mathcal{A}$ to it; this defines a substructure $\mathcal{B}$ whose carrier is exactly the specified set.

Part (i) now applies to the universal first-order theory, givingIt is the substructure generated by the first-order language's constants, often called the ground-term substructure. The source's constant-symbol assumption ensures its nonemptiness, even when no other elements can be generated.

Adjoin to $T$ the negations of all closed-term instances of $\theta$. If the resulting set had a first-order model $\mathcal{A}$, its ground-term substructure $\mathcal{B}$ from (ii) would still first-order model $T$. The assumed existential consequence therefore supplies a tuple $\vec{b}$ in $\mathcal{B}$ satisfying $\theta$. Each $b_j$ is the value of a closed term $t_j$.

Quantifier-free agreement between a substructure and its ambient first-order structure givescontradicting the adjoined negation of this very ground instance. Thusis unsatisfiable. Compactness theorem gives a finite unsatisfiable subset. Its finitely many ground negations imply that, for some finite list of first-order term tuples,If the finite subset already shows $T$ itself inconsistent and supplies no ground negations, choose any one closed-term tuple using the available constant; then any first-order sentence is a consequence of $T$, so $m=1$ suffices. Otherwise the selected list is nonempty. This also explains why the conclusion contains a finite disjunction rather than necessarily one universal choice of a witness first-order term.