Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2007 (C1.1, DMAC 2460, DMPC 2460)

This University of Oxford Part C paper is cross-listed for Mathematics and Mathematics and Philosophy. Section A concerns Gödel second incompleteness theorem and provability logic; section B concerns model theory. ^[ref] The archive contains the complete editable four-page transcription. Bounded official-source searches found no advertised answers to this exact paper. All 31 source leaves are answered below. The enumeration and function-definability conventions are stated explicitly, and the canonical-model construction uses the function-free setting permitted by the source.

Use the numeralwise enumeration in arithmetic convention in the first-order theory: membership supplies a standard stage with a provable enumerating instance, while nonmembership makes every standard-stage instance refutable. Put $D=\{n:P⊢E_n(\bar{n})\}$. By the definition of $a$, the diagonal instance $E_a(\bar{a})$ is exactly $G$.

If $P⊢G$, then $a\in D$. Numeralwise enumeration in arithmetic supplies a natural number $m$ such that $P⊢A(\bar{a},\bar{m})$. But universal instantiation of $G$ gives $P⊢\neg A(\bar{a},\bar{m})$. This contradicts first-order consistency. ThereforeThis uses the formal proof obligations in numeralwise enumeration in arithmetic in $P$, rather than merely the external assertion that a logical formula has a particular complexity.

One-consistency says that no bounded arithmetic formula $F(x)$ has a provable existential closure while each of its standard numeral instances is refutable. It implies first-order consistency, since an inconsistent classical first-order theory proves every logical formula.

If $P$ is one-consistent, (i) gives $P⊬G$, so $a\notin D$. Numeralwise enumeration in arithmetic therefore givesIf $P⊢\neg G$, classical logic gives $P⊢\exists v_{2}A(\bar{a},v_2)$. The matrix is bounded, and the preceding displayed derivations refute every standard instance. This violates one-consistency. ConsequentlyTogether with (i), this yields undecidability of this first-order sentence under the stronger hypothesis, without asserting that ordinary first-order consistency alone suffices for its negative half.

Bounded completeness of an arithmetic theory means that every bounded arithmetic first-order sentence true in the standard natural numbers is provable in $S$. If $S$ is first-order consistent and proves a false bounded arithmetic sentence $B$, bounded completeness of an arithmetic theory also proves its true bounded negation, a contradiction. Conversely, if every bounded theorem is true, $S$ cannot be inconsistent, because inconsistency would prove the false bounded arithmetic sentence $0=1$. ThusIf $S$ is one-consistent and proves $\exists xB(x)$ with bounded matrix, that existential sentence cannot be false: otherwise every $\neg B(\bar{n})$ would be a true bounded arithmetic sentence and hence provable, contrary to one-consistency. Thus $S$ has Sigma-1 soundness.

Conversely, Sigma-1 soundness excludes inconsistency. If $S⊢\exists xB(x)$, it supplies a standard witness $n$ with $B(n)$ true. Bounded completeness of an arithmetic theory proves $B(\bar{n})$, so first-order consistency forbids a formal proof of $\neg B(\bar{n})$. Hence there cannot simultaneously be refutations of all standard instances. ThereforeFinite blocks of existential logical variables are treated as finite tuples of witnesses, with the same argument.

Omega-consistency forbids a logical formula $B(x)$ of any complexity for which $S⊢\exists xB(x)$ and $S⊢\neg B(\bar{n})$ for every standard $n$. The difference from one-consistency is that the matrix is unrestricted. It implies first-order consistency.

For a complete first-order consistent classical first-order theory, theorem membership obeys the ordinary Boolean truth tables. For example, it proves a conjunction exactly when it proves both conjuncts; completeness and first-order consistency also make theoremhood of a negation the complement of theoremhood of the first-order sentence. Omega-consistency additionally gives the witness propertyThe reverse implication is existential introduction. For the forward implication, if no standard instance were provable, completeness would give a formal proof of each negated instance, violating omega-consistency. This works also after replacing additional free variables by numerals.

