2.6.9: The Compactness Theorem

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

One important consequence of the completeness theorem is the compactness theorem. The compactness theorem states that if each finite subset of a set of sentences is satisfiable, the entire set is satisfiable—even if the set itself is infinite. This is far from obvious. There is nothing that seems to rule out, at first glance at least, the possibility of there being infinite sets of sentences which are contradictory, but the contradiction only arises, so to speak, from the infinite number. The compactness theorem says that such a scenario can be ruled out: there are no unsatisfiable infinite sets of sentences each finite subset of which is satisfiable. Like the completeness theorem, it has a version related to entailment: if an infinite set of sentences entails something, already a finite subset does.

Definition \(\PageIndex{1}\)

A set \(\Gamma\) of formulas is finitely satisfiable if and only if every finite \(\Gamma_0 \subseteq \Gamma\) is satisfiable.

Theorem \(\PageIndex{1}\): Compactness Theorem

The following hold for any sentences \(\Gamma\) and \(A\):

1. \(\Gamma \Entails A\) iff there is a finite \(\Gamma_0 \subseteq \Gamma\) such that \(\Gamma_0 \Entails A\).
2. \(\Gamma\) is satisfiable if and only if it is finitely satisfiable.

Proof. We prove (2). If \(\Gamma\) is satisfiable, then there is a structure \(\Struct{M}\) such that \(\Sat{M}{A}\) for all \(A \in \Gamma\). Of course, this \({\Struct{M}}\) also satisfies every finite subset of \(\Gamma\), so \(\Gamma\) is finitely satisfiable.

Now suppose that \(\Gamma\) is finitely satisfiable. Then every finite subset \(\Gamma_0 \subseteq \Gamma\) is satisfiable. By soundness (Corollaries 9.11.2 and 8.12.3), every finite subset is consistent. Then \(\Gamma\) itself must be consistent by Propositions 8.8.5 and 9.7.5. By completeness (Theorem 10.8.1), since \(\Gamma\) is consistent, it is satisfiable. ◻

Problem \(\PageIndex{1}\)

Prove (1) of Theorem \(\PageIndex{1}\).

Example \(\PageIndex{1}\)

In every model \(\Struct{M}\) of a theory \(\Gamma\), each term \(t\) of course picks out an element of \(\Domain{M}\). Can we guarantee that it is also true that every element of \(\Domain{M}\) is picked out by some term or other? In other words, are there theories \(\Gamma\) all models of which are covered? The compactness theorem shows that this is not the case if \(\Gamma\) has infinite models. Here’s how to see this: Let \(\Struct{M}\) be an infinite model of \(\Gamma\), and let \(c\) be a constant symbol not in the language of \(\Gamma\). Let \(\Delta\) be the set of all sentences \(\eqN[c][t]\) for \(t\) a term in the language \(\Lang{L}\) of \(\Gamma\), i.e., \[\Delta = \Setabs{\eqN[c][t]}{t \in \Trm[L]}.\nonumber\] A finite subset of \(\Gamma \cup \Delta\) can be written as \(\Gamma' \cup \Delta'\), with \(\Gamma' \subseteq \Gamma\) and \(\Delta' \subseteq \Delta\). Since \(\Delta'\) is finite, it can contain only finitely many terms. Let \(a \in \Domain{M}\) be an element of \(\Domain{M}\) not picked out by any of them, and let \(\Struct{M'}\) be the structure that is just like \(\Struct{M}\), but also \(\Assign{c}{M'} = a\). Since \(a \neq \Value{t}{M}\) for all \(t\) occuring in \(\Delta'\), \(\Sat{M'}{\Delta'}\). Since \(\Sat{M}{\Gamma}\), \(\Gamma' \subseteq \Gamma\), and \(c\) does not occur in \(\Gamma\), also \(\Sat{M'}{\Gamma'}\). Together, \(\Sat{M'}{\Gamma' \cup \Delta'}\) for every finite subset \(\Gamma' \cup \Delta'\) of \(\Gamma \cup \Delta\). So every finite subset of \(\Gamma \cup \Delta\) is satisfiable. By compactness, \(\Gamma \cup \Delta\) itself is satisfiable. So there are models \(\Sat{M}{\Gamma \cup \Delta}\). Every such \(\Struct{M}\) is a model of \(\Gamma\), but is not covered, since \(\Value{c}{M} \neq \Value{t}{M}\) for all terms \(t\) of \(\Lang{L}\).

