Model theory

This is startling: $\Sigma$ can be infinite, even encoding infinitely many constraints, yet consistency need only be checked finitely many constraints at a time. It is the bridge from finitary proof (a formal derivation is always a finite object) to infinitary semantics (a model can be infinite), and it is the single theorem responsible for the existence of infinite and nonstandard models throughout model theory.

We prove the contrapositive: if $\Sigma$ has no model, then some finite $\Sigma_0 \subseteq \Sigma$ has no model.

Suppose $\Sigma$ is unsatisfiable. By Gödel's Completeness Theorem for first-order logic (semantic entailment coincides with syntactic derivability: $\Sigma \models \bot$ iff $\Sigma \vdash \bot$), $\Sigma$ being unsatisfiable is equivalent to $\Sigma$ being syntactically inconsistent, i.e. $\Sigma \vdash \bot$ — a contradiction is formally derivable from $\Sigma$.

A formal derivation is by definition a finite sequence of formulas, each justified by an axiom, a premise from $\Sigma$, or an inference rule applied to earlier lines. Since the derivation of $\bot$ is finite, it cites only finitely many premises from $\Sigma$; collect them into a finite set $\Sigma_0 = \{\sigma_1, \dots, \sigma_n\} \subseteq \Sigma$.

The very same finite derivation, using only premises from $\Sigma_0$, witnesses $\Sigma_0 \vdash \bot$. By soundness of first-order logic (derivability implies entailment), $\Sigma_0 \models \bot$, i.e. $\Sigma_0$ is unsatisfiable — it has no model.

So we have produced a finite $\Sigma_0 \subseteq \Sigma$ with no model, proving the contrapositive. Equivalently: if every finite subset of $\Sigma$ has a model, no such inconsistent finite derivation can exist, so $\Sigma$ cannot be unsatisfiable, hence $\Sigma$ has a model.

This shows first-order logic cannot pin down cardinality: any theory with an infinite model (e.g. the axioms of a field, of set theory, ...) already has a countable model, no matter how "big" the original model was built to be. Combined with the upward version (any infinite model has elementary extensions of every larger cardinality), this is the source of Skolem's Paradox — a countable structure can satisfy the same first-order sentences as an uncountable one, including sentences that "assert" uncountability from the inside.

We build $N$ as the union of a countable increasing chain of countable subsets of $M$, using the Tarski–Vaught test: a subset $N \subseteq M$ (as a substructure) is elementary iff for every $\mathcal{L}$-formula $\psi(x, \bar{y})$ and every tuple $\bar{a}$ from $N$, if there is some $b \in M$ with $\mathcal{M} \models \psi(b, \bar{a})$, then there is already such a witness $b \in N$.

Since $\mathcal{L}$ is countable, there are only countably many formulas $\psi(x,\bar y)$. Start with any countably infinite $X_0 \subseteq M$ (possible since $M$ is infinite). Given a countable $X_n$, for each formula $\psi(x,\bar y)$ and each tuple $\bar a$ from $X_n$ (still only countably many pairs, since $X_n$ is countable and $\mathcal{L}$ is countable), if $\exists b \in M\, \mathcal{M} \models \psi(b,\bar a)$, choose one such witness $b$ (using the Axiom of Choice) and add it to form $X_{n+1}$; this adds only countably many new elements, so $X_{n+1}$ stays countable.

Let $N = \bigcup_{n<\omega} X_n$; a countable union of countable sets, so $N$ is countable (and infinite, since $X_0 \subseteq N$). We check the Tarski–Vaught test for $N$: given $\psi(x,\bar y)$ and $\bar a$ from $N$, since $\bar a$ is a finite tuple it lies entirely in some single $X_n$ (the chain is increasing); if a witness $b \in M$ exists for $\psi(b, \bar a)$, then by construction of $X_{n+1}$, a witness was already chosen and placed into $X_{n+1} \subseteq N$.

By the Tarski–Vaught test, $N$ (with the induced $\mathcal{L}$-structure $\mathcal{N}$) satisfies $\mathcal{N} \preceq \mathcal{M}$. Elementary substructures satisfy exactly the same sentences as the ambient structure, so $\mathcal{N}$ is a countably infinite model witnessing the theorem.