Now induct on logical formulas with their remaining free variables replaced by standard numerals. At the atomic level, the equivalence between theoremhood and standard truth follows from bounded completeness of an arithmetic theory and bounded soundness of an arithmetic theory from (b). The Boolean steps use the truth-table facts just proved. The existential step uses the witness property and the induction hypothesis on its matrix; universal quantification follows by negation. Hencefor every first-order sentence $X$. Completeness ensures it decides each first-order sentence, and this equivalence ensures every decision is correct.

Start with the supplied bounded-complete, one-consistent first-order theory $T$ proving a false first-order sentence $F$. Replace it by its deductive closure, which preserves these properties and contains $F$. Enumerate the arithmetic first-order sentences as $X_0,X_1,\dots$. Recursively extend the current first-order theory by either $X_n$ or $\neg X_n$, choosing an extension which remains one-consistent as permitted by the supplied lemma, and then take its deductive closure. Call the resulting increasing sequence $T_n$, with $T_0$ the initial first-order theory, and put $S={\bigcup }_n{T}_n$.

Every stage is still bounded-complete. By (b), every stage has Sigma-1 soundness. If $S$ proved a false Sigma-1 first-order sentence, the finite formal proof would use assumptions from one stage $T_n$, contradicting its Sigma-1 soundness. Thus $S$ has Sigma-1 soundness and is bounded-complete, so (b) makes it one-consistent.

This soundness of an arithmetic theory argument is essential: the definition of one-consistency involves infinitely many standard refutations, so it would be insufficient merely to say that a violation has a finite formal proof. What has a finite formal proof is the false existential sentence, and bounded completeness of an arithmetic theory is what turns one-consistency into the needed soundness of an arithmetic theory condition.

The union is deductively closed because each formal proof has finitely many assumptions. It contains either $X$ or $\neg X$ for every first-order sentence, by the numeralwise enumeration in arithmetic, and contains the false first-order sentence $F$. If it were omega-consistent, (c) would make it correct on all first-order sentences, contradicting $F$. We have therefore constructedOmega-consistency always implies one-consistency by restricting its matrices. This counterexample proves that the converse is strictly false.

A logical formula separates $A$ from $B$ in $S$ if it is provable at the standard numeral tuple of every member of $A$ and refutable at that of every member of $B$:There is no obligation on tuples outside the two sets. In a first-order consistent first-order theory these two obligations make $A$ and $B$ disjoint.

Let $h$ be the Gödel number of $H(v_1)$ and take the literal diagonal first-order sentence $R=H(\bar{h})$. If $S⊢R$, then $h$ belongs to the second source set, so separation gives $S⊢\neg H(\bar{h})$, a contradiction. If $S⊢\neg R$, then $h$ belongs to the first source set, so separation gives $S⊢H(\bar{h})$, again a contradiction. HenceThe direction of separation matters: here $H$ is provable on refutable diagonal codes and refutable on provable diagonal codes.

Write $H(\vec{v})$ for the proposed stage-comparison logical formula and fix a standard tuple $\vec{a}$. If $\vec{a}\in A$, numeralwise enumeration in arithmetic supplies a standard $m$ with $S⊢F(\overline{\stackrel{⃗}{a}},\bar{m})$. Disjointness gives $\vec{a}\notin B$, so $S⊢\neg G(\overline{\stackrel{⃗}{a}},\bar{j})$ for every standard $j$, in particular $j=0,\dots ,m$. The source's finite initial-segment axiom combines this finite list intoUse $\bar{m}$ as the existential witness to obtain $S⊢H(\overline{\stackrel{⃗}{a}})$.

If instead $\vec{a}\in B$, choose $n$ with $S⊢G(\overline{\stackrel{⃗}{a}},\bar{n})$. Disjointness gives refutations of $F(\overline{\stackrel{⃗}{a}},\bar{j})$ for all $j$, so the finitely many $j\le n$ giveFor an arbitrary $x$, the source's comparison axiom gives $x\le \bar{n}$ or $\bar{n}\le x$. In the first case the first conjunct of the proposed witness condition is false. In the second case $y=\bar{n}$ witnesses failure of its bounded universal conjunct, since $G(\overline{\stackrel{⃗}{a}},\bar{n})$ is provable. Generalization over $x$ therefore gives $S⊢\neg H(\overline{\stackrel{⃗}{a}})$.

