Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2008 (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 a complete editable six-page transcription. Bounded official-source searches found no advertised solutions to this exact paper. All 37 source leaves are answered below. The solutions state the proof-numbering convention in A2(d), the naming convention for diagram inclusions in B6(ii), and the literal printed stability definition in B8(ii)(e).

An arithmetic logical formula is ${\Sigma }_0$, or bounded, if all its quantifiers are bounded by arithmetical first-order terms. A ${\Sigma }_1$ logical formula has an initial block of existential quantifiers followed by a bounded matrix, up to the usual logical transformations. Soundness of an arithmetic theory at a given level means that every first-order sentence of that level proved by the first-order theory is true in the standard natural numbers. Here ${\Sigma }_0$-completeness means that every true bounded arithmetic sentence is provable.

A first-order theory is one-consistent if there is no bounded arithmetic formula $A(x)$ for which it proves $\exists xA(x)$ while proving $\neg A(\bar{n})$ for every standard natural number $n$. This is a restricted form of omega-consistency. In particular one-consistency implies first-order consistency, since an inconsistent first-order theory proves every first-order sentence and its negation.

Suppose a ${\Sigma }_0$-complete first-order theory $S$ is first-order consistent. If it proved a false bounded arithmetic sentence $\theta$, the true bounded arithmetic sentence $\neg \theta$ would also be provable by completeness, contradicting first-order consistency. Thus $S$ is ${\Sigma }_0$-sound. Conversely ${\Sigma }_0$-soundness excludes inconsistency because an inconsistent first-order theory proves the false bounded arithmetic sentence $0=1$. ThereforeIf $S$ is one-consistent but proved a false existential sentence $\exists xA(x)$ with bounded matrix, every standard instance $\neg A(\bar{n})$ would be true and hence provable. This violates one-consistency. Thus it is ${\Sigma }_1$-sound. Conversely, ${\Sigma }_1$-soundness implies first-order consistency by the previous argument, since bounded arithmetic sentences are included at the existential level. If $S$ proved $\exists xA(x)$, soundness of an arithmetic theory would give a standard witness $n$ with $A(n)$ true. Bounded completeness of an arithmetic theory would then give $S⊢A(\bar{n})$, so first-order consistency prevents simultaneous formal proofs of all the negated instances. HenceMultiple existential logical variables can be treated as a finite tuple of witnesses; the same reasoning applies.

The definition of $a$ makes the diagonal instance $E_a[\bar{a}]$ exactly $G_S$. The representing logical formula therefore has the standard interpretationIf $S⊢G_S$, choose an actual witness $m$ to the left-hand existential statement. The bounded arithmetic sentence $A(\bar{a},\bar{m})$ is true and hence provable by ${\Sigma }_0$-completeness. But $G_S$ also gives $S⊢\neg A(\bar{a},\bar{m})$, a contradiction. ThusNow assume one-consistency. It implies first-order consistency, so no formal proof of $G_S$ exists and $A(a,m)$ is false for each standard $m$. Each bounded arithmetic sentence $\neg A(\bar{a},\bar{m})$ is consequently true and provable. A formal proof of $\neg G_S$ would give a formal proof of $\exists v_{2}A(\bar{a},v_2)$ while every standard witness instance is refuted, contrary to one-consistency. HenceThe two hypotheses play different roles: ordinary first-order consistency excludes the positive Gödel sentence, while the stronger hypothesis also excludes its negation.

By the standard interpretation of the representing logical formula,If $S$ is first-order consistent, part (b) supplies the right-hand side, so $G_S$ is true. If $S$ is inconsistent, explosion gives $S⊢G_S$, so the representing existential statement is true and $G_S$ is false. ThereforeThis is an external truth assertion about the standard natural numbers. Formalizing that assertion inside a first-order theory requires the additional facts explicitly supplied in part (d).

Put $T=S\cup \{\neg G_S\}$. The first supplied equivalence, retained in $T$, combines with its new axiom to giveThe supplied implication $\mathrm{Con}(T)\to \mathrm{Con}(S)$ then yields, by contraposition,Finally the second supplied equivalence is $T⊢G_T\leftrightarrow \mathrm{Con}(T)$, so propositional reasoning givesNo extra first-order consistency assumption is needed for this formal derivation. If $S$ is first-order consistent, part (b) shows that adding $\neg G_S$ preserves first-order consistency, because inconsistency of the extension would imply $S⊢G_S$. Such a first-order consistent extension therefore proves the negation of its own true Gödel sentence, illustrating why first-order consistency alone does not imply one-consistency.

Write $\rho ={\mathrm{Pr}}_{PA}^{\ast }(┌R┐)$. The supplied fixed-point equivalence gives $PA⊢R\leftrightarrow \neg \rho$.

If PA proved $R$, the first assumed property would give $PA⊢\rho$, while the equivalence would give $PA⊢\neg \rho$. This contradicts first-order consistency. If PA proved $\neg R$, the second assumed property would give $PA⊢\neg \rho$, and the reverse implication of the equivalence would give $PA⊢R$, again a contradiction. HenceThis is the Rosser improvement: its comparison of formal proof codes permits ordinary first-order consistency to exclude both alternatives, without assuming one-consistency.

If PA is inconsistent, every desired conclusion is already a theorem, so it suffices to analyze the first-order consistent case. Use $Q(u,v)$ for the bounded arithmetical proof relation and $\mathrm{neg}(u)$ for the code of the negation of the logical formula coded by $u$.

Suppose $PA⊢E_n$ and let $m$ be the code of an actual formal proof. By first-order consistency there is no formal proof of $\neg E_n$, in particular none with code at most $m$. Thusis a true bounded arithmetic sentence. Bounded completeness of an arithmetic theory proves it in PA, and existential introduction gives $PA⊢{\mathrm{Pr}}_{PA}^{\ast }(\bar{n})$.

Conversely suppose $PA⊢\neg E_n$ and choose an actual formal proof code $k$ of that negation. First-order consistency excludes every formal proof of $E_n$, so each of the finitely many statements $\neg Q(\bar{n},\bar{j})$ for $j<k$ is true and provable. The supplied finite-case theorem permits PA to combine them into the assertion that no formal proof code below $k$ proves $E_n$.

PA also proves $Q(\overline{\mathrm{neg}(n)},\bar{k})$. For any candidate formal proof code $v\ge \bar{k}$, this one code already refutes the universal no-earlier-negation condition in the Rosser predicate symbol. For $v<\bar{k}$, the finite verification refutes its positive formal proof condition. The supplied order dichotomy and finite-case expansion cover all $v$. ThereforeThe argument uses bounded verification of a finite initial segment and one fixed counter-witness beyond it; it does not infer that PA proves the absence of all ordinary formal proofs merely from first-order consistency.

If PA is first-order consistent and already proves $\neg X$, it cannot also prove $X$. By the correctness of the ordinary arithmetized arithmetical proof relation, $\mathbb{N}\models \neg {\mathrm{Pr}}_{PA}(┌X┐)$.

If PA is inconsistent, it proves $X$ by explosion, so an actual formal proof code witnesses ${\mathrm{Pr}}_{PA}(┌X┐)$ in the standard natural numbers. ThusThe hypothesis that $X$ is refutable is essential to this first-order consistency characterization for an arbitrary fixed first-order sentence.

Let $C$ denote the addition-commutativity first-order sentence and put $d=┌\neg C┐$. In the ordinary checker for PA derivations, replace the axiom test ${\mathrm{Ax}}_{PA}(u)$ byKeep all tests for sequence formation, earlier lines, logical axiom schemes and inference rules unchanged. This gives a formal proof checker $Q_S(u,w)$ which recognizes exactly ordinary $S$-derivations. The finite syntactic modification is arithmetizable by the same bounded coding apparatus as the original checker.

For the proof-order comparison in the next part, make the choice of coding explicit. Reserve code $0$ for the one-line derivation of the newly added axiom $\neg C$, and give an ordinary derivation with code $w$ the new code $w+1$. A corresponding bounded relation isEvery code has a specified decoding, every genuine formal proof is represented, and no false formal proof is admitted. The reserved code duplicates one genuine derivation, which is harmless. This is one explicit arithmetized arithmetical proof relation obtainable from the PA checker by the requested axiom change and a simple renumbering. Stating the proof-order convention matters because a Rosser predicate symbol uses code order, not merely the existence of formal proofs.

Use the arithmetical proof relation and coding just constructed. A formal proof of $C$ cannot have code $0$, since that code was reserved for $\neg C$. Every candidate code $v$ for a formal proof of $C$ is therefore positive. But code $0\le v$ is already a formal proof of $\neg C$, so the no-earlier-negation condition fails for every candidate. HencePA proves $C$ by induction, while $S$ has $\neg C$ as an added axiom. Thus $S$ is inconsistent and its ordinary arithmetical provability predicate is true of every first-order sentence, including $C$. The displayed negative Rosser assertion can nevertheless be true, because the Rosser condition compares the order of opposite formal proofs rather than asking for their mere existence.

There is an important coding qualification. The PDF refers to a course formal proof coding but does not specify its numerical ordering. The truth of this Rosser assertion for an inconsistent first-order theory is not coding-invariant, so formal proof length alone cannot establish it for an unspecified fixed coding. For example, a different legitimate numbering could reserve code $0$ for a known PA formal proof of $C$, code $1$ for the new axiom $\neg C$, and higher codes for all other derivations. Then code $0$ would witness ${\mathrm{Pr}}_S^{\ast }(┌C┐)$ instead. The explicit allowed construction in part (i) supplies a convention under which the requested assertion holds; interpreting it as a claim about some externally fixed course numbering requires that numbering's corresponding order property.

Use the Hilbert-Bernays-Löb derivability conditions for an arithmetical provability predicate. Abbreviate $P_S(┌A┐)$ by $PA$. The conditions needed below areThese are the usual theoremhood, distribution and positive-introspection conditions intended by a standard arithmetical provability predicate; arbitrary predicate symbols merely agreeing with provability externally need not satisfy them.

Since $S⊢\neg Y$, it proves $Y\to G$. The first two conditions give $S⊢PY\to PG$. For the converse, the fixed-point equivalence gives $S⊢G\to (PG\to Y)$. Applying theoremhood and distribution givesPositive introspection also gives $PG\to PPG$, and distribution combines these to yield $S⊢PG\to PY$. Thus $S⊢PG\leftrightarrow PY$. Combining with $G\leftrightarrow \neg PG$ provesIf $S$ proved $\neg PY$, it would prove $G$. The theoremhood condition would then give $PG$, while the fixed-point equivalence gives $\neg PG$. Therefore first-order consistency implies

Put $T=S\cup \{\neg X\}$ and assume $S⊢P_S(┌X┐)\to X$. In $T$, contraposition against its extra axiom gives $\neg P_S(┌X┐)$.

Classical logic proves $(\neg X\to X)\to X$. By the derivability conditions,Compose this with the supplied formalized deduction implication from $P_T(┌X┐)$ to its left-hand side. Then $T$ provesand thereforeThe other supplied assumption says this is impossible if $T$ is first-order consistent. Thus $T$ is inconsistent. By the deduction theorem, inconsistency after adjoining $\neg X$ yields $S⊢\neg \neg X$, henceThis establishes Löb's inference rule using precisely the strengthened unprovability assumption and the formalized deduction property supplied in the question.

Take a first-order sentence $Y$ refutable in $S$ and suppose, toward contradiction, that a first-order consistent $S$ proved $\neg P_S(┌Y┐)$. Propositional logic would then giveLöb's inference, applied with $X=Y$, would give $S⊢Y$, contradicting the existing formal proof of $\neg Y$. Hence first-order consistency excludes the proposed formal proof of non-provability.

Thus the familiar unprovability of the first-order consistency statement associated with a refutable first-order sentence is a special consequence of the general ruleThe general rule applies to every first-order sentence, not just a chosen false or refutable one.

Let $j=i+n$ with $n\ge 1$. Positive introspection supplies the theorem $F_k\to F_{k+1}$ for every $k\ge 1$, since $F_k$ itself has the form $P_S(┌F_{k-1}┐)$.

Induction on $n$ consequently givesAt $n=1$ this is the identity implication. To pass from $n$ to $n+1$, compose the induction hypothesis with the positive-introspection implication at $k=i+n$, which is at least one. Composing the result with the assumed $F_j\to F_i$ givesi.e. $S⊢P_S(┌F_i┐)\to F_i$. Löb's rule now yieldsThe index restriction on positive introspection has been respected even when $i=0$: the chain begins at $F_{i+1}$, which already is a provability assertion.

The source's system called $K$ already contains positive introspection, so its displayed axioms are those usually called $K4$. PutWe first show that its axioms prove $\square A\to A$, the implication suggested in the hint. From $B$, positive introspection gives $\square B$. Distribution applied to $\square A=\square (B\to \square X)$ and $\square B$ gives $\square \square X$. Distribution applied to $B=\square (\square X\to X)$ and this last result gives $\square X$. Thus the theorem-level implications combine by propositional reasoning intowhich is $K4⊢\square A\to A$.

Since $S$ contains these axioms, it proves that implication. Its assumed Löb inference rule, applied to the first-order sentence $A$, yields $S⊢A$. Unpacking $A$ provesThis uses necessitation only as part of the ordinary modal theorem rules; no inference of a boxed temporary assumption has been made.

Let $C=\square X\wedge X$. The normal distribution axiom and necessitation of $C\to X$ give $\square C\to \square X$. Combining this with propositional reasoning yields the theoremIndeed, $X$ together with $\square C$ supplies both conjuncts of $C$. Necessitate this theorem and apply distribution to obtainThe new Löb axiom at $C$ now gives $\square X\to \square C$. Finally, necessitation and distribution applied to the tautology $C\to \square X$ give $\square C\to \square \square X$. Composition provesNo positive-introspection instance was used in deriving it. The argument shows why that scheme can be dropped when the Löb scheme is added.

Set $Y=\square X\to X$. The Löb axiom at $X$ is $\square Y\to \square X$. Therefore $Y$ and $\square Y$ together imply $X$, provingFor the converse, the tautology $X\to Y$ gives $\square X\to \square Y$ by necessitation and distribution. Consequently $\square Y\to X$ together with $\square X$ gives $X$, sowhose consequent is $Y$. Combining both directions gives an unboxed equivalence as a theorem of GL. Necessitation then yields exactly

Under the arithmetical interpretation $\square A=P_S(┌A┐)$, the Löb axiom says that a formal proof of the local reflection implication for $A$ already entails a formal proof of $A$:It is a formalized constraint on self-verification of a formal proof system. Externally, Löb's theorem says that if the system itself proves its own local reflection implication for $A$, it proves $A$. Distribution reflects closure of formal proofs under implication, necessitation reflects that a theorem has an arithmetically recognizable formal proof, and positive introspection reflects formal proof verification inside arithmetic.

Taking $A$ to be a refutable first-order sentence, especially a contradiction, recovers the obstruction behind the second incompleteness theorem: a first-order consistent sufficiently strong system cannot prove the corresponding claim that no formal proof of that first-order sentence exists. This does not identify provability with truth, nor grant the unrestricted factivity principle $\square A\to A$ as a theorem of the system. The Löb axiom is the characteristic additional scheme of Gödel–Löb provability logic.

An $L$-structure has a nonempty underlying set $A$. It assigns to each constant symbol $c_k$ an element $c_k^{\mathcal{A}}\in A$, to each $n$-ary function symbol $f_j$ a function $A^n\to A$, and to each $n$-ary predicate symbol $P_i$ a relation contained in $A^n$. Logical equality, when included as logical equality, is interpreted as actual identity.

The arities belong to the specification of the first-order language. An assignment of logical variables to elements of $A$ then evaluates first-order terms recursively and determines satisfaction of logical formulas through the logical connectives and quantifiers. A first-order sentence has no free variables, so its truth in the first-order structure is independent of the assignment.

The set $\Sigma$ is satisfiable if there is one $L$-structure $\mathcal{A}$ satisfying every first-order sentence in $\Sigma$ simultaneously. It is finitely satisfiable if each finite subset ${\Sigma }_0\subseteq \Sigma$ has a first-order model; that first-order model is allowed to depend on the chosen finite subset.

Thus the two statements have different quantifier orders:Satisfiability immediately implies finite satisfiability by using the same first-order structure for every finite subset. The converse is the substantive content of compactness theorem.

The compactness theorem states that a set of first-order sentences has a first-order model if and only if every finite subset has a first-order model.

For the nontrivial direction suppose every finite subset of $\Sigma$ is satisfiable. If $\Sigma$ were inconsistent, a finite formal derivation of a contradiction would use only finitely many premises ${\Sigma }_0\subseteq \Sigma$. Soundness of an arithmetic theory would then exclude a first-order model of ${\Sigma }_0$, contradicting finite satisfiability. Therefore $\Sigma$ is first-order consistent. The completeness theorem, proved by adjoining witnesses and constructing a Henkin term model, supplies a first-order model of $\Sigma$.

The reverse direction is immediate by restriction of the list of required first-order sentences. The key reason compactness theorem follows from syntactic completeness is that every formal proof uses only finitely many premises, even when the whole first-order theory is infinite.

Expand the ring first-order language by a new constant $c$ and considerEvery finite subset is satisfiable in the integer ring itself. Only finitely many divisibility conditions occur; interpret $c$ as a nonzero common multiple of their positive integer indices, using $1$ if none occur. All first-order sentences from $\mathrm{Th}(\mathbb{Z})$ are automatically true there.

Compactness theorem therefore gives a first-order model. Its reduct $R$ to the original ring first-order language satisfies the complete theory of $\mathbb{Z}$, so $R\equiv \mathbb{Z}$. Its element $c^R$ is nonzero and divisible by every positive standard integer. ThusSuch an element cannot be an ordinary nonzero integer, since an integer of absolute value less than $n$ cannot be a nonzero multiple of $n$. The statement concerns each standard integer index separately; it does not assert divisibility by every internally nonzero element of $R$.

Let $L_A$ expand $L$ by a constant $c_a$ for each $a\in A$, and let ${\mathcal{A}}_A$ be the canonical expansion interpreting $c_a$ as $a$. Its diagram of a structure is the set of all atomic and negated atomic $L_A$-sentences true in ${\mathcal{A}}_A$. Its elementary diagram is the set of all $L_A$-sentences true there:A substructure inclusion $\mathcal{A}\subseteq \mathcal{B}$ means that $A\subseteq B$, constants have the same interpretations, the operations of $\mathcal{B}$ restrict to those of $\mathcal{A}$, and each relation restricts to the corresponding relation on $A$.

An elementary substructure additionally preserves the truth of every logical formula with parameters from $A$:Here the right-hand condition includes the substructure requirements by applying it to atomic logical formulas and their negations.

If $\mathcal{A}\subseteq \mathcal{B}$, interpret each new constant $c_a$ in $\mathcal{B}$ as the same element $a$. Atomic logical formulas and their negations then have exactly their truth values in ${\mathcal{A}}_A$, so the expansion satisfies the diagram of a structure. If the inclusion is elementary, every logical formula with those named parameters has the same truth value, so the expansion satisfies the elementary diagram.

Conversely, from any expansion ${\mathcal{B}}^{+}$ satisfying the diagram of a structure defineThe diagram of a structure contains $c_a\ne c_{a^{\prime }}$ whenever $a\ne a^{\prime }$, so $e$ is injective. It contains every true function-value equation, so $e$ commutes with all operations and constants. Positive and negative relation instances ensure both preservation and reflection of the relations. Thus $e$ is an embedding of first-order structures. If the expansion satisfies the elementary diagram, for every logical formula $\varphi$ and tuple $\vec{a}$ it also givesso $e$ is an elementary embedding of first-order structures.

The precise conclusion for an arbitrary expansion is an embedding of first-order structures, rather than a literal inclusion of the original carriers. The source's inclusion notation is correct when one uses the customary identification of $\mathcal{A}$ with its embedded copy, or requires the expansion to interpret $c_a$ as the actual element $a$ of a carrier already containing $A$. With that naming convention, $e$ is the inclusion and the requested two equivalences follow exactly.

Without the convention the literal wording fails, even in the first-order language of logical equality: singleton first-order structures with carriers $\{0\}$ and $\{1\}$ have a diagram-satisfying expansion by sending the first first-order structure's named point to $1$, but the first carrier is not a subset of the second. The embedding of first-order structures formulation proved above states the invariant result and makes the intended inclusion formulation precise.

The Downward Lowenheim-Skolem theorem says that for an $L$-structure $M$ and a subset $S\subseteq M$, there is an elementary substructure $N\preccurlyeq M$ containing $S$ withIf an infinite cardinal $\kappa$ satisfies $\max (|L|,{\aleph }_0)\le \kappa \le |M|$, one can in particular obtain size exactly $\kappa$ by starting with a subset of that size.

Choose a default element $a_0\in M$. For every logical formula $\exists x\varphi (x,\vec{y})$ choose a Skolem function $F_{\varphi }$ which returns a witness in $M$ when one exists, and returns $a_0$ otherwise. Begin with $S$, the interpretations of the first-order language's constants, and $a_0$. Successively adjoin the values of all the original functions and these Skolem functions on finite tuples already chosen. Let $N$ be the union of the resulting countable sequence of closure stages.

There are at most $\max (|L|,{\aleph }_0)$ logical formulas, and each function has finite arity. With $\kappa =\max (|S|,|L|,{\aleph }_0)$, each closure stage has size at most $\kappa$, and so does their countable union. Closure under the original functions makes $N$ an $L$-substructure. Whenever $M\models \exists x\varphi (x,\vec{a})$ for parameters in $N$, its chosen Skolem witness belongs to $N$, since the finitely many parameters lie in some common stage. The Tarski–Vaught test therefore gives $N\preccurlyeq M$.

For the exact-cardinality version, choose an initial set of $\kappa$ elements, enlarged to contain any prescribed subset of size at most $\kappa$. The construction gives an upper bound $\kappa$ while containment gives the matching lower bound.

Add a predicate symbol $P_{\theta }$ for each $L$-formula $\theta (\vec{x})$, of arity equal to its displayed free-variable tuple. Let $T^{+}$ consist of $T$ together with all defining axiomsEvery first-order model of $T$ has a unique such expansion, interpreting the new predicate symbols by their defining sets. Conversely the reduct of every first-order model of $T^{+}$ satisfies $T$.

Given an arbitrary $L^{+}$-formula $\psi (\vec{x})$, replace each new atomic predicate symbol by its original $L$-definition, renaming bound variables to avoid capture. This produces an $L$-formula ${\psi }^{-}(\vec{x})$ withThe defining axiom for that particular logical formula now gives an atomic replacement:Thus the expanded first-order theory eliminates quantifiers. For a first-order sentence, the same translation is an $L$-sentence, decided by completeness of $T$; hence every expanded first-order sentence is decided and $T^{+}$ is complete. Empty free-variable tuples can be handled by zero-ary predicate symbols, or by the usual logical truth and falsity constants. This definitional expansion is called Morleyization.

Prime elements are first-order definable in the ring first-order language. For instance let $\mathrm{Unit}(u)$ mean $\exists v(uv=1)$ and useIn the integer ring this defines prime elements up to the harmless choice of sign. Expand the first-order language by names for every integer and a new constant $c$. Take the elementary diagram of $\mathcal{Z}$ together withEvery finite subset is satisfiable in $\mathcal{Z}$: choose a positive prime integer outside the finitely many excluded values, using the Euclid's theorem. Compactness theorem gives a first-order model of the entire set. The complete-diagram argument embeds $\mathcal{Z}$ elementarily into its reduct; identify that copy with the original integer ring.

The resulting elementary extension contains $c$, a prime element unequal to every named standard integer. ThereforeThe construction rules out all standard integers, not merely the finite list appearing in any one approximation.

Apply downward Löwenheim-Skolem to the extension from part (i), keeping all standard integers and the new prime $c$. The first-order language and this prescribed subset are countable, so there is a countable elementary substructure $N$ containing them. In particular $N\equiv \mathcal{Z}$ and contains an element outside the standard copy of $\mathbb{Z}$.

No ring isomorphism $N\to \mathcal{Z}$ can exist. Such an isomorphism fixes $0$ and $1$, hence every nonnegative integer numeral. It also fixes each negative integer, which is the unique solution of $x+\bar{n}=0$ for the corresponding positive $n$. Consequently it fixes the whole standard copy. The image of $c$ would be some standard integer $a$, already the image of that same named standard element, violating injectivity.

Thus $N$ and $\mathcal{Z}$ are two nonisomorphic countably infinite first-order models of $T$, so

Every integer is definable without parameters in the ring first-order language. For $a\ge 0$, use $x=\bar{a}$; for $a=-m<0$, use $x+\bar{m}=0$. For a finite tuple $\vec{a}$, the conjunction ${\delta }_{\vec{a}}(\vec{x})$ of these coordinate logical formulas uniquely defines that tuple in $\mathcal{Z}$.

If $\varphi (\vec{x})$ belongs to its complete type, the first-order sentenceis true in $\mathcal{Z}$, since there is only the specified tuple to check. It therefore belongs to $T=\mathrm{Th}(\mathcal{Z})$. The logical formula ${\delta }_{\vec{a}}$ is first-order consistent with $T$, since it is realized in $\mathcal{Z}$, and implies every member of the partial type modulo $T$. Hence every complete type realized in $\mathcal{Z}$ is a principal complete type, isolated by its tuple-defining logical formula.

Take the parameter-free complete typeof the nonstandard prime constructed in part (i). It is first-order consistent and complete because it consists of exactly the logical formulas true of an actual element in a first-order model of $T$. It contains $x\ne \bar{a}$ for every integer $a$, and consequently no element of $\mathcal{Z}$ realizes it. ThusIt is necessarily a nonprincipal complete type. If a first-order consistent logical formula isolated it, completeness of $T$ would force the existential closure of that logical formula to hold in every first-order model of $T$, including $\mathcal{Z}$; a witness there would realize the partial type, a contradiction. This connects the explicit omission with the hypothesis of the omitting types theorem.

Enumerate the standard positive primes as $(p_n{)}_{n<\omega }$. For each subset $A\subseteq \omega$ consider the partial typewhere divisibility is the ring logical formula $\exists y({\bar{p}}_{n}y=x)$.

Every finite subset is realized in $\mathbb{Z}$: take the product of the finitely many primes required to divide $x$, or $1$ if there are none. This is nonzero and is not divisible by any of the distinct finitely many primes required not to divide it. Compactness theorem supplies a complete type extending $q_A$.

Distinct subsets $A,B$ yield distinct complete extensions, because at an index in their symmetric difference they require opposite divisibility statements. There are $2^{{\aleph }_0}$ such subsets, so there are at least that many complete one-types. There are at most that many because the first-order language has only countably many logical formulas and a partial type is a set of them. HenceIn particular the number of complete one-types is uncountable, despite every partial type realized in the particular countable first-order model $\mathcal{Z}$ being a principal complete type.

The Ryll-Nardzewski theorem says that for a complete theory $T$ in a countable first-order language with infinite first-order models, the following are equivalent: $T$ is ${\aleph }_0$-categorical; for every positive integer $n$, the set $S_n(T)$ of complete parameter-free $n$-types is finite; every such finite-arity complete type is isolated by a logical formula. The countable-language hypothesis and the requirement for every finite arity are important.

The omitting types theorem says that, for a first-order consistent complete theory in a countable first-order language, a countable family of nonprincipal partial types in finite tuples of logical variables can all be omitted in a countable first-order model. Here nonprincipal means that no logical formula first-order consistent with the first-order theory implies every logical formula of the partial type. Omission means that no tuple in the constructed first-order model satisfies all logical formulas of that partial type. The complete one-type version is the special case of one partial type in one logical variable.

Use the complete theory of dense linear orders without endpoints in the first-order language $\{<\}$. It eliminates quantifiers: existential conditions on one new point reduce to finitely many logical equality constraints and interval bounds, and density and absence of endpoints decide whether a suitable point exists. Its countably infinite first-order models are all isomorphic to the rational order by the usual back-and-forth method, extending finite order-preserving maps alternately along enumerations of the two first-order models. Thus it is ${\aleph }_0$-categorical.

To distinguish first-order models of size ${\aleph }_1$, letwith ordered sums. Both are dense without endpoints and have cardinality ${\aleph }_1$. The first has cofinality ${\aleph }_1$: countably many points lie in a bounded set of block indices and cannot be cofinal. The second has cofinality ${\aleph }_0$, supplied by its final rational block. Cofinality of a linear order is preserved by isomorphism, so they are not isomorphic. ThereforeFor Ryll-Nardzewski, its $n$-types are precisely the finitely many equality-and-order patterns on $n$ coordinates. Each is isolated by the conjunction specifying that pattern, agreeing with the theorem's prediction.

Use $AC{F}_0$, the complete theory of algebraically closed fields of characteristic zero. Its quantifier elimination is a standard characterization of this complete theory. Algebraically closed fields of a fixed characteristic are classified up to isomorphism by transcendence degree over their prime field.

For such a field $K$,when the transcendence degree is infinite, while finite transcendence degree also gives a countable field. This follows by counting rational functions in a transcendence basis and then algebraic elements over that field. Thus every first-order model of cardinality ${\aleph }_1$ has transcendence degree ${\aleph }_1$, and the classification gives a unique such first-order model.

On the other hand $\overline{\mathbb{Q}}$ and an algebraic closure of $\mathbb{Q}(t)$ are countably infinite first-order models with transcendence degrees zero and one, so are not isomorphic. HenceThe transcendental complete one-type consists of $f(x)\ne 0$ for every nonzero polynomial over $\mathbb{Q}$. Quantifier elimination makes it complete. It is nonprincipal: any parameter-free one-variable logical formula containing a transcendental element defines a cofinite set, hence contains algebraic elements as well and cannot isolate this partial type. The first-order model $\overline{\mathbb{Q}}$ omits it, concretely illustrating the omitting types theorem. The existence of infinitely many algebraic complete one-types, together with this nonprincipal complete type, also agrees with the failure of the Ryll-Nardzewski finiteness condition.

Take the first-order theory of an infinite set in the first-order language of logical equality alone, with an axiom asserting at least $n$ distinct elements for each positive integer $n$. It is complete and eliminates quantifiers: a new logical variable either equals a specified old logical variable or is required to avoid only finitely many existing values, which an infinite domain permits.

For every infinite cardinal $\kappa$, any two first-order models of size $\kappa$ are isomorphic because every bijection between their underlying sets preserves logical equality, the whole first-order language. ThusIts complete $n$-types record only the partition of coordinate indices according to logical equality. There are finitely many such partitions, and each is isolated by the corresponding logical equalities and inequalities. Ryll-Nardzewski therefore recovers countable categoricity; there are no nonprincipal complete finite-arity partial types to omit in this example.

The same complete theory $T_{\infty }$ of an infinite pure set provides this property directly. For $n$ logical variables, each complete type specifies exactly which logical variables are equal. First-order consistency requires an equivalence relation on the finite index set, and infinitude ensures every such partition is realizable. Hencewhere $B_n$ is the $n$th Bell number, counting partitions of an $n$-element set. For example the first values are $B_1=1$, $B_2=2$ and $B_3=5$. The isolating conjunction lists logical equality within blocks and inequality between blocks. This explicitly verifies the hypothesis which Ryll-Nardzewski identifies with ${\aleph }_0$-categoricity.

Use the first-order theory $T_{\mathbb{Z}}$ of a bijection $f$ with named inverse $g$ and no finite cycles. Its axioms areEvery first-order model is a disjoint union of free two-sided integer orbits. Write $f^k$ for positive powers of $f$ and for powers of $g$ when $k$ is negative.

This first-order theory is complete and eliminates quantifiers. Every first-order term reduces to $f^k(x_i)$, and atomic logical formulas reduce to statements $x_j=f^k(x_i)$. To eliminate an existential logical variable in a conjunction of literals, first remove self-equalities using the no-finite-cycle axioms. If an equation fixes that logical variable as an integer translate of another logical variable, substitute that value. If no such equation remains, only finitely many points are excluded by the remaining inequalities, so some value exists in the infinite domain. Apply this to disjunctive normal form and then induct on logical formulas. The resulting parameter-free first-order sentences are decided, proving completeness.

For each fixed finite $n$, a complete type records a partition of the logical variables into common orbits and finitely many integer offsets within each block. There are countably many possibilities. Countable first-order models with one orbit and with two orbits are not isomorphic, so the first-order theory is not ${\aleph }_0$-categorical.

Thus this example has the source's explicitly defined countable-type property. In fact it also satisfies ordinary omega-stability: over a countable parameter set, an element is either a specified integer translate of a parameter, giving countably many possibilities, or lies in an entirely new orbit, giving one further complete one-type. The same finite-orbit-pattern description handles finite tuples. ThereforeThe source prints the label “$0$-stable”; the construction meets its stated definition as well as the usual stronger omega-stability condition. The difference between countably many and finitely many partial types is exactly why Ryll-Nardzewski does not yield categoricity here.

Reuse the complete free-bijection theory from part (e). Quantifier elimination shows that every one-variable atomic statement is already decided by the no-finite-cycle axioms. Thus there is exactly one complete one-type, isolated by $x=x$.

For two logical variables, each integer $k$ gives a different complete type isolated byThere is also the complete typesaying that the two elements lie in different orbits. These exhaust the possibilities by quantifier elimination. In particularThe last complete type is a nonprincipal complete type. Any logical formula uses only finitely many integer offsets after quantifier elimination; a pair in a single orbit with a sufficiently different offset agrees with a different-orbit pair on those tests. Hence no single logical formula can isolate $p_{\infty }$.

The one-orbit first-order model $(\mathbb{Z},f(n)=n+1,g(n)=n-1)$ omits $p_{\infty }$, while a two-orbit first-order model realizes it. This illustrates the omitting types theorem and shows concretely why finitely many complete one-types alone cannot replace the all-arities condition in Ryll-Nardzewski.