Example \(\PageIndex{2}\)

Consider a language \(\Lang{L}\) containing the predicate symbol \(<\), constant symbols \(\Obj{0}\), \(\Obj{1}\), and function symbols \(+\), \(\times\), \(-\), \(\div\). Let \(\Gamma\) be the set of all sentences in this language true in \(\Struct{Q}\) with domain \(\Rat\) and the obvious interpretations. \(\Gamma\) is the set of all sentences of \(\Lang{L}\) true about the rational numbers. Of course, in \(\Rat\) (and even in \(\Real\)), there are no numbers which are greater than \(0\) but less than \(1/k\) for all \(k \in \PosInt\). Such a number, if it existed, would be an infinitesimal: non-zero, but infinitely small. The compactness theorem shows that there are models of \(\Gamma\) in which infinitesimals exist: Let \(\Delta\) be \(\{0<c\} \cup \Setabs{c < (\Obj{1} \div \num{k})}{k \in \PosInt}\) (where \(\num{k} = (\Obj{1} + (\Obj{1} + \dots + (\Obj{1} + \Obj{1})\dots))\) with \(k\) \(\Obj{1}\)’s). For any finite subset \(\Delta_0\) of \(\Delta\) there is a \(K\) such that all the sentences \(c < (\Obj{1} \div \num{k})\) in \(\Delta_0\) have \(k < K\). If we expand \(\Struct{Q}\) to \(\Struct{Q'}\) with \(\Assign{c}{Q'} = 1/K\) we have that \(\Sat{Q'}{\Gamma \cup \Delta_0}\), and so \(\Gamma \cup \Delta\) is finitely satisfiable (Exercise: prove this in detail). By compactness, \(\Gamma \cup \Delta\) is satisfiable. Any model \(\Struct{S}\) of \(\Gamma \cup \Delta\) contains an infinitesimal, namely \(\Assign{c}{S}\).

Problem \(\PageIndex{2}\)

In the standard model of arithmetic \(\Struct{N}\), there is no element \(k \in \Domain{N}\) which satisfies every formula \(\num{n} < x\) (where \(\num{n}\) is \(\Obj{0}^{\prime\dots\prime}\) with \(n\) \(\prime\)’s). Use the compactness theorem to show that the set of sentences in the language of arithmetic which are true in the standard model of arithmetic \(\Struct{N}\) are also true in a structure \(\Struct{N'}\) that contains an element which does satisfy every formula \(\num{n} < x\).

Example \(\PageIndex{3}\)

We know that first-order logic with identity predicate can express that the size of the domain must have some minimal size: The sentence \(A_{\ge n}\) (which says “there are at least \(n\) distinct objects”) is true only in structures where \(\Domain{M}\) has at least \(n\) objects. So if we take \[\Delta = \Setabs{A_{\ge n}}{n \ge 1}\nonumber\] then any model of \(\Delta\) must be infinite. Thus, we can guarantee that a theory only has infinite models by adding \(\Delta\) to it: the models of \(\Gamma \cup \Delta\) are all and only the infinite models of \(\Gamma\).

So first-order logic can express infinitude. The compactness theorem shows that it cannot express finitude, however. For suppose some set of sentences \(\Lambda\) were satisfied in all and only finite structures. Then \(\Delta \cup \Lambda\) is finitely satisfiable. Why? Suppose \(\Delta' \cup \Lambda' \subseteq \Delta \cup \Lambda\) is finite with \(\Delta' \subseteq \Delta\) and \(\Lambda' \subseteq \Lambda\). Let \(n\) be the largest number such that \(A_{\ge n} \in \Delta'\). \(\Lambda\), being satisfied in all finite structures, has a model \(\Struct{M}\) with finitely many but \(\ge n\) elements. But then \(\Sat{M}{\Delta' \cup \Lambda'}\). By compactness, \(\Delta \cup \Lambda\) has an infinite model, contradicting the assumption that \(\Lambda\) is satisfied only in finite structures.