Thus the logical formula separates $A$ from $B$. The formal proof uses the enumerators' numeralwise positive and negative formal proof properties and the two explicit order principles supplied in the source; it does not assume the first-order theory can decide arbitrary unbounded existential logical formulas.

A logical formula $D(\vec{x},y)$ weakly defines a total numerical function $f$ in $S$ if, for every standard input tuple $\vec{n}$ and $m=f(\vec{n})$,Strong definability of a numerical function additionally requires the internal uniqueness statementTogether with the positive instance, this is equivalent to proving $\forall y(D(\overline{\stackrel{⃗}{n}},y)\leftrightarrow y=\bar{m})$ for each standard input. The universal quantifier is the extra strength: it covers nonstandard potential outputs in first-order models of $S$. These are the weak and strong function conventions used here. ^[ref]

Suppose the graph of the total function is Sigma-1. Its complement is also Sigma-1, sinceReplace the graph assertion on the right by its Sigma-1 definition; existential quantifiers can be collected into one block. Bounded completeness of an arithmetic theory supplies numeralwise stage enumerators for each of these two disjoint complementary sets. Apply (b) to them. Its separating logical formula is provable exactly at the required graph tuples in the positive direction and refutable at all the other standard tuples, proving weak definability of a numerical function.

Using the graph logical formula alone would only supply positive instances from true existential witnesses; the separation construction is what supplies the negative-instance formal proofs without assuming Sigma-1 soundness or completeness for false Sigma-1 statements.

Let $d(n)$ be the Gödel number of the diagonal first-order sentence obtained by substituting $\bar{n}$ into the one-free-variable logical formula with code $n$, with an arbitrary default value on noncodes. By the assumptions and (c), this total function has a strong defining logical formula $D(x,y)$.

For the specified $F$, form the one-variable logical formulaLet $h$ be the Gödel number of $H$ and put $C=H(\bar{h})$. Then $d(h)=┌C┐$. Strong definability of a numerical function at this particular standard input givesSubstitution into the existential definition yieldsThe permitted equivalence between the source's two substitution notations identifies this with its requested fixed point. Bound variables are renamed when necessary before forming $H$, so the substitution is capture-free. This constructs one particular first-order sentence from the code of the logical formula which applies $F$ to its own diagonal output.

Write $\square A$ for $P(┌A┐)$. A standard arithmetical provability predicate obeys the Hilbert-Bernays-Löb derivability conditions:The first condition is a rule about theorems; the latter two are statements proved within the first-order theory. When the terminology also includes external adequacy, require that $P(\bar{n})$ be true in the standard natural numbers exactly when the logical formula with code $n$ has an $S$-proof.

For Peano arithmetic, code finite strings, logical formulas and formal proof sequences by natural numbers. Formal proof checking is effective and has an arithmetized bounded checking relation with its computation data. Existentially assert the existence of a correct formal proof code and any required checking data. The resulting predicate symbol is Sigma-1, and its standard truth means exactly that an actual finite PA formal proof exists. Effective operations on formal proof codes combine an implication formal proof with an antecedent formal proof, and turn a formal proof into a formal proof that its code is a formal proof; PA verifies those constructions. They give distribution and positive introspection, while an actual theorem's finite formal proof gives its internal provability assertion. This is the requested rough construction, with the three internal formal proof properties distinguished from external agreement.

Abbreviate $P(┌A┐)$ by $\square A$. Since $S⊢\neg X$, it proves $X\to G$. The theoremhood and distribution conditions giveThe fixed-point equation gives $S⊢G\to (\square G\to X)$, because $G$ implies $\neg \square G$ and a false antecedent implies any conclusion. Applying theoremhood and distribution yieldsPositive introspection gives $\square G\to \square \square G$; distribution then gives $\square G\to \square X$. Thus $S⊢\square G\leftrightarrow \square X$. Combining with $G\leftrightarrow \neg \square G$ provesIn particular, choosing a fixed logical contradiction for $X$ identifies this Gödel sentence with the formal consistency statement of $S$.

