42.02.02 · mathematical-logic / model-theory

The Compactness Theorem and the Method of Diagrams

shipped3 tiersLean: none

Anchor (Master): Marker 2002 *Model Theory: An Introduction* (Springer GTM 217) Ch. 2 (compactness, diagrams, elementary amalgamation, the Łoś-Vaught test, preservation theorems, types); Chang and Keisler 1990 *Model Theory* 3e (North-Holland) Ch. 2-5 (the systematic theory of diagrams, ultraproducts and Łoś's theorem, the Keisler-Shelah isomorphism theorem, the Robinson consistency and Craig interpolation theorems, Beth definability, preservation theorems); Hodges 1993 *Model Theory* (Cambridge) Ch. 5-6, 8-9 (the preservation hierarchy via diagrams, amalgamation and the joint embedding property, interpolation); Robinson 1956 *A result on consistency and its application to the theory of definition* (Indag. Math. 18) and Craig 1957 *Three uses of the Herbrand-Gentzen theorem* (J. Symbolic Logic 22)

Intuition Beginner

The previous unit taught you to compare two worlds: when one sits inside another, and when no statement can tell two worlds apart. This unit answers the next question. How do you build a world that contains exactly the features you want? The tool is compactness, and the trick that aims it is the method of diagrams.

Compactness is a promise about demands. Suppose you have a long, possibly endless list of demands you want a single world to satisfy. The promise says: if every finite handful of those demands can be met by some world, then the whole list can be met by one world at once. You only ever have to check finite handfuls, which you can often do by hand. The full theorem was proved earlier; here it becomes a construction machine.

The method of diagrams is how you load the machine. To force a new world to contain a faithful copy of a world you already have, you give every object in the old world its own private name, then write down every basic fact about those named objects — who is below whom, what adds to what. Any world that believes all of those labelled facts is forced to contain a copy of the old world.

Now you stack on extra demands — "there is a number bigger than all of these" — check that each finite handful is met inside the old world, and let compactness deliver a new world holding both the copy and the intruder. Listing facts, naming objects, checking finite handfuls: that is the whole craft this unit teaches.

Visual Beginner

The picture shows the two moves stacked together. First the diagram plants a faithful copy of the old world; then a list of extra demands forces an intruder, and compactness delivers one world holding both.

   STEP 1 — THE DIAGRAM PLANTS A COPY

   old world: whole numbers, each with its own name
        name(0), name(1), name(2), name(3), ...
   basic facts written down (the diagram):
        name(0) < name(1) ,  name(1) < name(2) ,  name(2) < name(3) , ...
        name(1) + name(1) = name(2) ,  ...

   any world believing ALL these labelled facts
   must contain a faithful copy of the whole numbers.

   STEP 2 — EXTRA DEMANDS FORCE AN INTRUDER

   add one new name  c  and the endless demands:
        c > name(0) ,  c > name(1) ,  c > name(2) , ...

   each finite handful is met inside the old world
   (let c be a big enough ordinary number)

   so compactness gives ONE world with both:

     copy of whole numbers  ............ intruder
     0   1   2   3   ...  ........  ...  c   c+1  ...
     |---|---|---|----        ----|----|---|---
      planted by the diagram        forced past every name

move	what you write down	what it forces
atomic diagram	basic facts, each object named	a copy of the old world is embedded
elementary diagram	every fact, not just basic ones	an exact, statement-respecting copy
extra demands	"bigger than every name"	an intruder past the whole copy
compactness	check each finite handful	one world meeting all demands at once

Read top to bottom: name everything, list the facts, pile on what you want, check finite handfuls, collect the world.

Worked example Beginner

We build a world that contains a faithful copy of the whole numbers and also a single number sitting past all of them. We do it with the two moves: write the diagram, then add demands.

Step 1. Name every whole number. Give $0$ the name $n_{0}$ , give $1$ the name $n_{1}$ , give $2$ the name $n_{2}$ , and so on, one private name per number.

Step 2. Write down the basic facts — the diagram. For every pair, record who is below whom: $n_{0} < n_{1}$ , $n_{1} < n_{2}$ , $n_{2} < n_{3}$ , and so on; also record the addition facts like $n_{1} + n_{1} = n_{2}$ . This is a long list, but every item on it is a plain basic fact true of the whole numbers.

Step 3. Add a new name $c$ and the extra demands $c > n_{0}$ , $c > n_{1}$ , $c > n_{2}$ , continuing without end. These say $c$ beats every named whole number.

Step 4. Check finite handfuls. Take any finite piece of the whole list. It mentions finitely many named numbers, with a largest name, say $n_{N}$ . Inside the ordinary whole numbers, let $c$ stand for $N + 1$ . Then every basic fact in the handful is true (it was true of the whole numbers) and every demand $c > n_{k}$ in the handful holds because $N + 1$ beats $0, 1, \dots, N$ . So the handful is met.

Step 5. Apply compactness. Every finite handful is met, so one world meets the entire list. In that world the names $n_{0}, n_{1}, n_{2}, \dots$ pick out a faithful copy of the whole numbers (all the basic facts hold), and $c$ names an object bigger than every one of them.

What this tells us: the diagram forced the copy, the extra demands forced the intruder, and finite-handful checking — each handful met by a big enough ordinary number — let compactness hand us a single world with both. The recipe is general: name, list, demand, check, collect.

Check your understanding Beginner

Exercise (easy, multiple choice).

You want to force any world to contain a faithful copy of the whole numbers. What do you write down?

A. A single demand saying "this world contains the whole numbers."

B. Every basic fact about the named whole numbers — who is below whom, what adds to what — using a private name for each one.

C. Only the demand that there is a number bigger than all the others.

D. Nothing; compactness builds the copy by itself.

Hint

The diagram is a list of basic facts, one for every relationship among the named objects.

Answer

B. Naming each whole number and writing down every basic fact about the names is the diagram; any world believing all of it must contain a faithful copy. Feedback-correct: the copy is forced by listing the basic facts under private names, not by a single slogan. Feedback-wrong: A is not something first-order facts can say in one line; C forces only an intruder, not a copy; D skips the work that does the forcing.

Formal definition Intermediate+

Fix a first-order language $L$ , the satisfaction relation $⊨$ , and the embedding/elementary-embedding hierarchy of 42.02.01 pending. The compactness theorem — a set of $L$ -sentences has a model iff every finite subset does — is established in 42.01.07 pending; this unit takes it as given and deploys it. The deployment device is the method of diagrams.

Let $M$ be an $L$ -structure with universe $M$ . Expand $L$ to $L_{M} = L \cup {c_{a} : a \in M}$ by a fresh constant for each element. The atomic diagram is $$ \mathrm{Diag}(\mathfrak{M}) = {, \varphi(c_{a_1}, \dots, c_{a_n}) : \varphi \text{ atomic or negated-atomic}, \ \mathfrak{M} \models \varphi[a_1, \dots, a_n] ,}, $$ and the elementary diagram $Diag_{el} (M)$ is the set of all $L_{M}$ -sentences true in $(M, a)_{a \in M}$ (the expansion interpreting $c_{a}$ as $a$ ) ^{[Marker Ch. 2]}.

Diagram lemma. For an $L_{M}$ -structure $N$ , write $h : a \mapsto c_{a}^{N}$ . Then $N ⊨ Diag (M)$ iff $h$ is an $L$ -embedding of $M$ into the reduct $N ↾ L$ , and $N ⊨ Diag_{el} (M)$ iff $h$ is an elementary embedding. The slogan: models of the diagram are the structures admitting an embedding of $M$ ; models of the elementary diagram are those admitting an elementary embedding. Composing the lemma with compactness gives the workhorse: an $L$ -theory $T$ has a model into which $M$ embeds iff $T \cup Diag (M)$ is satisfiable, and an elementary extension of $M$ satisfying $T$ iff $T \cup Diag_{el} (M)$ is satisfiable. Consistency becomes "there is a model embedding what I want."

Two named structural facts deployed below. A theory $T$ is complete when for every $L$ -sentence $σ$ , either $T ⊨ σ$ or $T ⊨ \neg σ$ . $T$ is $κ$ -categorical when all its models of cardinality $κ$ are isomorphic. A class $K$ of structures has the joint embedding property when any two members embed into a common member, and a theory admits elementary amalgamation when any two elementary extensions $N_{1}, N_{2}$ of a common $M$ admit elementary embeddings into a single $P$ agreeing on $M$ .

Counterexamples to common slips Intermediate+

" $Diag (M)$ already pins down $M$ up to isomorphism." It pins down only an embedded copy. The structure $(Z; <)$ models $Diag (N; <)$ via the inclusion, yet is not isomorphic to $(N; <)$ . The atomic diagram controls the quantifier-free fragment; quantified facts are the surplus carried only by $Diag_{el}$ .
"A $κ$ -categorical theory is complete with no further hypothesis." The Łoś-Vaught test needs no finite models. The theory of a single equivalence relation with exactly two classes, each infinite, fails categoricity in the relevant sense once finite models intrude; the cleanest statements require ruling finite models out so that all $κ$ -sized models are infinite and Löwenheim-Skolem applies uniformly.
"Compactness builds the model, so the diagram is optional." Compactness only certifies satisfiability of a sentence set. Without the diagram there is no sentence set whose models are forced to contain a prescribed structure; the diagram is exactly the translation of "embeds $M$ " into first-order sentences that compactness can act on.

Key theorem with proof Intermediate+

The signature result is the Łoś-Vaught test, the most-used completeness criterion in model theory: categoricity at a single cardinal, plus the absence of finite models, forces completeness. It is the diagram-and-compactness method turned into a decision procedure for "does this theory settle every sentence?"

Theorem (Łoś-Vaught test). Let $T$ be a satisfiable $L$ -theory with no finite models. If $T$ is $κ$ -categorical for some $κ \geq ∣ L ∣ + ℵ_{0}$ , then $T$ is complete ^{[Marker Ch. 2]}.

Proof. Suppose, toward a contradiction, that $T$ is not complete: some sentence $σ$ has $T \neq ⊨ σ$ and $T \neq ⊨ \neg σ$ . Then both $T \cup {\neg σ}$ and $T \cup {σ}$ are satisfiable, by models $A$ and $B$ respectively, with $A ⊨ \neg σ$ and $B ⊨ σ$ . Since $T$ has no finite models, $A$ and $B$ are infinite. By the Löwenheim-Skolem theorems of 42.01.07 pending — downward to shrink and upward (adjoin $κ$ distinct constants to $Diag_{el}$ and apply compactness) to grow — each of $A, B$ has a model elementarily equivalent to it of cardinality exactly $κ$ . Call these $A_{κ} \equiv A$ and $B_{κ} \equiv B$ ; both model $T$ , both have cardinality $κ$ . Now $κ$ -categoricity gives $A_{κ} ≅ B_{κ}$ , hence $A_{κ} \equiv B_{κ}$ . But $A_{κ} ⊨ \neg σ$ (it agrees with $A$ ) while $B_{κ} ⊨ σ$ (it agrees with $B$ ), so $A_{κ} \neq \equiv B_{κ}$ . The contradiction shows no such $σ$ exists, so $T$ is complete. $□$

Corollary (worked completeness results). The theory $DLO$ of dense linear orders without endpoints is $ℵ_{0}$ -categorical (Cantor's back-and-forth theorem, 42.02.01 pending) with no finite models, hence complete; the theory $ACF_{p}$ of algebraically closed fields of fixed characteristic $p$ is $κ$ -categorical in every uncountable $κ$ (a model is determined up to isomorphism by its transcendence degree, which equals $κ$ when $κ > ℵ_{0}$ ) with no finite models, hence complete — and decidable, since a complete recursively axiomatized theory is decidable. The same test certifies the completeness of the theory of the random graph and of infinite-dimensional vector spaces over a fixed field. The deeper structure of $κ$ -categoricity — Morley's theorem that categoricity in one uncountable cardinal forces it in all — is the subject of 42.02.06 pending.

Bridge. The Łoś-Vaught test is the foundational reason a single categoricity datum settles every sentence: completeness, an unbounded condition over all sentences, is decided by one isomorphism at one cardinal, and this is exactly the diagram-and-compactness method run as a completeness criterion. It builds toward the elementary amalgamation and Robinson consistency results below, whose proofs splice models along shared elementary diagrams, and it appears again in the categoricity theory of 42.02.06 pending, where Morley's theorem upgrades the single-cardinal hypothesis to a transfer across all uncountable cardinals. The argument generalises the non-standard-model construction of 42.01.07 pending from "force one intruder" to "force a model of prescribed size elementarily equivalent to a given one," and putting these together, the upward and downward Löwenheim-Skolem moves that resize a model are precisely the steps that make two arbitrary models of $T$ comparable at the categoricity cardinal. The central insight is that completeness equals " $\equiv$ -uniqueness," and at the categoricity cardinal $\equiv$ -uniqueness collapses into $≅$ -uniqueness, which the hypothesis hands over for free.

Exercises Intermediate+

Exercise 3 (medium, symbolic).

Use the elementary diagram and compactness to prove that every structure $M$ has a proper elementary extension (one $N ≻ M$ with $∣ N ∣ > ∣ M ∣$ when $M$ is infinite, or merely $N \neq = M$ ).

Hint

Add one new constant $d$ to $Diag_{el} (M)$ together with $d \neq = c_{a}$ for every $a \in M$ . Check finite satisfiability in $M$ itself.

Answer

Form $Γ = Diag_{el} (M) \cup {d \neq = c_{a} : a \in M}$ in $L_{M} \cup {d}$ . A finite $Γ_{0}$ uses $d \neq = c_{a}$ for finitely many $a$ , say $a \in F$ ; interpret the structure as $(M, a)_{a \in M}$ and let $d$ be any element of $M ∖ F$ (nonempty when $M$ is infinite; for finite $M$ adjoin one new point realizing the same elementary type if available, otherwise the claim is for infinite $M$ ). Then $Γ_{0}$ holds, so by compactness $Γ$ has a model $N^{*}$ . By the diagram lemma its reduct $N$ is an elementary extension of $M$ via $a \mapsto c_{a}^{N^{*}}$ , and $d^{N^{*}}$ is distinct from every image $c_{a}^{N^{*}}$ , so the embedding is not onto and $N ≻ M$ properly. Rubric: full credit for the elementary-diagram-plus-new-constant theory, the finite-satisfiability check, and the diagram-lemma conclusion that the extension is elementary and proper.

Exercise 4 (medium, symbolic).

Prove the Łoś-Vaught test specialization: deduce that $DLO$ (dense linear orders without endpoints) is complete, citing the categoricity input.

Hint

$DLO$ has no finite models and is $ℵ_{0}$ -categorical by Cantor's back-and-forth theorem. Apply the test at $κ = ℵ_{0}$ .

Answer

$DLO$ is satisfiable ( $(Q; <)$ is a model) and has no finite models (density forces infinitely many points between any two). By Cantor's theorem (42.02.01 pending) any two countable dense linear orders without endpoints are isomorphic, so $DLO$ is $ℵ_{0}$ -categorical, and $ℵ_{0} = ∣ L ∣ + ℵ_{0}$ for the finite language ${<}$ . The Łoś-Vaught test applies: a satisfiable theory with no finite models, $κ$ -categorical at $κ = ℵ_{0} \geq ∣ L ∣ + ℵ_{0}$ , is complete. Hence $DLO$ decides every ${<}$ -sentence, and since it is recursively axiomatized it is decidable. Rubric: full credit for verifying no-finite-models, citing $ℵ_{0}$ -categoricity, and invoking the test at the right cardinal.

Exercise 5 (medium, symbolic).

State and prove the Łoś-Tarski preservation direction one way: if a theory $T$ is axiomatized by universal ( $Π_{1}$ ) sentences, then $T$ is preserved under substructures (every substructure of a model of $T$ is a model of $T$ ).

Hint

A universal sentence true in $N$ restricts to any substructure $M \subseteq N$ because substructures preserve and reflect quantifier-free formulas, over which the universal quantifier ranges into a smaller domain.

Answer

Let $σ = \forall \overset{x}{ˉ} ψ (\overset{x}{ˉ})$ with $ψ$ quantifier-free, and suppose $N ⊨ σ$ and $M \subseteq N$ . For any tuple $\overset{a}{ˉ}$ from $M \subseteq N$ , $N ⊨ ψ [\overset{a}{ˉ}]$ since $N ⊨ σ$ ; as $M \subseteq N$ preserves quantifier-free formulas in both directions (42.02.01 pending, Proposition 1), $M ⊨ ψ [\overset{a}{ˉ}]$ . As $\overset{a}{ˉ}$ was arbitrary, $M ⊨ \forall \overset{x}{ˉ} ψ = σ$ . If $T$ is axiomatized by such sentences, each holds in $M$ , so $M ⊨ T$ . (The converse — preservation under substructures implies $Π_{1}$ -axiomatizability — is the harder diagram-and-compactness direction.) Rubric: full credit for the quantifier-free restriction argument and the conclusion for the whole axiom set.

Exercise 6 (medium, symbolic).

Show that the diagonal embedding $M \to M^{I} / U$ into an ultrapower (each $a \mapsto$ the class of the constant function $a$ ) is elementary, citing Łoś's theorem.

Hint

Łoś's theorem says a formula holds of a tuple of classes in $M^{I} / U$ iff it holds of the representatives at $U$ -almost-all indices. For a constant tuple, the index set is all of $I \in U$ .

Answer

Let $d : M \to M^{I} / U$ send $a$ to the class $[i \mapsto a]_{U}$ of the constant function. For an $L$ -formula $φ$ and tuple $\overset{a}{ˉ}$ from $M$ , Łoś's theorem gives $M^{I} / U ⊨ φ [d \overset{a}{ˉ}] \Leftrightarrow {i \in I : M ⊨ φ [\overset{a}{ˉ}]} \in U$ . The set on the right is either $\emptyset$ or all of $I$ depending on whether $M ⊨ φ [\overset{a}{ˉ}]$ , and $I \in U$ while $\emptyset \in / U$ . Hence $M^{I} / U ⊨ φ [d \overset{a}{ˉ}] \Leftrightarrow M ⊨ φ [\overset{a}{ˉ}]$ , which is exactly the elementarity of $d$ . Rubric: full credit for applying Łoś to the constant tuple and reading off the equivalence with $M ⊨ φ [\overset{a}{ˉ}]$ .

Exercise 7 (hard, symbolic).

Prove elementary amalgamation: if $M ⪯ N_{1}$ and $M ⪯ N_{2}$ , there is a structure $P$ with elementary embeddings $f_{1} : N_{1} \to P$ and $f_{2} : N_{2} \to P$ that agree on $M$ (i.e. $f_{1} ↾ M = f_{2} ↾ M$ ).

Hint

Work in a language with constants for $N_{1}$ and for $N_{2}$ , sharing the constants for $M$ . Show $Diag_{el} (N_{1}) \cup Diag_{el} (N_{2})$ is satisfiable by checking finite subsets, using that both agree with $Diag_{el} (M)$ on shared constants.

Answer

Choose disjoint constant sets ${c_{b} : b \in N_{1}}$ and ${d_{e} : e \in N_{2}}$ but identify $c_{a} = d_{a}$ for $a \in M$ (legitimate since $M \subseteq N_{1}$ and $M \subseteq N_{2}$ as elementary substructures). Let $Γ = Diag_{el} (N_{1}) \cup Diag_{el} (N_{2})$ in the combined language. A finite $Γ_{0}$ involves finitely many constants from each side; the $N_{2}$ -side sentences in $Γ_{0}$ are, up to the shared $M$ -constants, an elementary-diagram fragment of $N_{2}$ with parameters whose $L (M)$ -type is realized in $N_{1}$ because $N_{1} ⪰ M$ and $N_{2} ⪰ M$ force agreement on all $L (M)$ -formulas. Concretely: interpret all constants inside $N_{1}$ , sending the shared $M$ -constants to their elements of $M$ and the finitely many $d_{e}$ -constants of $Γ_{0}$ to witnesses in $N_{1}$ realizing the same $L (M)$ -formulas they satisfy in $N_{2}$ (such witnesses exist since $N_{1} \equiv_{M} N_{2}$ , both being elementary extensions of $M$ ). Then $N_{1}$ models $Γ_{0}$ , so $Γ$ is finitely satisfiable; compactness yields a model $P^{*}$ , whose reduct $P$ receives elementary embeddings $f_{1}, f_{2}$ of $N_{1}, N_{2}$ by the diagram lemma, agreeing on $M$ because the $M$ -constants were identified. Rubric: full credit for the shared-constant setup, the finite-satisfiability check using $N_{1} \equiv_{M} N_{2}$ , and the diagram-lemma extraction of the two elementary embeddings agreeing on $M$ .

Exercise 8 (hard, symbolic).

Derive Craig's interpolation theorem from the Robinson joint consistency theorem (which you may assume): if $⊨ φ \to ψ$ for $L$ -sentences $φ, ψ$ , there is an interpolant $θ$ in the common vocabulary with $⊨ φ \to θ$ and $⊨ θ \to ψ$ .

Hint

Let $L_{1}$ be the vocabulary of $φ$ , $L_{2}$ that of $ψ$ , $L_{0} = L_{1} \cap L_{2}$ . If no $L_{0}$ -interpolant exists, the $L_{0}$ -consequences of $φ$ and of $\neg ψ$ are jointly consistent over $L_{0}$ ; apply Robinson to get a model of $φ \land \neg ψ$ .

Answer

Let $L_{1}, L_{2}$ be the vocabularies of $φ, ψ$ and $L_{0} = L_{1} \cap L_{2}$ . Let $Θ = {θ an L_{0} -sentence : φ ⊨ θ}$ be the $L_{0}$ -consequences of $φ$ . Suppose no interpolant exists, i.e. no $θ \in Θ$ has $θ ⊨ ψ$ . Then $Θ \cup {\neg ψ}$ is satisfiable: otherwise $Θ ⊨ ψ$ , and by compactness a finite conjunction $θ_{0}$ of members of $Θ$ has $θ_{0} ⊨ ψ$ , an interpolant. Take a model and let $T_{2} = Th (its L_{2} -reduct) \supseteq {\neg ψ}$ , and $T_{1}$ the deductive closure of ${φ}$ in $L_{1}$ . Their $L_{0}$ -restrictions are jointly consistent: $T_{1}$ 's $L_{0}$ -consequences are exactly $Θ$ (the $L_{0}$ -theory generated by $φ$ ), which holds in the chosen model, so no $L_{0}$ -sentence is proved by $T_{1}$ and refuted by $T_{2}$ . By Robinson joint consistency, $T_{1} \cup T_{2}$ has a model $A$ ; then $A ⊨ φ$ (from $T_{1}$ ) and $A ⊨ \neg ψ$ (from $T_{2}$ ), so $A ⊨ φ \land \neg ψ$ , contradicting $⊨ φ \to ψ$ . Hence an interpolant $θ \in Θ$ with $θ ⊨ ψ$ exists; $φ ⊨ θ$ holds by construction, and the degenerate cases (unsatisfiable $φ$ , valid $ψ$ ) take $θ = ⊥, ⊤$ . Rubric: full credit for the $L_{0}$ -consequence set, the no-interpolant $\Rightarrow$ joint-consistency step, and the Robinson contradiction with $⊨ φ \to ψ$ .

Advanced results Master

The compactness theorem and the diagram lemma organize five developments: the diagram dictionary turning consistency into embeddings, the Łoś-Vaught completeness test with its amalgamation companions, the Robinson-Craig-Beth circle on consistency and definability, the preservation theorems reading the quantifier prefix off the map hierarchy, and the ultraproduct construction supplying the calculus-free proof and the Keisler-Shelah characterization of $\equiv$ .

Theorem 1 (the diagram dictionary). For an $L$ -structure $M$ and an $L$ -theory $T$ : $T$ has a model embedding $M$ iff $T \cup Diag (M)$ is satisfiable, and $T$ has a model into which $M$ embeds elementarily iff $T \cup Diag_{el} (M)$ is satisfiable ^{[Marker Ch. 2]}. Fed to compactness, this manufactures structures with prescribed substructures: the non-standard models of arithmetic ( $T = Th (N)$ , $Diag_{el} (N)$ , plus $c > S^{n} 0$ ); the proper elementary extensions of any infinite $M$ (add $d \neq = c_{a}$ for all $a$ ); the models realizing a prescribed set of formulas (a type) by adding those formulas in a fresh variable-constant and checking finite satisfiability against $Diag_{el} (M)$ — the construction 42.02.03 pending develops in full. The diagram is the precise translation under which "embeds $M$ " becomes a first-order constraint that compactness can satisfy.

Theorem 2 (Łoś-Vaught test, amalgamation, joint embedding). A satisfiable theory with no finite models that is $κ$ -categorical for some $κ \geq ∣ L ∣ + ℵ_{0}$ is complete ^{[Marker Ch. 2]}; the worked instances are $DLO$ , $ACF_{p}$ , the random graph, and infinite vector spaces over a fixed field, all thereby complete and (being recursively axiomatized) decidable. The proof is the resize-to- $κ$ -and-compare argument, and the same diagram amalgamation yields more: any two elementary extensions of a common $M$ amalgamate elementarily over $M$ (satisfiability of $Diag_{el} (N_{1}) \cup Diag_{el} (N_{2})$ with shared $M$ -constants), and a complete theory has the joint embedding property (its models elementarily embed into a common elementary extension). These amalgamation facts are the existence proofs behind monster models and the homogeneous-universal models on which stability theory operates.

Theorem 3 (Robinson consistency, Craig interpolation, Beth definability). Robinson's joint consistency theorem: for theories $T_{1} \supseteq T$ in $L_{1}$ and $T_{2} \supseteq T$ in $L_{2}$ with $T$ a complete theory in $L_{0} = L_{1} \cap L_{2}$ , the union $T_{1} \cup T_{2}$ is consistent; in general $T_{1} \cup T_{2}$ is consistent iff no $L_{0}$ -sentence is proved by $T_{1}$ and refuted by $T_{2}$ ^{[Robinson 1956]}. The proof is the alternating elementary-chain amalgamation: build $M_{0} ⪯ M_{1} ⪯ \dots$ flipping between models of $T_{1}$ and $T_{2}$ , at each stage realizing the elementary diagram of the previous model over the shared $L_{0}$ -reduct by compactness and the $L_{0}$ -completeness hypothesis, and taking the union, whose $L_{1}$ - and $L_{2}$ -reducts model $T_{1}$ and $T_{2}$ . Craig's interpolation theorem — $⊨ φ \to ψ$ yields an interpolant $θ$ in the common vocabulary with $⊨ φ \to θ \to ψ$ — follows from Robinson consistency by the no-interpolant-implies-joint-consistency contrapositive ^{[Craig 1957]}. Beth's definability theorem — implicit definability of a predicate by a theory equals explicit definability over the old vocabulary — follows from interpolation applied to the two-copy theory $T (R) \cup T (R^{'})$ asserting that two predicates implicitly defined the same way must coincide; the interpolant in the shared old vocabulary is the explicit definition.

