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

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).