If $S⊢G$, theoremhood gives $S⊢\square G$, while the fixed-point equivalence also gives $S⊢\neg \square G$. Therefore first-order consistency implies $S⊬G$.

If $S\cup \{\neg G\}$ were inconsistent, the deduction theorem and classical propositional logic would give $S⊢\neg \neg G$, hence $S⊢G$. This is impossible by the preceding argument. ThereforeThis is a syntactic first-order consistency result. It does not claim that the extra axiom is true in the standard natural numbers or that the extended first-order theory is sound.

First establish the transfer of provability requested in the hint. The propositional theorem $X\to (\neg G\to X)$ and the derivability conditions giveThe supplied arithmetized deduction equivalence identifies the right-hand provability assertion, within $S^{\ast }$, with ${\square }^{\ast }X$. HenceChoose a fixed contradiction $\perp$ for $X$. Part (b) gives $S⊢G\leftrightarrow \neg \square \perp$, so adjoining $\neg G$ gives $S^{\ast }⊢\square \perp$. The transfer implication now gives $S^{\ast }⊢{\square }^{\ast }\perp$.

Apply (b) inside $S^{\ast }$ to its own Gödel sentence: it proves $G^{\ast }\leftrightarrow \neg {\square }^{\ast }\perp$. The last provability assertion therefore entailsThus the extension proves the negation of its own Gödel sentence as well. When $S$ is first-order consistent, (c) says this phenomenon occurs in a first-order consistent extension; the extension asserts an internal formal proof of contradiction without there being an actual standard formal proof of contradiction.

All implications in this argument are theorems of the extension $S$. From $Y\to (\square Y\to X)$, necessitation and normal modal distribution giveAxiom4 gives $\square Y\to \square \square Y$, soUnder the additional propositional antecedent $\square X\to X$, this theorem implies $\square Y\to X$. The reverse half of the fixed-point equivalence, $(\square Y\to X)\to Y$, consequently gives the theoremNecessitate that theorem and apply distribution to obtain $\square (\square X\to X)\to \square Y$. Combining with $\square Y\to \square X$ provesNecessitation was applied to a theorem after its propositional antecedent had been incorporated, never directly to a temporary assumption.

Take $\square A={\mathrm{Pr}}_{PA}(┌A┐)$ for the standard formal proof predicate symbol and putUse as given the arithmetization of syntax in PA, the derivability conditions, and the diagonal lemma. The latter supplies the fixed point needed in (a), and the former conditions interpret its normal modal distribution, necessitation on theorems and axiom4. Thus the argument in (a) proves the internal Löb implication in PA. With $X=\perp$ it readsThe inner implication is the first-order consistency first-order sentence $\neg \square \perp$, so contraposition givesThis is the arithmetic statement of the second incompleteness theorem proved within PA: if PA is first-order consistent, there is no PA formal proof of its first-order consistency first-order sentence. The displayed implication is a PA theorem without assuming that PA proves its antecedent.

For the corresponding external consequence, if a first-order consistent PA proved ${\mathrm{Con}}_{PA}$, theoremhood would give a formal proof of its boxed assertion. The displayed theorem together with the supposed formal proof of first-order consistency gives its negation, contradicting first-order consistency. Hence an externally first-order consistent PA does not prove its own first-order consistency.

Put $Y=\square X\to X$. The Löb axiom gives $\square Y\to \square X$. Consequently $Y$ implies $\square Y\to X$: if $\square Y$ holds, first obtain $\square X$ and then apply $Y$.

For the other direction, $X\to Y$ is a propositional theorem. Necessitation and distribution give $\square X\to \square Y$. Hence $\square Y\to X$ implies $\square X\to X$, which is $Y$. We have proved the unboxed theoremNecessitation yieldsThis is the explicit fixed point for the modalized operator $Z\mapsto (\square Z\to X)$.