Theorem 4 (preservation theorems via diagrams). The Łoś-Tarski theorem: a first-order theory is preserved under substructures iff it is axiomatizable by universal ( $Π_{1}$ ) sentences, and preserved under extensions iff by existential ( $Σ_{1}$ ) sentences ^{[Chang and Keisler Ch. 3]}. The forward direction (syntax $\to$ preservation) is the quantifier-free restriction of 42.02.01 pending; the converse (preservation $\to$ syntax) is the diagram argument: if $T$ is preserved under substructures, the set of $Π_{1}$ -consequences $T_{\forall}$ has the same models as $T$ , proved by embedding a model of $T_{\forall}$ into a model of $T$ via a compactness argument on $Diag$ plus the universal theory of the target. The Chang-Łoś-Suszko theorem extends this: a theory is preserved under unions of chains iff it is $Π_{2}$ -axiomatizable, the diagram amalgamation now run along an $ω$ -chain. These read the quantifier prefix as the exact semantic invariant a map respects, the preservation counterpart of the prenex hierarchy.

Theorem 5 (ultraproducts, Łoś's theorem, Keisler-Shelah). The ultraproduct $\prod_{U} M_{i}$ over an ultrafilter $U$ on the index set satisfies a formula of a tuple of $U$ -classes iff $U$ -almost-all factors satisfy it of the representatives — Łoś's theorem ^{[Chang and Keisler Ch. 4]}. This yields the calculus-free compactness proof (the ultraproduct of models of each finite subset, over an ultrafilter concentrating on the cones, models the whole theory), and it is a construction tool: the diagonal embedding into the ultrapower $M^{I} / U$ is elementary, so $M^{I} / U$ is an elementary extension; $R^{*} = R^{N} / U$ over a non-principal $U$ is the hyperreals, with the transfer principle as Łoś applied to $R$ . The Keisler-Shelah isomorphism theorem closes the circle: $M \equiv N$ iff there is an index set $I$ and ultrafilter $U$ with $M^{I} / U ≅ N^{I} / U$ — elementary equivalence is exactly isomorphism of suitable ultrapowers, a purely algebraic rendering of the logical relation $\equiv$ of 42.02.01 pending.

Synthesis. The diagram lemma is the foundational reason model theory is constructive rather than merely comparative, and putting these together it drives all five developments through one translation: " $N$ embeds $M$ " becomes " $N ⊨ Diag (M)$ ," so compactness, which only ever certifies satisfiability, becomes a machine for building structures with prescribed parts. This is exactly what Theorem 1 makes precise and what the Łoś-Vaught test of Theorem 2 exploits — completeness is $\equiv$ -uniqueness, and the resize-to- $κ$ moves of 42.01.07 pending collapse $\equiv$ -uniqueness into the $≅$ -uniqueness that categoricity supplies. The Robinson-Craig-Beth circle of Theorem 3 is the same amalgamation read for definability: the alternating elementary chain that splices two theories over a shared complete $L_{0}$ -theory is dual to the interpolant that separates them, and Beth definability is the central insight that implicit and explicit definition coincide because the splicing model and the interpolating sentence are two faces of one consistency fact. The preservation theorems of Theorem 4 generalise the map hierarchy of 42.02.01 pending from "which formulas a fixed map respects" to "which theories a class of maps respects," reading the quantifier prefix as the semantic invariant; the converse directions are diagram-and-compactness arguments, the bridge being that $T_{\forall}$ and $T$ share models exactly when every model of the universal theory embeds into a model of $T$ .

Ultraproducts of Theorem 5 supply the alternative proof of the compactness that started the chapter and, via Keisler-Shelah, identify the logical relation $\equiv$ with an algebraic isomorphism of ultrapowers — the same equivalence approached from compactness, from games 42.02.01 pending, and now from ultrafilters. This is the workhorse promised at the Beginner tier: name, list, demand, check, collect, assembled into the engine that builds the types 42.02.03 pending, the quantifier-eliminating theories 42.02.05 pending, and the categorical theories 42.02.06 pending of the rest of model theory.

Full proof set Master

Proposition 1 (diagram lemma). Let $M$ be an $L$ -structure and $N$ an $L_{M}$ -structure, $h : a \mapsto c_{a}^{N}$ . Then $N ⊨ Diag (M)$ iff $h$ is an $L$ -embedding $M \to N ↾ L$ , and $N ⊨ Diag_{el} (M)$ iff $h$ is elementary.

Proof. For the atomic case, $N ⊨ Diag (M)$ means that for every atomic or negated-atomic $φ$ and tuple $\overset{a}{ˉ}$ from $M$ , $M ⊨ φ [\overset{a}{ˉ}]$ iff $N ⊨ φ (c_{\overset{a}{ˉ}})$ , and $N ⊨ φ (c_{\overset{a}{ˉ}})$ iff $N ↾ L ⊨ φ [h \overset{a}{ˉ}]$ by the definition of $h$ . So membership in $Diag (M)$ records exactly $M ⊨ φ [\overset{a}{ˉ}] \Leftrightarrow N ↾ L ⊨ φ [h \overset{a}{ˉ}]$ for all atomic and negated-atomic $φ$ . This biconditional for all such $φ$ is precisely the condition that $h$ preserves and reflects atomic relations and term values; the negated equalities $c_{a} \neq = c_{b}$ ( $a \neq = b$ ) force $h$ injective. By the embedding criterion of 42.02.01 pending, $h$ is an embedding. The elementary case repeats the argument with $φ$ ranging over all $L$ -formulas: $N ⊨ Diag_{el} (M)$ iff $M ⊨ φ [\overset{a}{ˉ}] \Leftrightarrow N ↾ L ⊨ φ [h \overset{a}{ˉ}]$ for every $φ$ , which is the definition of $h$ being elementary. $□$

Proposition 2 (consistency-to-embedding). An $L$ -theory $T$ has a model admitting an embedding (resp. elementary embedding) of $M$ iff $T \cup Diag (M)$ (resp. $T \cup Diag_{el} (M)$ ) is satisfiable.

Proof. ( $\Rightarrow$ ) If $N ⊨ T$ with an embedding $g : M \to N$ , expand $N$ to $L_{M}$ by $c_{a}^{N^{*}} = g (a)$ ; then $N^{*} ⊨ T$ (the sentences of $T$ are $L$ -sentences, unaffected) and $N^{*} ⊨ Diag (M)$ by Proposition 1, so the union is satisfiable. ( $\Leftarrow$ ) If $N^{*} ⊨ T \cup Diag (M)$ , its reduct $N = N^{*} ↾ L$ models $T$ and, by Proposition 1, receives the embedding $a \mapsto c_{a}^{N^{*}}$ . The elementary case is identical with $Diag_{el}$ . $□$

Proposition 3 (Łoś-Vaught test). A satisfiable $L$ -theory $T$ with no finite models that is $κ$ -categorical for some $κ \geq ∣ L ∣ + ℵ_{0}$ is complete.

Proof. If not, fix $σ$ with $T \cup {σ}$ and $T \cup {\neg σ}$ both satisfiable, by infinite models $B ⊨ T \cup {σ}$ , $A ⊨ T \cup {\neg σ}$ (infinite because $T$ has no finite models). By the downward and upward Löwenheim-Skolem theorems 42.01.07 pending — the upward direction via adjoining $κ$ distinct constants to the elementary diagram and applying compactness, then trimming by the downward theorem — there are $A_{κ} \equiv A$ and $B_{κ} \equiv B$ of cardinality exactly $κ$ , both modelling $T$ . By $κ$ -categoricity $A_{κ} ≅ B_{κ}$ , so $A_{κ} \equiv B_{κ}$ . But $A_{κ} ⊨ \neg σ$ and $B_{κ} ⊨ σ$ , contradicting $\equiv$ . So $T$ decides every $σ$ . $□$

Proposition 4 (proper elementary extensions exist). Every infinite $L$ -structure $M$ has a proper elementary extension.

Proof. Let $Γ = Diag_{el} (M) \cup {d \neq = c_{a} : a \in M}$ in $L_{M} \cup {d}$ . A finite $Γ_{0}$ constrains $d \neq = c_{a}$ for $a$ in a finite $F \subseteq M$ ; interpreting the base as $(M, a)_{a \in M}$ and $d$ as any element of the infinite set $M ∖ F$ models $Γ_{0}$ . By compactness $Γ$ has a model $N^{*}$ ; by Proposition 2 (elementary case) its reduct $N$ is an elementary extension of $M$ via $a \mapsto c_{a}^{N^{*}}$ , and $d^{N^{*}}$ differs from every $c_{a}^{N^{*}}$ , so the embedding is not surjective: $M ≺ N$ properly. $□$

Proposition 5 (elementary amalgamation). If $M ⪯ N_{1}$ and $M ⪯ N_{2}$ , there are a structure $P$ and elementary embeddings $f_{i} : N_{i} \to P$ agreeing on $M$ .

Proof. In a language with disjoint constants ${c_{b}}_{b \in N_{1}}$ , ${d_{e}}_{e \in N_{2}}$ identified on $M$ ( $c_{a} = d_{a}$ for $a \in M$ ), let $Γ = Diag_{el} (N_{1}) \cup Diag_{el} (N_{2})$ . A finite $Γ_{0}$ mentions finitely many $d_{e}$ , say $e \in E \subseteq N_{2} ∖ M$ , with a conjunction $χ (\overset{c}{ˉ}, \overset{ˉ}{d}_{E})$ of their elementary-diagram sentences over $M$ -constants $\overset{c}{ˉ}$ . Since $N_{2} ⪰ M$ , the tuple $\overset{e}{ˉ}$ realizes some $L (M)$ -type, and as $N_{1} ⪰ M$ as well, $N_{1} \equiv_{M} N_{2}$ , so $N_{1} ⊨ \exists \overset{x}{ˉ} χ (\overset{c}{ˉ}, \overset{x}{ˉ})$ (the existential closure over the $M$ -parameters holds in $N_{2}$ , hence in $N_{1}$ ). Interpreting the $N_{1}$ -constants in $N_{1}$ and the finitely many $d_{e}$ as such witnesses models $Γ_{0}$ . By compactness $Γ$ is satisfiable in some $P^{*}$ ; Proposition 2 extracts elementary embeddings $f_{1}, f_{2}$ of $N_{1}, N_{2}$ into $P = P^{*} ↾ L$ , and the identified $M$ -constants force $f_{1} ↾ M = f_{2} ↾ M$ . $□$

Proposition 6 (Łoś's theorem and the elementary ultrapower). For an ultrafilter $U$ on $I$ and structures $(M_{i})_{i \in I}$ , $\prod_{U} M_{i} ⊨ φ [[f_{1}]_{U}, \dots] \Leftrightarrow {i : M_{i} ⊨ φ [f_{1} (i), \dots]} \in U$ ; consequently the diagonal map $M \to M^{I} / U$ is elementary.

Proof. Induct on $φ$ . Atomic formulas hold by the definition of the ultraproduct operations on $U$ -classes and the ultrafilter's closure under supersets and finite intersections. Negation uses that $U$ is an ultrafilter (a set is in $U$ iff its complement is not): $\prod_{U} M_{i} ⊨ \neg φ$ iff ${i : M_{i} ⊨ φ} \in / U$ iff its complement ${i : M_{i} ⊨ \neg φ} \in U$ . Conjunction uses closure under intersection. For $\exists y ψ$ : if the index set $J = {i : M_{i} ⊨ \exists y ψ} \in U$ , choose for each $i \in J$ a witness $g (i)$ and set $g (i)$ arbitrarily off $J$ ; then ${i : M_{i} ⊨ ψ [g (i), \dots]} \supseteq J \in U$ , so by the inductive hypothesis $\prod_{U} M_{i} ⊨ ψ [[g]_{U}, \dots]$ , whence $⊨ \exists y ψ$ . Conversely a witness class $[g]_{U}$ pushes its defining index set into $U$ and hence into $J$ . Taking all $M_{i} = M$ and $f$ constant gives, for the diagonal $d (a) = [i \mapsto a]_{U}$ , the index set $\emptyset$ or $I$ ; since $I \in U$ , $\prod_{U} M ⊨ φ [d \overset{a}{ˉ}] \Leftrightarrow M ⊨ φ [\overset{a}{ˉ}]$ , so $d$ is elementary. $□$

Connections Master

Structures, embeddings, and elementary equivalence 42.02.01 pending supplies the map hierarchy and the diagram definitions this unit deploys. The atomic and elementary diagrams introduced there as the bridge from comparison to construction are realized here as satisfiable theories whose models are forced to embed a prescribed structure; the embedding criterion and the elementary-substructure machinery of that unit are exactly the inputs to the diagram lemma. That unit owns the static comparison of two structures; this unit turns the comparison into a generator of new ones.
Compactness and the Löwenheim-Skolem theorems for first-order logic 42.01.07 pending is the metatheorem this unit takes as its engine. The compactness statement proved there as a corollary of completeness, and the upward and downward Löwenheim-Skolem theorems that resize models, are the precise tools the Łoś-Vaught test and the amalgamation arguments call. Where that unit proves compactness, this unit aims it: every construction here is a finite-satisfiability check feeding the theorem of that unit.
Types and the omitting types theorem, co-produced as 42.02.03 pending, extends the diagram method from realizing a single structure to realizing and omitting prescribed sets of formulas. The diagram-plus-new-constant construction that builds elementary extensions here is the realizing half; the omitting types theorem is its dual, constructing models that avoid a non-isolated type, and both run on the consistency-to-model translation this unit establishes. Saturated and homogeneous models are the amalgamation closure of the extensions built here.
Quantifier elimination and model completeness, co-produced as 42.02.05 pending, specialize the preservation theorems and the diagram method to theories whose embeddings are all elementary. Model completeness is precisely that every embedding between models is elementary — the diagram lemma then makes $Diag$ and $Diag_{el}$ interchangeable over models of the theory — and Robinson's test for model completeness is a direct diagram-and-compactness criterion. The completeness results the Łoś-Vaught test yields here ( $ACF_{p}$ , $DLO$ ) are exactly the theories that unit shows eliminate quantifiers.
Categoricity and Morley's theorem 42.02.06 pending upgrades the single-cardinal hypothesis of the Łoś-Vaught test. Where the test here takes $κ$ -categoricity at one cardinal as input to completeness, Morley's theorem proves that uncountable categoricity at one cardinal transfers to all uncountable cardinals, refining the crude completeness criterion into the stability-theoretic classification. The amalgamation and elementary-extension constructions of this unit are the existence lemmas that the categoricity analysis presupposes.

Historical & philosophical context Master

The method of diagrams is due to Abraham Robinson, who introduced it in the early 1950s as the systematic device for converting algebraic and model-theoretic existence questions into questions of consistency, to be settled by the compactness theorem. Robinson's 1956 paper "A result on consistency and its application to the theory of definition" proved the joint consistency theorem and applied it to the theory of definition, recovering Evert Beth's 1953 theorem that implicit definability coincides with explicit definability ^{[Robinson 1956]}. William Craig's 1957 "Three uses of the Herbrand-Gentzen theorem" established the interpolation theorem, originally by proof-theoretic means via cut elimination, and observed its bearing on definability; the model-theoretic derivation of interpolation from Robinson consistency, and of Beth definability from interpolation, organized these results into the single circle presented here ^{[Craig 1957]}.

The Łoś-Vaught test was isolated independently by Jerzy Łoś and Robert Vaught around 1954 as the first general criterion deriving completeness from categoricity, and it remains the standard route to the completeness of $ACF_{p}$ , $DLO$ , and the random graph. Łoś's fundamental theorem on ultraproducts, also from 1955, supplied the calculus-free proof of compactness and the ultrapower construction; H. Jerome Keisler and later Saharon Shelah established that elementary equivalence is exactly isomorphism of suitable ultrapowers, the Keisler-Shelah theorem, codified with the preservation theorems of Łoś, Tarski, Chang, and Suszko in the textbooks of Chang and Keisler, Hodges, and Marker ^{[Chang and Keisler Ch. 4]}.

Bibliography Master

@book{marker2002modeltheory,
  author    = {Marker, David},
  title     = {Model Theory: An Introduction},
  series    = {Graduate Texts in Mathematics},
  volume    = {217},
  publisher = {Springer},
  year      = {2002}
}

@book{changkeisler1990,
  author    = {Chang, Chen Chung and Keisler, H. Jerome},
  title     = {Model Theory},
  edition   = {3},
  series    = {Studies in Logic and the Foundations of Mathematics},
  volume    = {73},
  publisher = {North-Holland},
  year      = {1990}
}

@book{hodges1993modeltheory,
  author    = {Hodges, Wilfrid},
  title     = {Model Theory},
  series    = {Encyclopedia of Mathematics and its Applications},
  volume    = {42},
  publisher = {Cambridge University Press},
  year      = {1993}
}

@article{robinson1956consistency,
  author  = {Robinson, Abraham},
  title   = {A result on consistency and its application to the theory of definition},
  journal = {Indagationes Mathematicae},
  volume  = {18},
  year    = {1956},
  pages   = {47--58}
}

@article{craig1957interpolation,
  author  = {Craig, William},
  title   = {Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory},
  journal = {Journal of Symbolic Logic},
  volume  = {22},
  year    = {1957},
  pages   = {269--285}
}

@article{beth1953,
  author  = {Beth, Evert W.},
  title   = {On Padoa's method in the theory of definition},
  journal = {Indagationes Mathematicae},
  volume  = {15},
  year    = {1953},
  pages   = {330--339}
}

@article{vaught1954,
  author  = {Vaught, Robert L.},
  title   = {Applications of the L\"{o}wenheim-Skolem-Tarski theorem to problems of completeness and decidability},
  journal = {Indagationes Mathematicae},
  volume  = {16},
  year    = {1954},
  pages   = {467--472}
}

@article{keisler1961ultraproducts,
  author  = {Keisler, H. Jerome},
  title   = {Ultraproducts and elementary classes},
  journal = {Indagationes Mathematicae},
  volume  = {23},
  year    = {1961},
  pages   = {477--495}
}

@article{shelah1971ultrapower,
  author  = {Shelah, Saharon},
  title   = {Every two elementarily equivalent models have isomorphic ultrapowers},
  journal = {Israel Journal of Mathematics},
  volume  = {10},
  year    = {1971},
  pages   = {224--233}
}

Prerequisites

42.02.01

Tier anchors

beginner: Marker 2002 *Model Theory: An Introduction* (Springer GTM 217) §2.1-2.2 (compactness read informally as 'if every finite handful of demands can be met, the whole batch can be met at once', and the method of diagrams read as 'write down every basic fact about a world, name each object with its own label, and any world that believes all those labelled facts must contain a faithful copy of the first'; the picture of forcing an extra number bigger than every ordinary one, or a number smaller than every ordinary fraction, simply by listing demands and checking each finite handful by hand); building a world that contains a copy of the whole numbers and also an intruder past all of them
intermediate: Marker 2002 *Model Theory: An Introduction* §2.1-2.3 (the compactness theorem as the model-building workhorse; the atomic diagram Diag(M) and the diagram lemma — a structure models Diag(M) iff it admits an embedding of M; the elementary diagram Diag_el(M) and elementary embeddings; building elementary extensions with prescribed elements by compactness, the non-standard models of arithmetic, the upward Löwenheim-Skolem theorem via new constants, the Łoś-Vaught test for completeness); Chang and Keisler 1990 *Model Theory* 3e (North-Holland) Ch. 2-3
master: Marker 2002 *Model Theory: An Introduction* (Springer GTM 217) Ch. 2 (compactness, diagrams, elementary amalgamation, the Łoś-Vaught test, preservation theorems, types); Chang and Keisler 1990 *Model Theory* 3e (North-Holland) Ch. 2-5 (the systematic theory of diagrams, ultraproducts and Łoś's theorem, the Keisler-Shelah isomorphism theorem, the Robinson consistency and Craig interpolation theorems, Beth definability, preservation theorems); Hodges 1993 *Model Theory* (Cambridge) Ch. 5-6, 8-9 (the preservation hierarchy via diagrams, amalgamation and the joint embedding property, interpolation); Robinson 1956 *A result on consistency and its application to the theory of definition* (Indag. Math. 18) and Craig 1957 *Three uses of the Herbrand-Gentzen theorem* (J. Symbolic Logic 22)

References

Marker, D. — Model Theory: An Introduction · Graduate Texts in Mathematics 217, Springer (2002), Chapter 2. Treats compactness as the central model-building tool of model theory and develops the method of diagrams. For an L-structure M with universe M, expand L to L_M by adjoining a constant c_a for each a ∈ M; the atomic diagram Diag(M) is the set of all atomic and negated-atomic L_M-sentences true in M (under c_a ↦ a), and the elementary diagram Diag_el(M) is the set of ALL L_M-sentences true in M. The diagram lemma: an L_M-structure N models Diag(M) iff the map a ↦ c_a^N is an L-embedding of M into the reduct of N; N models Diag_el(M) iff that map is an elementary embedding. Combined with compactness this is the engine for building models with prescribed properties: a theory T has a model embedding M iff T ∪ Diag(M) is satisfiable, and an elementary extension realizing M iff T ∪ Diag_el(M) is satisfiable. Applications: non-standard models of arithmetic (𝔑 has a proper elementary extension by Diag_el(𝔑) plus c > n for every numeral, since every finite subset is satisfied in 𝔑 itself); the upward Löwenheim-Skolem theorem by adjoining κ distinct constants to Diag_el(M); the Łoś-Vaught test — a satisfiable L-theory T with no finite models that is κ-categorical for some κ ≥ |L| is complete (if T were not complete it would have two non-elementarily-equivalent models, hence by Löwenheim-Skolem two non-isomorphic models of size κ, contradicting κ-categoricity), with the standard corollaries that ACF_p and DLO and the theory of the random graph and infinite-dimensional vector spaces over a fixed field are complete and decidable; elementary amalgamation (two elementary extensions of a common M can be amalgamated over M) and the joint embedding property for a complete theory.
Chang, C. C. and Keisler, H. J. — Model Theory · Studies in Logic and the Foundations of Mathematics 73, 3rd edition, North-Holland (1990), Chapters 2-6. The systematic source for the diagram method and its compactness deployments. Develops the consistency/diagram dictionary in full: models of D(M) (atomic diagram) are exactly the structures with an embedding of M, models of the elementary diagram are exactly those with an elementary embedding. Proves the Robinson joint consistency theorem: if T_1 and T_2 are theories in languages L_1, L_2 with L_0 = L_1 ∩ L_2, T_1 ∪ T_2 is consistent iff there is no L_0-sentence σ with T_1 ⊢ σ and T_2 ⊢ ¬σ (equivalently T_1 and T_2 have a common L_0-complete extension), by an alternating elementary-chain amalgamation over the L_0-reducts. Derives Craig's interpolation theorem (if ⊨ φ → ψ then there is an interpolant θ in the common vocabulary with ⊨ φ → θ and ⊨ θ → ψ) from Robinson consistency, and the Beth definability theorem (implicit definability equals explicit definability) from interpolation. Presents the ultraproduct construction and Łoś's fundamental theorem (a first-order formula holds of a tuple in ∏_U M_i iff the set of indices where it holds in M_i lies in the ultrafilter U) as the alternative, calculus-free proof of compactness and as a model-construction tool: the ultrapower M^I/U is an elementary extension of M (the diagonal embedding is elementary by Łoś), ℝ* = ℝ^ℕ/U is the hyperreals, and the Keisler-Shelah theorem states M ≡ N iff some ultrapowers M^I/U ≅ N^I/U are isomorphic (the ultrapower characterization of elementary equivalence). The Łoś-Tarski preservation theorem (a theory is preserved under substructures iff Π_1-axiomatizable), the Chang-Łoś-Suszko theorem (preserved under unions of chains iff Π_2-axiomatizable), and the Łoś-Vaught completeness test.
Robinson, A. — A result on consistency and its application to the theory of definition · Indagationes Mathematicae 18 (1956), pp. 47-58. Robinson's joint consistency theorem and the model-theoretic theory of definition. The joint consistency theorem: for theories T_1 ⊇ T (in L_1) and T_2 ⊇ T (in L_2) with T a complete theory in the common language L_0 = L_1 ∩ L_2, T_1 ∪ T_2 is consistent. The general form drops completeness of T to the condition that no L_0-sentence is proved by one side and refuted by the other. Robinson's proof is the prototype diagram-and-compactness amalgamation: build an elementary chain M_0 ≼ M_1 ≼ ⋯ alternating between models of T_1 and T_2, at each stage realizing the elementary diagram of the previous model over the shared L_0-reduct using compactness and the completeness/consistency hypothesis on L_0, and take the union, whose L_1- and L_2-reducts model T_1 and T_2 respectively. The paper applies the theorem to definability: Beth's theorem that a predicate implicitly defined by a theory (any two expansions of a model agreeing on the old vocabulary agree on the new predicate) is explicitly definable (the theory proves the predicate equivalent to an old-vocabulary formula).
Craig, W. — Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory · Journal of Symbolic Logic 22 (1957), pp. 269-285. Craig's interpolation theorem: if φ and ψ are first-order sentences with ⊨ φ → ψ, then there is an interpolant θ whose non-logical vocabulary is contained in the common vocabulary of φ and ψ (the relation, function, and constant symbols occurring in both) such that ⊨ φ → θ and ⊨ θ → ψ; the degenerate cases where φ is unsatisfiable or ψ valid are handled by ⊥ and ⊤. Craig gave a proof-theoretic derivation from Gentzen's cut-elimination / the Herbrand-Gentzen theorem; the model-theoretic proof routes through Robinson's joint consistency theorem (no interpolant ⇒ the deductively-closed theories generated by φ and by ¬ψ in the common language are jointly consistent over their L_0-intersection ⇒ a model of φ ∧ ¬ψ, contradiction). The paper draws the consequence, refined by Beth and Robinson, that interpolation yields the equivalence of implicit and explicit definability — the Beth definability theorem — establishing the model-theoretic theory of definition as a corollary of interpolation.

Estimated time

beginner: 20m
intermediate: 54m
master: 90m