2.6.2: Outline of the Proof

\(\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} } }\)

The proof of the completeness theorem is a bit complex, and upon first reading it, it is easy to get lost. So let us outline the proof. The first step is a shift of perspective, that allows us to see a route to a proof. When completeness is thought of as “whenever \(\Gamma \Entails A\) then \(\Gamma \Proves A\),” it may be hard to even come up with an idea: for to show that \(\Gamma \Proves A\) we have to find a derivation, and it does not look like the hypothesis that \(\Gamma \Entails A\) helps us for this in any way. For some proof systems it is possible to directly construct a derivation, but we will take a slightly different approach. The shift in perspective required is this: completeness can also be formulated as: “if \(\Gamma\) is consistent, it is satisfiable.” Perhaps we can use the information in \(\Gamma\) together with the hypothesis that it is consistent to construct a structure that satisfies every sentence in \(\Gamma\). After all, we know what kind of structure we are looking for: one that is as \(\Gamma\) describes it!

If \(\Gamma\) contains only atomic sentences, it is easy to construct a model for it. Suppose the atomic sentences are all of the form \(\Atom{P}{a_1,\dots,a_n}\) where the \(a_i\) are constant symbols. All we have to do is come up with a domain \(\Domain{M}\) and an assignment for \(P\) so that \(\Sat{M}{\Atom{P}{a_1,\ldots,a_n}}\). But that’s not very hard: put \(\Domain{M} = \Nat\), \(\Assign{\Obj c_i}{M} = i\), and for every \(\Atom{P}{a_1,\ldots,a_n} \in \Gamma\), put the tuple \(\tuple{k_1, \dots, k_n}\) into \(\Assign{P}{M}\), where \(k_i\) is the index of the constant symbol \(a_i\) (i.e., \(a_i \ident \Obj c_{k_i}\)).

Now suppose \(\Gamma\) contains some formula \(\lnot B\), with \(B\) atomic. We might worry that the construction of \({\Struct{M}}\) interferes with the possibility of making \(\lnot B\) true. But here’s where the consistency of \(\Gamma\) comes in: if \(\lnot B \in \Gamma\), then \(B \notin \Gamma\), or else \(\Gamma\) would be inconsistent. And if \(B \notin \Gamma\), then according to our construction of \({\Struct{M}}\), \(\SatN{M}{B}\), so \(\Sat{M}{\lnot B}\). So far so good.

What if \(\Gamma\) contains complex, non-atomic formulas? Say it contains \(A \land B\). To make that true, we should proceed as if both \(A\) and \(B\) were in \(\Gamma\). And if \(A \lor B \in \Gamma\), then we will have to make at least one of them true, i.e., proceed as if one of them was in \(\Gamma\).

This suggests the following idea: we add additional formulas to \(\Gamma\) so as to (a) keep the resulting set consistent and (b) make sure that for every possible atomic sentence \(A\), either \(A\) is in the resulting set, or \(\lnot A\) is, and (c) such that, whenever \(A \land B\) is in the set, so are both \(A\) and \(B\), if \(A \lor B\) is in the set, at least one of \(A\) or \(B\) is also, etc. We keep doing this (potentially forever). Call the set of all formulas so added \(\Gamma^*\). Then our construction above would provide us with a structure \(\Struct{M}\) for which we could prove, by induction, that it satisfies all sentences in \(\Gamma^*\), and hence also all sentence in \(\Gamma\) since \(\Gamma \subseteq \Gamma^*\). It turns out that guaranteeing (a) and (b) is enough. A set of sentences for which (b) holds is called complete. So our task will be to extend the consistent set \(\Gamma\) to a consistent and complete set \(\Gamma^*\).

There is one wrinkle in this plan: if \(\lexists{x}{A(x)} \in \Gamma\) we would hope to be able to pick some constant symbol \(c\) and add \(A(c)\) in this process. But how do we know we can always do that? Perhaps we only have a few constant symbols in our language, and for each one of them we have \(\lnot A(c) \in \Gamma\). We can’t also add \(A(c)\), since this would make the set inconsistent, and we wouldn’t know whether \(\Struct{M}\) has to make \(A(c)\) or \(\lnot A(c)\) true. Moreover, it might happen that \(\Gamma\) contains only sentences in a language that has no constant symbols at all (e.g., the language of set theory).