Use the supplied uniqueness theorem for the modalized logical formula $A(p)=\square p\to X$. Its occurrence of $p$ is boxed, and the source assumes $p$ does not occur in $X$. Choose another first-order sentence letter $q$ absent from $X$ and from $p$. Besides the uniqueness theorem and propositional reasoning, use that GL is closed under uniform substitution in modal logic.

Let $Y=\square X\to X$. Uniformly substitute $Y$ for the fresh letter $q$ in the uniqueness theorem. Since $q$ occurs nowhere in $X$, this givesPart (c) proves the second conjunct outright. Propositional reasoning removes that already-proved conjunct and yieldsThe freshness conditions make the substitution legal and ensure it changes only the placeholder intended for the second fixed point.

A canonical first-order structure is generated by its names: every element is the value of a closed term. In the function-free setting permitted here, this means every element is the interpretation of a constant symbol. Equivalently, the natural map from closed terms modulo logical equality in the first-order structure onto its carrier is surjective. When canonical is defined specifically using constant names, the same definition and all the arguments below apply in this function-free setting.

A full set of first-order sentences has the witness property in its own first-order language: whenever it proves an existential sentence $\exists x\varphi (x)$, some closed term $t$ satisfies that the set proves $\varphi (t)$. In a deductively closed set, one can equivalently state this using membership of the first-order sentences. In the function-free setting the witness first-order term is a constant symbol. This is the Henkin witness property; fullness does not by itself replace the separate requirements of first-order consistency and completeness.

A sufficient condition is that $T$ be first-order consistent, complete, and full in its own first-order language. Work in the allowed function-free setting. Since $T$ proves the logically valid first-order sentence $\exists x(x=x)$, fullness guarantees at least one constant and a nonempty collection of names.

Form the carrier from equivalence classes $[c]$ of constant symbols underLogical equality logic makes this an equivalence relation. Interpret a constant by its class and interpret each relation symbol bySubstitution of equals makes this independent of representatives. This defines a canonical first-order structure because every carrier element is named by a constant.

The truth lemma, proved by induction on logical formulas with constants substituted for their free variables, saysAtomic formulas hold by construction; completeness and first-order consistency give the Boolean steps. For the existential step, a witness in the first-order structure is a named class, so its truth gives a proved instance and hence a proved existential sentence. Conversely a proved existential sentence has a constant witness by fullness, and the induction hypothesis realizes that instance in the first-order structure. The universal case follows by negation. Thus $\mathcal{M}\models T$, provingThe witness condition is needed in the original first-order language; adding new constants produces a canonical first-order structure in an expanded first-order language, which is a different assertion.

A prime model of a complete theory $T$ is a first-order model admitting an elementary embedding of first-order structures into every first-order model of $T$. Let $\mathcal{A}\models T$ be canonical and $\mathcal{B}\models T$. For each closed term $t$, defineEvery element of $A$ has a name, so this defines the desired map on all of $A$. If two first-order terms agree in $\mathcal{A}$, their logical equality first-order sentence holds in one first-order model of the complete theory and therefore in every first-order model of it; they agree in $\mathcal{B}$. This proves well-definedness. If they are distinct in $\mathcal{A}$, their inequality holds throughout the complete theory as well, proving injectivity.

For every logical formula $\varphi (\vec{x})$ and named tuple ${\vec{t}}^{\mathcal{A}}$, the substituted first-order sentence $\varphi (\vec{t})$ has the same truth value in the two first-order models by completeness of $T$. ConsequentlyThus $e$ is elementary. Since $\mathcal{B}$ was arbitrary, every such canonical first-order structure is prime. This formal proof also handles closed-term generation when function symbols are present; under the constant-name convention one simply uses constants as the first-order terms.

A first-order theory is a set of first-order sentences in a fixed first-order language, often identified with its deductive closure. It is $\kappa$-categorical if it has a first-order model of cardinality $\kappa$ and all first-order models of that cardinality are isomorphic as first-order structures in that same first-order language. In particular, an isomorphism must preserve the named constants as well as the order.

