Past exam of the mathematics course of the University of Cambridge / 2024 / iii / Paper 120 (Model Theory and Non-Classical Logic)

Expand $L$ to $L(M)$ by a constant $c_m$ for each $m\in M$. The diagram of a structure $\mathrm{Diag}(M)$ contains all atomic and negated atomic $L(M)$-sentences true in $M$. The elementary diagram $\mathrm{ElDiag}(M)$ contains every $L(M)$-sentence true in $M$.

The method of diagrams combines one of these sets with another theory and applies the compactness theorem. A model of $\mathrm{Diag}(M)$ yields an embedding of $M$ by $m\mapsto c_m$, while a model of $\mathrm{ElDiag}(M)$ yields an elementary embedding.

On $A={\bigcup }_i{A}_i$, interpret a constant at its common value, a function on a tuple by choosing one $A_i$ containing the tuple, and a relation similarly. Total ordering of the indices and compatibility of substructures make these definitions independent of the chosen stage. Every $A_i$ is then a substructure of $A$.

For an elementary chain, induction on formulas provesThe atomic step follows from the induced structure, Boolean steps are immediate, and for an existential formula any witness in the union lies in a later $A_j$ containing the parameters; elementarity between $A_i$ and $A_j$ moves existence back to $A_i$. This is the elementary chain theorem.

A sentence $\forall \bar{x}\exists \bar{y}\phi (\bar{x},\bar{y})$ with quantifier-free $\phi$ is preserved by a union of an embedding chain: a tuple $\bar{a}$ occurs at some stage, a witness $\bar{b}$ exists at that stage, and quantifier-free formulas are preserved in the union. Thus every forall-exists axiomatized theory is inductive.

Conversely, let $T_0$ contain all forall-exists consequences of $T$ and suppose $M\models T_0$. The diagram-and-compactness sandwich lemma says that one can constructwhere every $N_i\models T$ and every $M_i\preccurlyeq M_{i+1}$. For completeness, the first extension is obtained by adding to $T$ the diagram of $M_i$ together with all universal formulas over $M_i$ true there. A finite inconsistency would give a forall-exists consequence of $T$ false in $M_i$. The resulting extension embeds into an elementary extension $M_{i+1}$ by the method of diagrams.

The $N_i$ form an embedding chain and have the same union $N$ as the $M_i$. By the assumed preservation, $N\models T$; by the elementary chain theorem, $M\preccurlyeq N$. Hence $M\models T$, so $T_0\models T$. The two theories are equivalent, proving the characterization.

A model-complete theory is one for which every embedding between models is elementary. If $(M_i)$ is an embedding chain of models, all transition embeddings are therefore elementary. The elementary chain theorem shows that the union is a model elementarily extending every $M_i$, so the theory is preserved under unions of embedding chains. Part (c) then gives an axiomatization by forall-exists sentences.

A complete $n$-type over $X\subseteq M$ is a maximal set $p(\bar{x})$ of $L(X)$-formulas consistent with the theory of $M$ with parameters from $X$. Equivalently, for every formula $\phi (\bar{x})$, exactly one of $\phi ,\neg \phi$ belongs to $p$.

The type space $S_n^M(X)$ has these types as points and basic open setsSince $[\phi {]}^c=[\neg \phi ]$, these sets are clopen. An isolated type is a point $\{p\}=[\phi ]$ for some formula $\phi \in p$.

Add new constants $\bar{c}$ and considerEvery finite subset is satisfiable because $p$ is consistent over $M$. By the compactness theorem it has a model $N^{\prime }$. The constants naming $M$ give an elementary embedding $M\to N^{\prime }$, and ${\bar{c}}^{N^{\prime }}$ realizes $p$. Replacing $N^{\prime }$ by an isomorphic copy containing $M$ gives the required realization of a type in an elementary extension.

If $p\ne q$, completeness gives a formula $\phi$ with $\phi \in p$ and $\neg \phi \in q$. Thenand these two disjoint open sets cover $S_n^M(X)$. This proves the total disconnectedness of a type space.

Write the Ehrenfeucht-Mostowski model as the Skolem hull of its order-indiscernible skeleton $(a_i{)}_{i\in \eta }$. Every element is $t(a_{i_1},\dots ,a_{i_r})$ for a Skolem term $t$. Choose supports for the elements of $X$ and let $J\subseteq \eta$ be their union. Then

When $\eta$ is well ordered, the type over $X$ of $t(a_{i_1},\dots ,a_{i_r})$ is determined by $t$ and the finite order pattern of the indices $i_k$ relative to $J$. There are at most $|L|$ terms and at most $|J|$ such finite patterns. Therefore the number of realized complete one-types is at most

Assume $M$ is a prime model. By the downward Lowenheim-Skolem theorem, $T$ has a countable model, and the elementary embedding of $M$ into it makes $M$ countable. If a tuple $\bar{a}\in M$ had a nonisolated type, the omitting types theorem would give a countable model of $T$ omitting that type. An elementary embedding of $M$ into this model would realize it, a contradiction. Thus $M$ is atomic.

Conversely, let $M$ be countable and atomic, enumerate it as $(a_i{)}_{i<\omega }$, and let $N\models T$. Construct an elementary embedding recursively. Suppose $a_0,\dots ,a_{n-1}$ have been mapped to $\bar{b}$. Let $\psi (\bar{x})$ isolate the type of $(a_0,\dots ,a_{n-1})$ and let $\theta (\bar{x},y)$ isolate the type of $(a_0,\dots ,a_n)$. Since the latter extends the former and is realized in $M$, completeness givesThe tuple $\bar{b}$ realizes $\psi$, so a suitable image of $a_n$ exists in $N$. The union of the finite partial elementary maps is an elementary embedding $M\to N$. Hence $M$ is prime.

Let $M$ be a prime model and let $[\phi ]\subseteq S_n(T)$ be a nonempty basic open set. Some model of $T$ realizes $\phi$, so completeness of $T$ givesTherefore $M$ realizes $\phi$ by some tuple $\bar{a}$. The prime-model characterization in part (e) says ${\mathrm{tp}}^M(\bar{a}/\varnothing )$ is isolated, and it lies in $[\phi ]$. Every nonempty basic open set thus contains an isolated point, proving density of isolated types from a prime model.

Under the Implicational Curry-Howard correspondence, propositions are simple types and assumptions are typed variables. The natural-deduction rulescorrespond respectively to the typing rulesAn assumption $x:A$ corresponds to the variable rule. Induction on a proof converts each rule into the matching typing construction; induction on a typing derivation reverses the process. Thus derivability of an implicational formula from assumptions is equivalent to inhabitation of its corresponding type.

By part (a), such a term would provein intuitionistic propositional logic. Consider the two-world Kripke model for intuitionistic propositional logic $r<s$. Let $\sigma$ hold only at $s$ and let $\tau$ hold nowhere. At both worlds $\sigma \to \tau$ fails, so $(\sigma \to \tau )\to \sigma$ holds at $r$ vacuously, while $\sigma$ does not hold at $r$. The displayed formula therefore fails at $r$. By the Kripke completeness theorem for intuitionistic propositional logic, it is not derivable, so no simply typed lambda term inhabits that type.

No such first-order theory exists. Suppose $T$ axiomatized the Heyting algebras having only finitely many regular elements. Expand the language by constants $c_n$ and addEvery finite subset has a model: take a sufficiently large finite Boolean algebra, in which every element is regular. By the compactness theorem, the entire expanded theory has a model. Its reduct is a model of $T$ with infinitely many distinct regular elements, contradicting the proposed axiomatization.