2.6.10: A Direct Proof of 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} } }\)

We can prove the Compactness Theorem directly, without appealing to the Completeness Theorem, using the same ideas as in the proof of the completeness theorem. In the proof of the Completeness Theorem we started with a consistent set \(\Gamma\) of sentences, expanded it to a consistent, saturated, and complete set \(\Gamma^*\) of sentences, and then showed that in the term model \(\Struct{M(\Gamma^*)}\) constructed from \(\Gamma^*\), all sentences of \(\Gamma\) are true, so \(\Gamma\) is satisfiable.

We can use the same method to show that a finitely satisfiable set of sentences is satisfiable. We just have to prove the corresponding versions of the results leading to the truth lemma where we replace “consistent” with “finitely satisfiable.”

Proposition \(\PageIndex{1}\)

Suppose \(\Gamma\) is complete and finitely satisfiable. Then:

1. \((A \land B) \in \Gamma\) iff both \(A \in \Gamma\) and \(B \in \Gamma\).
2. \((A \lor B) \in \Gamma\) iff either \(A \in \Gamma\) or \(B \in \Gamma\).
3. \((A \lif B) \in \Gamma\) iff either \(A \notin \Gamma\) or \(B \in \Gamma\).

Problem \(\PageIndex{1}\)

Prove Proposition \(\PageIndex{1}\). Avoid the use of \(\Proves\).

Lemma \(\PageIndex{1}\)

Every finitely satisfiable set \(\Gamma\) can be extended to a saturated finitely satisfiable set \(\Gamma'\).

Problem \(\PageIndex{2}\)

Prove Lemma \(\PageIndex{1}\). (Hint: The crucial step is to show that if \(\Gamma_n\) is finitely satisfiable, so is \(\Gamma_n \cup \{D_n\}\), without any appeal to derivations or consistency.)

Proposition \(\PageIndex{2}\)

Suppose \(\Gamma\) is complete, finitely satisfiable, and saturated.

1. \(\lexists{x}{A(x)} \in \Gamma\) iff \(A(t) \in \Gamma\) for at least one closed term \(t\).
2. \(\lforall{x}{A(x)} \in \Gamma\) iff \(A(t) \in \Gamma\) for all closed terms \(t\).

Problem \(\PageIndex{3}\)

Prove Proposition \(\PageIndex{2}\).

Lemma \(\PageIndex{2}\)

Every finitely satisfiable set \(\Gamma\) can be extended to a complete and finitely satisfiable set \(\Gamma^*\).

Problem \(\PageIndex{4}\)

Prove Lemma \(\PageIndex{2}\). (Hint: the crucial step is to show that if \(\Gamma_n\) is finitely satisfiable, then either \(\Gamma_n \cup \{A_n\}\) or \(\Gamma_n \cup \{\lnot A_n\}\) is finitely satisfiable.)

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

\(\Gamma\) is satisfiable if and only if it is finitely satisfiable.

Proof. 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. By Lemma \(\PageIndex{1}\), there is a finitely satisfiable, saturated set \(\Gamma' \supseteq \Gamma\). By Lemma \(\PageIndex{2}\), \({\Gamma'}\) can be extended to a complete and finitely satisfiable set \(\Gamma^*\), and \(\Gamma^*\) is still saturated. Construct the term model \(\Struct{M(\Gamma^*)}\) as in Definition 10.6.1. Note that Proposition 10.6.1 did not rely on the fact that \(\Gamma^*\) is consistent (or complete or saturated, for that matter), but just on the fact that \(\Struct{M(\Gamma^*)}\) is covered. The proof of the Truth Lemma (Lemma 10.6.1) goes through if we replace references to Proposition 10.3.1 and Proposition 10.4.2 by references to Proposition \(\PageIndex{1}\) and Proposition \(\PageIndex{2}\). ◻

Problem \(\PageIndex{5}\)

Write out the complete proof of the Truth Lemma (Lemma 10.6.1) in the version required for the proof of Theorem \(\PageIndex{1}\).