A first-order theory is complete if it is first-order consistent and decides every first-order sentence: for each $\sigma$ it entails either $\sigma$ or $\neg \sigma$. Equivalently all its first-order models satisfy exactly the same first-order sentences. First-order consistency is included to exclude the vacuous first-order theory with no first-order models. The distinctions matter here: naming infinitely many ordered points changes countable categoricity without destroying completeness.

Use two expansions of the rational order. In the first interpret $c_n=n$, so the named sequence is unbounded above. In the second interpret $c_n=-1/n$, so the named sequence is strictly increasing but has upper bounds in the rational order. Both expansions are countably infinite first-order models of the specified first-order theory.

An isomorphism preserving each $c_n$ would preserve the existence of an element greater than all the named constants, since any such element in one first-order structure would map to such an element in the other. The first first-order structure has none and the second has, for instance, $0$. They cannot be isomorphic. ThusThe property of lying above all $c_n$ is an infinite partial type rather than a single first-order sentence. This is why its realization can distinguish the two first-order models without contradicting the completeness established in (iv).

In a countable first-order model, the finitely many named constants split the order into the open intervalstogether with the $n$ named points. Each interval is a countable dense linear order without endpoints in its induced order. It is nonempty and infinite by density and the absence of endpoints.

Use Cantor's classification of countable dense linear orders without endpoints: each such interval is isomorphic to the rational order. It follows by a back-and-forth method extending finite increasing partial bijections alternately along enumerations of the two orders. Given two first-order models of ${\mathrm{DLO}}_n$, choose isomorphisms between their corresponding intervals and send each named point to its counterpart. Their union is an increasing bijection preserving all constants, hence an isomorphism in $L_n$.

There are countable first-order models, for example any finite increasing list in the rational order. ThereforeFor $n=0$, the same argument is just the classification theorem for the whole order.

Use the completeness of the first-order theory of dense linear orders without endpoints and its quantifier elimination. After naming finitely many increasing constants, quantifier elimination still holds in the expanded first-order language: treat these constants as fixed parameters when eliminating quantifiers. Every quantifier-free sentence is a Boolean combination of logical equalities and order comparisons of the named constants, all decided by their stated strict increasing order. Hence ${\mathrm{DLO}}_n$ is complete.

An alternative formal proof of this finite case uses the stated general theorem that a first-order theory in a countable first-order language with only infinite first-order models and a unique countable first-order model is complete: if first-order models disagreed on a first-order sentence, downward Löwenheim-Skolem would give disagreeing countable first-order models. Part (iii) supplies the uniqueness.

Every first-order sentence of $L_{\omega }$ mentions only finitely many constant symbols, hence belongs to some $L_n$. Its truth is decided by ${\mathrm{DLO}}_n$, and every first-order model of ${\mathrm{DLO}}_{\omega }$ has a reduct satisfying that finite first-order theory. Thus the larger first-order theory also decides every first-order sentence. The rational-order examples in (ii) establish first-order consistency. ConsequentlyThere is no contradiction with (ii): completeness is agreement on individual finite first-order sentences, while categoricity requires a global isomorphism respecting all constants simultaneously.

An $n$-type over a first-order theory $T$ is a set of logical formulas in the displayed $n$ free variables first-order consistent with $T$. A complete type chooses exactly one of $\varphi$ and $\neg \varphi$ for each such logical formula. Equivalently it is a maximal consistent such set. For parameter-free partial types the logical formulas use the original first-order language; partial types over parameters use additional names for those parameters.

A partial type $p(\vec{x})$ is principal if some logical formula $\theta (\vec{x})$ first-order consistent with $T$ implies every member of $p$ modulo $T$:Such a $\theta$ is a principal formula of a type of the partial type. For a complete type it isolates that partial type, so principal complete types are exactly isolated types.

For a tuple $\vec{a}$ in a first-order structure $\mathcal{A}$, its parameter-free partial type isIt is a complete type over $\mathrm{Th}(\mathcal{A})$ because the first-order structure decides the truth of every logical formula at that tuple.