The solution to this problem is to simply add infinitely many constants at the beginning, plus sentences that connect them with the quantifiers in the right way. (Of course, we have to verify that this cannot introduce an inconsistency.)

Our original construction works well if we only have constant symbols in the atomic sentences. But the language might also contain function symbols. In that case, it might be tricky to find the right functions on \(\Nat\) to assign to these function symbols to make everything work. So here’s another trick: instead of using \(i\) to interpret \(\Obj c_i\), just take the set of constant symbols itself as the domain. Then \(\Struct M\) can assign every constant symbol to itself: \(\Assign{\Obj c_i}{M} = \Obj c_i\). But why not go all the way: let \(\Domain{M}\) be all terms of the language! If we do this, there is an obvious assignment of functions (that take terms as arguments and have terms as values) to function symbols: we assign to the function symbol \(\Obj f^n_i\) the function which, given \(n\) terms \(t_1\), …, \(t_n\) as input, produces the term \(\Obj f^n_i(t_1, \dots, t_n)\) as value.

The last piece of the puzzle is what to do with \(\eq[][]\). The predicate symbol \(\eq[][]\) has a fixed interpretation: \(\Sat{M}{\eq[t][t']}\) iff \(\Value{t}{M} = \Value{t'}{M}\). Now if we set things up so that the value of a term \(t\) is \(t\) itself, then this structure will make no sentence of the form \(\eq[t][t']\) true unless \(t\) and \(t'\) are one and the same term. And of course this is a problem, since basically every interesting theory in a language with function symbols will have as theorems sentences \(\eq[t][t']\) where \(t\) and \(t'\) are not the same term (e.g., in theories of arithmetic: \(\eq[(\Obj 0+ \Obj 0)][\Obj 0]\)). To solve this problem, we change the domain of \(\Struct M\): instead of using terms as the objects in \(\Domain{M}\), we use sets of terms, and each set is so that it contains all those terms which the sentences in \(\Gamma\) require to be equal. So, e.g., if \(\Gamma\) is a theory of arithmetic, one of these sets will contain: \(\Obj 0\), \((\Obj 0 + \Obj 0)\), \((\Obj 0 \times \Obj 0)\), etc. This will be the set we assign to \(\Obj 0\), and it will turn out that this set is also the value of all the terms in it, e.g., also of \((\Obj 0 + \Obj 0)\). Therefore, the sentence \(\eq[(\Obj 0+ \Obj 0)][\Obj 0]\) will be true in this revised structure.

So here’s what we’ll do. First we investigate the properties of complete consistent sets, in particular we prove that a complete consistent set contains \(A \land B\) iff it contains both \(A\) and \(B\), \(A \lor B\) iff it contains at least one of them, etc. (Proposition 10.3.1). Then we define and investigate “saturated” sets of sentences. A saturated set is one which contains conditionals that link each quantified sentence to instances of it (Definition 10.4.2). We show that any consistent set \(\Gamma\) can always be extended to a saturated set \(\Gamma'\) (Lemma 10.4.1). If a set is consistent, saturated, and complete it also has the property that it contains \(\lexists{x}{A(x)}\) iff it contains \(A(t)\) for some closed term \(t\) and \(\lforall{x}{A(x)}\) iff it contains \(A(t)\) for all closed terms \(t\) (Proposition 10.4.2). We’ll then take the saturated consistent set \({\Gamma'}\) and show that it can be extended to a saturated, consistent, and complete set \(\Gamma^*\) (Lemma 10.5.1). This set \(\Gamma^*\) is what we’ll use to define our term model \(\Struct M(\Gamma^*)\). The term model has the set of closed terms as its domain, and the interpretation of its predicate symbols is given by the atomic sentences in \(\Gamma^*\) (Definition 10.6.1). We’ll use the properties of saturated, complete consistent sets to show that indeed \(\Sat{M(\Gamma^*)}{A}\) iff \(A \in \Gamma^*\) (Lemma 10.6.1), and thus in particular, \(\Sat{M(\Gamma^*)}{\Gamma}\). Finally, we’ll consider how to define a term model if \(\Gamma\) contains \(\eq[][]\) as well (Definition 10.7.3) and show that it satisfies \(\Gamma^*\) (Lemma 10.7.1).