Let $\vec{a}\in A^n$, with $A$ finite, and put $T=\mathrm{Th}(\mathcal{A})$. There are only finitely many competing tuples $\vec{b}\in A^n$. For each whose complete type differs from that of $\vec{a}$, choose a logical formula ${\varphi }_{\vec{b}}$ true at $\vec{a}$ and false at $\vec{b}$. Such a logical formula exists by the inequality of their complete types, negating a distinguishing logical formula if necessary.

Let $\theta$ be the conjunction of this finite list, or logical truth if the list is empty. It is true at $\vec{a}$, and every tuple satisfying it has the same partial type as $\vec{a}$. For each $\psi \in \mathrm{tp}(\vec{a})$, the first-order sentenceis therefore true in $\mathcal{A}$ and belongs to $T$. The logical formula $\theta$ is first-order consistent with $T$ because it is realized at $\vec{a}$. It is consequently a principal formula of a type of the partial type, proving every partial type realized in a finite first-order structure is principal. Finiteness of the first-order structure, rather than finiteness of the first-order language, is what makes the conjunction finite.

Every automorphism preserves all logical formulas by induction on their construction, so an automorphism taking $\vec{a}$ to $\vec{b}$ necessarily gives equal partial types.

For the converse, first note that a finite first-order structure is atomic by (ii). Thus in both cases every realized finite-tuple partial type has an isolating logical formula. Suppose two finite tuples $\vec{u},\vec{v}$ have the same complete type, and choose a new element $x$ to extend the first tuple. Let $\theta (\vec{z},w)$ isolate the realized partial type of $(\vec{u},x)$. Sincelogical equality of partial types gives $\mathcal{A}\models \exists w\theta (\vec{v},w)$. Choose a witness $y$. Isolation ensures $(\vec{u},x)$ and $(\vec{v},y)$ have the same complete type. In particular, if $x$ is distinct from the entries already used, their inequality logical formulas ensure $y$ is distinct from its corresponding entries. The resulting finite map is injective and partial elementary.

Start from $\vec{a}\mapsto \vec{b}$, which is well-defined even for repeated coordinates because their logical equality patterns agree. Enumerate the carrier and extend alternately to include the next missing element in the domain and the next missing element in the range. For a range step apply the same extension argument to the inverse finite map. The union is an elementary bijection from $A$ onto itself: every finite tuple and every logical formula involving it is handled at some stage. It is therefore an automorphism taking $\vec{a}$ to $\vec{b}$. In the finite case the construction terminates once all elements have been included.

HenceCountability makes the back-and-forth numeralwise enumeration in arithmetic exhaust the entire first-order structure; it cannot simply be dropped.

Use the first-order language with one equivalence relation $E$. Let $\mathcal{A}$ have exactly two equivalence classes, one countably infinite and one uncountable, with no further first-order structure. Its complete theory says that there are exactly two classes and both are infinite.

This first-order theory has quantifier elimination. To eliminate one existential logical variable from a conjunction of atomic formulas and negated atomic formulas, a logical equality either fixes its value, or finitely many inequalities exclude finitely many points. Its required equivalence-class membership is determined by the finitely many existing classes represented among the parameters. A required unused class exists exactly when fewer than two classes have already been used. Once its class is possible, infinitude supplies a point avoiding the finite exclusions. These tests are quantifier-free logical equality and equivalence conditions on the parameters. Disjunctive normal form and induction eliminate all quantifiers and also show completeness.

Thus a finite tuple's complete type is isolated by its finite equality-and-equivalence pattern. Every realized finite-tuple partial type is principal, so $\mathcal{A}$ is atomic. In particular all individual elements have the same complete one-type, isolated by $x=x$.

Choose $a$ in the countable class and $b$ in the uncountable class. Any automorphism taking $a$ to $b$ would give a bijection from their whole equivalence classes, impossible because their cardinalities differ. ThereforeIts uncountability is precisely what avoids the conclusion of (iii).

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.