The Completeness Theorem

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

How to use Read

This page follows First-Order Completeness in source order. Every one of the 832 formula occurrences is native, unflattened MathML with a stable source pin. The companion Listen page is a reviewed words-only stream.

5 disclosed reader corrections

The frozen source remains unchanged; each reviewed reader intervention is disclosed at the affected material.

SAR-002: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. Open affected formula.
TR024-SOURCE-FORMULA-001: The frozen source has two consecutive commas in the first function-term argument list. The reader removes the extra comma; the source formula and source MathML remain available for comparison. Open affected formula.
TR024-SOURCE-PROSE-001: The frozen source calls both Gamma and A sentences, although the theorem uses Gamma as a set of sentences. The reader supplies the missing type distinction; the source line is unchanged. Open affected formula.
TR024-SOURCE-PROSE-002: The frozen sentence combines 'for all' with 'have' and has no grammatical subject for the bound. The reader states that every displayed inequality in the finite subset has index k below K; the source is unchanged. Open affected formula.
TR024-SOURCE-SELECTION-001: The frozen conditional assigns this sentence's period to its unused non-first-order branch. The reader restores the terminal period after the FOL replacement list; the source is unchanged. Applies to reference reference-000484.

Introduction

The completeness theorem is one of the most fundamental results about logic. It comes in two formulations, the equivalence of which we'll prove. In its first formulation it says something fundamental about the relationship between semantic consequence and our derivation system: if a sentence $A$ source 19 follows from some sentences $Γ$ source 20, then there is also a derivation that establishes $Γ ⊢ A$ source 20. Thus, the derivation system is as strong as it can possibly be without proving things that don't actually follow.

In its second formulation, it can be stated as a model existence result: every consistent set of sentences is satisfiable. Consistency is a proof-theoretic notion: it says that our derivation system is unable to produce certain derivations. But who's to say that just because there are no derivations of a certain sort from $Γ$ source 29, it's guaranteed that there is a structure $M$ source 30? Before the completeness theorem was first proved—in fact before we had the derivation systems we now do—the great German mathematician David Hilbert held the view that consistency of mathematical theories guarantees the existence of the objects they are about. He put it as follows in a letter to Gottlob Frege:

If the arbitrarily given axioms do not contradict one another with all their consequences, then they are true and the things defined by the axioms exist. This is for me the criterion of truth and existence.

Frege vehemently disagreed. The second formulation of the completeness theorem shows that Hilbert was right in at least the sense that if the axioms are consistent, then some structure exists that makes them all true.

These aren't the only reasons the completeness theorem—or rather, its proof—is important. It has a number of important consequences, some of which we'll discuss separately. For instance, since any derivation that shows $Γ ⊢ A$ source 52 is finite and so can only use finitely many of the sentences in $Γ$ source 53, it follows by the completeness theorem that if $A$ source 54 is a consequence of $Γ$ source 54, it is already a consequence of a finite subset of $Γ$ source 55. This is called compactness. Equivalently, if every finite subset of $Γ$ source 57 is consistent, then $Γ$ source 57 itself must be consistent.

Although the compactness theorem follows from the completeness theorem via the detour through derivations, it is also possible to use the the proof of the completeness theorem to establish it directly. For what the proof does is take a set of sentences with a certain property—consistency—and constructs a structure out of this set that has certain properties (in this case, that it satisfies the set). Almost the very same construction can be used to directly establish compactness, by starting from “finitely satisfiable” sets of sentences instead of consistent ones. The construction also yields other consequences, e.g., that any satisfiable set of sentences has a finite or denumerables model. (This result is called the Löwenheim–Skolem theorem.) In general, the construction of structures from sets of sentences is used often in logic, and sometimes even in philosophy.

Outline of the Proof

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 $Γ ⊨ A$ source 18 then $Γ ⊢ A$ source 19,” it may be hard to even come up with an idea: for to show that $Γ ⊢ A$ source 20 we have to find a derivation, and it does not look like the hypothesis that $Γ ⊨ A$ source 22 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 $Γ$ source 26 is consistent, it is satisfiable.” Perhaps we can use the information in $Γ$ source 27 together with the hypothesis that it is consistent to construct a structure that satisfies every sentence in $Γ$ source 30. After all, we know what kind of structure we are looking for: one that is as $Γ$ source 32 describes it!

If $Γ$ source 34 contains only atomic sentences, it is easy to construct a model for it. Suppose the atomic sentences are all of the form $P (a_{1}, \dots, a_{n})$ source 37 where the $a_{i}$ source 37 are constants. All we have to do is come up with

a domain $| M |$ source 40 and an assignment for $P$ source 40 so that $M ⊨ P (a_{1}, \dots, a_{n})$ source 41. But that's not very hard: put $| M | = ℕ$ source 42, ${c_{i}}^{M} = i$ source 42, and for every $P (a_{1}, \dots, a_{n}) \in Γ$ source 43, put the tuple $⟨ k_{1}, \dots, k_{n} ⟩$ source 43 into $P^{M}$ source 44, where $k_{i}$ source 44 is the index of the constant symbol $a_{i}$ source 45 (i.e., $a_{i} \equiv c_{k_{i}}$ source 45).

Now suppose $Γ$ source 49 contains some formula $\neg B$ source 49, with $B$ source 49 atomic. We might worry that the construction of $M$ source 51 interferes with the possibility of making $\neg B$ source 52 true. But here's where the consistency of $Γ$ source 53 comes in: if $\neg B \in Γ$ source 53, then $B \notin Γ$ source 53, or else $Γ$ source 54 would be inconsistent. And if $B \notin Γ$ source 54, then according to our construction of $M$ source 56, $M ⊭ B$ source 57, so $M ⊨ \neg B$ source 58. So far so good.

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

This suggests the following idea: we add additional formulas to $Γ$ source 67 so as to (a) keep the resulting set consistent and (b) make sure that for every possible atomic sentence $A$ source 68, either $A$ source 69 is in the resulting set, or $\neg A$ source 69 is, and (c) such that, whenever $A \land B$ source 70 is in the set, so are both $A$ source 70 and $B$ source 70, if $A \lor B$ source 71 is in the set, at least one of $A$ source 71 or $B$ source 71 is also, etc. We keep doing this (potentially forever). Call the set of all formulas so added $Γ^{*}$ source 73. Then our construction above would provide us with a structure $M$ source 74 for which we could prove, by induction, that it satisfies all sentences in $Γ^{*}$ source 76, and hence also all sentence in $Γ$ source 76 since $Γ \subseteq Γ^{*}$ source 77. 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 $Γ$ source 80 to a consistent and complete set $Γ^{*}$ source 80.

There is one wrinkle in this plan: if $\exists x A (x) \in Γ$ source 83 we would hope to be able to pick some constant $c$ source 84 and add $A (c)$ source 84 in this process. But how do we know we can always do that? Perhaps we only have a few constants in our language, and for each one of them we have $\neg A (c) \in Γ$ source 87. We can't also add $A (c)$ source 87, since this would make the set inconsistent, and we wouldn't know whether $M$ source 89 has to make $A (c)$ source 89 or $\neg A (c)$ source 89 true. Moreover, it might happen that $Γ$ source 90 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 constants in the atomic sentences. But the language might also contain functions. In that case, it might be tricky to find the right functions on $ℕ$ source 102 to assign to these functions to make everything work. So here's another trick: instead of using $i$ source 103 to interpret $c_{i}$ source 104, just take the set of constants itself as the domain. Then $M$ source 105 can assign every constant to itself: ${c_{i}}^{M} = c_{i}$ source 106. But why not go all the way: let $| M |$ source 107 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 functions: we assign to the function ${f^{n}}_{i}$ source 110 the function which, given $n$ source 110 terms $t_{1}$ source 110, and so on, $t_{n}$ source 111 as input, produces the term ${f^{n}}_{i} (t_{1}, \dots, t_{n})$ source 111 as value.

The last piece of the puzzle is what to do with $=$ source 114. The predicate $=$ source 115 has a fixed interpretation: $M ⊨ t = t^{'}$ source 115 iff ${⟦ t ⟧}^{M} = {⟦ t^{'} ⟧}^{M}$ source 116. Now if we set things up so that the value of a term $t$ source 117 is $t$ source 117 itself, then this structure will make no sentence of the form $t = t^{'}$ source 118 true unless $t$ source 119 and $t^{'}$ source 119 are one and the same term. And of course this is a problem, since basically every interesting theory in a language with functions will have as theorems sentences $t = t^{'}$ source 122 where $t$ source 122 and $t^{'}$ source 122 are not the same term (e.g., in theories of arithmetic: $(0 + 0) = 0$ source 123). To solve this problem, we change the domain of $M$ source 124: instead of using terms as the objects in $| M |$ source 125, we use sets of terms, and each set is so that it contains all those terms which the sentences in $Γ$ source 126 require to be equal. So, e.g., if $Γ$ source 127 is a theory of arithmetic, one of these sets will contain: $0$ source 128, $(0 + 0)$ source 128, $(0 \times 0)$ source 128, etc. This will be the set we assign to $0$ source 129, and it will turn out that this set is also the value of all the terms in it, e.g., also of $(0 + 0)$ source 131. Therefore, the sentence $(0 + 0) = 0$ source 132 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$ source 137 iff it contains both $A$ source 138 and $B$ source 138, $A \lor B$ source 138 iff it contains at least one of them, etc. (Reference to the proposition characterizing complete consistent sets). 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 (Reference to the definition of the Henkin witness sentences). We show that any consistent set $Γ$ source 143 can always be extended to a saturated set $Γ^{'}$ source 144 (Reference to the Henkin saturation extension lemma). If a set is consistent, saturated, and complete it also has the property that it contains $\exists x A (x)$ source 146 iff it contains $A (t)$ source 146 for some closed term $t$ source 147 and $\forall x A (x)$ source 148 iff it contains $A (t)$ source 148 for all closed terms $t$ source 149 (Reference to the proposition characterizing quantifiers in a saturated set). We'll then take the saturated consistent set $Γ^{'}$ source 151 and show that it can be extended to a saturated, consistent, and complete set $Γ^{*}$ source 153 (Reference to Lindenbaum's extension lemma). This set $Γ^{*}$ source 154 is what we'll use to define our term model $M (Γ^{*})$ source 155. The term model has the set of closed terms as its domain, and the interpretation of its predicates is given by the atomic sentences in $Γ^{*}$ source 159 (Reference to the definition of the term model). We'll use the properties of saturated, complete consistent sets to show that indeed $M (Γ^{*}) ⊨ A$ source 162 iff $A \in Γ^{*}$ source 162 (Reference to the term-model Truth Lemma without identity), and thus in particular, $M (Γ^{*}) ⊨ Γ$ source 164. Finally, we'll consider how to define a term model if $Γ$ source 166 contains $=$ source 166 as well (Reference to the definition of the factored term model) and show that it satisfies $Γ^{*}$ source 168 (Reference to the quotient-model Truth Lemma with identity).

Complete Consistent Sets of sentence

Definition of a complete set of sentences

Complete set

A set $Γ$ source 20 of sentences is complete iff for any sentence $A$ source 21, either $A \in Γ$ source 21 or $\neg A \in Γ$ source 22.

source 19

Explanation

Complete consistent sets are important in the completeness proof since we can guarantee that every consistent set of sentences $Γ$ source 36 is contained in a complete consistent set $Γ^{*}$ source 37. A complete consistent set contains, for each sentence $A$ source 38, either $A$ source 38 or its negation $\neg A$ source 38, but not both. This is true in particular for atomic sentences, so from a complete consistent set in a language suitably expanded by constants, we can construct a structure where the interpretation of predicates is defined according to which atomic sentences are in $Γ^{*}$ source 47. This structure can then be shown to make all sentences in $Γ^{*}$ source 48 (and hence also all those in $Γ$ source 49) true. The proof of this latter fact requires that $\neg A \in Γ^{*}$ source 50 iff $A \notin Γ^{*}$ source 50, $(A \lor B) \in Γ^{*}$ source 50 iff $A \in Γ^{*}$ source 51 or $B \in Γ^{*}$ source 51, etc.

In what follows, we will often tacitly use the properties of reflexivity, monotonicity, and transitivity of $⊢$ source 55 (see

Reference to the Proof Theoretic Notions section for sequent calculus Reference to the Proof Theoretic Notions section for natural deduction Reference to the Proof Theoretic Notions section for axiomatic deduction Reference to the Proof Theoretic Notions section for tableaux).

Proposition characterizing complete consistent sets

Suppose $Γ$ source 62 is complete and consistent. Then:

If $Γ ⊢ A$ source 64, then $A \in Γ$ source 64.
$A \land B \in Γ$ source 67 iff both $A \in Γ$ source 68 and $B \in Γ$ source 68.
$A \lor B \in Γ$ source 70 iff either $A \in Γ$ source 71 or $B \in Γ$ source 71.
$A \to B \in Γ$ source 73 iff either $A \notin Γ$ source 74 or $B \in Γ$ source 74.

source 60

Proof

Let us suppose for all of the following that $Γ$ source 79 is complete and consistent.

If $Γ ⊢ A$ source 82, then $A \in Γ$ source 82.
Suppose that $Γ ⊢ A$ source 84. Suppose to the contrary that $A \notin Γ$ source 84. Since $Γ$ source 85 is complete, $\neg A \in Γ$ source 85. By
Reference to the explicit inconsistency proposition for sequent calculus Reference to the explicit inconsistency proposition for natural deduction Reference to the explicit inconsistency proposition for axiomatic deduction Reference to the explicit inconsistency proposition for tableaux, $Γ$ source 96 is inconsistent. This contradicts the assumption that $Γ$ source 97 is consistent. Hence, it cannot be the case that $A \notin Γ$ source 97, so $A \in Γ$ source 98.
Exercise.
First we show that if $A \lor B \in Γ$ source 135, then either $A \in Γ$ source 135 or $B \in Γ$ source 136. Suppose $A \lor B \in Γ$ source 136 but $A \notin Γ$ source 136 and $B \notin Γ$ source 137. Since $Γ$ source 137 is complete, $\neg A \in Γ$ source 138 and $\neg B \in Γ$ source 138. By
Reference to the proposition giving disjunction derivability facts for sequent calculus Reference to the proposition giving disjunction derivability facts for natural deduction Reference to the proposition giving disjunction derivability facts for axiomatic deduction Reference to the proposition giving disjunction derivability facts for tableaux, item (1), $Γ$ source 148 is inconsistent, a contradiction. Hence, either $A \in Γ$ source 148 or $B \in Γ$ source 149.
For the reverse direction, suppose that $A \in Γ$ source 151 or $B \in Γ$ source 151. By
Reference to the proposition giving disjunction derivability facts for sequent calculus Reference to the proposition giving disjunction derivability facts for natural deduction Reference to the proposition giving disjunction derivability facts for axiomatic deduction Reference to the proposition giving disjunction derivability facts for tableaux, item (2), $Γ ⊢ A \lor B$ source 162. By Reference to the derivability implies membership clause for complete consistent sets, $A \lor B \in Γ$ source 162, as required.
Exercise.

End of proof.

Exercise: complete the complete consistent set proof

Complete the proof of Reference to the proposition characterizing complete consistent sets.

source 212

Henkin Expansion

Proposition preserving consistency under language expansion

If $Γ$ source 34 is consistent in $L$ source 34 and $L^{'}$ source 34 is obtained from $L$ source 35 by adding a denumerable set of new constants $d_{0}$ source 35, $d_{1}$ source 36, and so on, then $Γ$ source 36 is consistent in $L^{'}$ source 36.

source 32

Definition of a saturated set

Saturated set

A set $Γ$ source 40 of formulas of a language $L$ source 40 is saturated iff for each formula $A (x) \in Frm (L)$ source 41 with one free variable $x$ source 42 there is a constant $c \in L$ source 42 such that $\exists x A (x) \to A (c) \in Γ$ source 45.

source 39

The following definition will be used in the proof of the next theorem.

Definition of the Henkin witness sentences

Let $L^{'}$ source 53 be as in Reference to the proposition preserving consistency under language expansion. Fix an enumeration $A_{0} (x_{0})$ source 54, $A_{1} (x_{1})$ source 54, and so on of all formulas $A_{i} (x_{i})$ source 54 of $L^{'}$ source 55 in which one variable ( $x_{i}$ source 55) occurs free. We define the sentences $D_{n}$ source 56 by induction on $n$ source 56.

Let $c_{0}$ source 58 be the first constant among the $d_{i}$ source 58 we added to $L$ source 59 which does not occur in $A_{0} (x_{0})$ source 59. Assuming that $D_{0}$ source 60, and so on, $D_{n - 1}$ source 60 have already been defined, let $c_{n}$ source 60 be the first among the new constants $d_{i}$ source 61 that occurs neither in $D_{0}$ source 62, and so on, $D_{n - 1}$ source 62 nor in $A_{n} (x_{n})$ source 62.

Now let $D_{n}$ source 64 be the formula $\exists x_{n} A_{n} (x_{n}) \to A_{n} (c_{n})$ source 65.

source 51

Henkin saturation extension lemma

Every consistent set $Γ$ source 72 can be extended to a saturated consistent set $Γ^{'}$ source 73.

source 70

Proof

Given a consistent set of sentences $Γ$ source 77 in a language $L$ source 77, expand the language by adding a denumerable set of new constants to form $L^{'}$ source 79. By Reference to the proposition preserving consistency under language expansion, $Γ$ source 79 is still consistent in the richer language. Further, let $D_{i}$ source 80 be as in Reference to the definition of the Henkin witness sentences. Let

Display defining the Henkin extension sequence

The two-row display starts with Gamma sub zero equal to Gamma and forms each successor by adjoining the current Henkin witness sentence.

$\begin{matrix} Γ_{0} & = Γ \\ Γ_{n + 1} & = Γ_{n} \cup {D_{n}} \end{matrix}$ source 82

source 82

i.e.,

Γ_{n + 1} = Γ \cup {D_{0}, \dots, D_{n}}

source 86, and let

Γ^{'} = ⋃_{n} Γ_{n}

source 87.

Γ^{'}

source 87 is clearly saturated.

If $Γ^{'}$ source 89 were inconsistent, then for some $n$ source 89, $Γ_{n}$ source 89 would be inconsistent (Exercise: explain why). So to show that $Γ^{'}$ source 90 is consistent it suffices to show, by induction on $n$ source 91, that each set $Γ_{n}$ source 92 is consistent.

The induction basis is simply the claim that $Γ_{0} = Γ$ source 94 is consistent, which is the hypothesis of the theorem. For the induction step, suppose that $Γ_{n}$ source 96 is consistent but $Γ_{n + 1} = Γ_{n} \cup {D_{n}}$ source 96 is inconsistent. Recall that $D_{n}$ source 97 is $\exists x_{n} A_{n} (x_{n}) \to A_{n} (c_{n})$ source 99, where $A_{n} (x_{n})$ source 101 is a formula of $L^{'}$ source 101 with only the variable $x_{n}$ source 102 free. By the way we've chosen the $c_{n}$ source 102 (see Reference to the definition of the Henkin witness sentences), $c_{n}$ source 103 does not occur in $A_{n} (x_{n})$ source 103 nor in $Γ_{n}$ source 104.

If $Γ_{n} \cup {D_{n}}$ source 106 is inconsistent, then $Γ_{n} ⊢ \neg D_{n}$ source 106, and hence both of the following hold:

Γ_{n} ⊢ \exists x_{n} A_{n} (x_{n}) Γ_{n} ⊢ \neg A_{n} (c_{n})

source 109

Since

c_{n}

source 119 does not occur in

Γ_{n}

source 120 or in

A_{n} (x_{n})

source 120, Reference to the Strong Generalization Theorem for axiomatic deduction Reference to the Strong Generalization Theorem for sequent calculus Reference to the Strong Generalization Theorem for natural deduction Reference to the Strong Generalization Theorem for tableaux applies. From

Γ_{n} ⊢ \neg A_{n} (c_{n})

source 123, we obtain

Γ_{n} ⊢ \forall x_{n} \neg A_{n} (x_{n})

source 127. Thus we have that both

Γ_{n} ⊢ \exists x_{n} A_{n} (x_{n})

source 131 and

Γ_{n} ⊢ \forall x_{n} \neg A_{n} (x_{n})

source 132, so

Γ_{n}

source 135 itself is inconsistent. (Note that

\forall x_{n} \neg A_{n} (x_{n}) ⊢ \neg \exists x_{n} A_{n} (x_{n})

source 139.) Contradiction:

Γ_{n}

source 145 was supposed to be consistent. Hence

Γ_{n} \cup {D_{n}}

source 146 is consistent.

End of proof.

Proposition characterizing quantifiers in a saturated set

Suppose $Γ$ source 161 is complete, consistent, and saturated.

$\exists x A (x) \in Γ$ source 163 iff $A (t) \in Γ$ source 163 for at least one closed term $t$ source 164. $\forall x A (x) \in Γ$ source 165 iff $A (t) \in Γ$ source 165 for all closed terms $t$ source 166.

source 160

Proof

First suppose that $\exists x A (x) \in Γ$ source 173. Because $Γ$ source 174 is saturated, $(\exists x A (x) \to A (c)) \in Γ$ source 175 for some constant $c$ source 176. By Reference to the proposition giving implication derivability facts for axiomatic deduction Reference to the proposition giving implication derivability facts for sequent calculus Reference to the proposition giving implication derivability facts for natural deduction Reference to the proposition giving implication derivability facts for tableaux, item (1), and Reference to the proposition characterizing complete consistent sets Reference to the derivability implies membership clause for complete consistent sets, $A (c) \in Γ$ source 178.

For the other direction, saturation is not necessary: Suppose $A (t) \in Γ$ source 182. Then $Γ ⊢ \exists x A (x)$ source 182 by Reference to the proposition giving quantifier derivability facts for axiomatic deduction Reference to the proposition giving quantifier derivability facts for sequent calculus Reference to the proposition giving quantifier derivability facts for natural deduction Reference to the proposition giving quantifier derivability facts for tableaux, item (1). By Reference to the proposition characterizing complete consistent sets Reference to the derivability implies membership clause for complete consistent sets, $\exists x A (x) \in Γ$ source 185.

Exercise.

End of proof.

Lindenbaum's Lemma

Lindenbaum extension lemma

Lindenbaum's Lemma

Every consistent set $Γ$ source 29 in a language $L$ source 29 can be extended to a complete and consistent set $Γ^{*}$ source 30.

source 27

Proof

Let $Γ$ source 34 be consistent. Let $A_{0}$ source 34, $A_{1}$ source 34, and so on be an enumeration of all the sentences of $L$ source 35. Define $Γ_{0} = Γ$ source 36, and

Γ_{n + 1} = \begin{matrix} Γ_{n} \cup {A_{n}} & if Γ n \cup {A n} is consistent; \\ Γ_{n} \cup {\neg A_{n}} & otherwise. \end{matrix}

source 37

Let

Γ^{*} = ⋃_{n \geq 0} Γ_{n}

source 45.

Each $Γ_{n}$ source 47 is consistent: $Γ_{0}$ source 47 is consistent by definition. If $Γ_{n + 1} = Γ_{n} \cup {A_{n}}$ source 48, this is because the latter is consistent. If it isn't, $Γ_{n + 1} = Γ_{n} \cup {\neg A_{n}}$ source 49. We have to verify that $Γ_{n} \cup {\neg A_{n}}$ source 50 is consistent. Suppose it's not. Then both $Γ_{n} \cup {A_{n}}$ source 51 and $Γ_{n} \cup {\neg A_{n}}$ source 52 are inconsistent. This means that $Γ_{n}$ source 53 would be inconsistent by

Reference to the proposition about two inconsistent opposite extensions for axiomatic deduction Reference to the proposition about two inconsistent opposite extensions for sequent calculus Reference to the proposition about two inconsistent opposite extensions for natural deduction Reference to the proposition about two inconsistent opposite extensions for tableaux, contrary to the induction hypothesis.

For every $n$ source 65 and every $i < n$ source 65, $Γ_{i} \subseteq Γ_{n}$ source 65. This follows by a simple induction on $n$ source 66. For $n = 0$ source 66, there are no $i < 0$ source 66, so the claim holds automatically. For the inductive step, suppose it is true for $n$ source 68. We show that if $i < n + 1$ source 68 then $Γ_{i} \subseteq Γ_{n + 1}$ source 68. We have $Γ_{n + 1} = Γ_{n} \cup {A_{n}}$ source 69 or $= Γ_{n} \cup {\neg A_{n}}$ source 69 by construction. So $Γ_{n} \subseteq Γ_{n + 1}$ source 70. If $i < n + 1$ source 71, then $Γ_{i} \subseteq Γ_{n}$ source 71 by inductive hypothesis (if $i < n$ source 72) or the trivial fact that $Γ_{n} \subseteq Γ_{n}$ source 72 (if $i = n$ source 73). We get that $Γ_{i} \subseteq Γ_{n + 1}$ source 73 by transitivity of $\subseteq$ source 74.

From this it follows that $Γ^{*}$ source 76 is consistent. Here's why: Let $Γ^{'} \subseteq Γ^{*}$ source 77 be finite. Each $B \in Γ^{'}$ source 77 is also in $Γ_{i}$ source 78 for some $i$ source 78. Let $n$ source 78 be the largest of these. Since $Γ_{i} \subseteq Γ_{n}$ source 79 if $i \leq n$ source 79, every $B \in Γ^{'}$ source 79 is also $\in Γ_{n}$ source 80, i.e., $Γ^{'} \subseteq Γ_{n}$ source 80, and $Γ_{n}$ source 81 is consistent. So, every finite subset $Γ^{'} \subseteq Γ^{*}$ source 81 is consistent. By Reference to the proof theoretic compactness proposition for axiomatic deduction Reference to the proof theoretic compactness proposition for sequent calculus Reference to the proof theoretic compactness proposition for natural deduction Reference to the proof theoretic compactness proposition for tableaux, $Γ^{*}$ source 90 is consistent.

Every sentence of $Frm (L)$ source 93 appears on the list used to define $Γ^{*}$ source 94. If $A_{n} \notin Γ^{*}$ source 94, then that is because $Γ_{n} \cup {A_{n}}$ source 95 was inconsistent. But then $\neg A_{n} \in Γ^{*}$ source 95, so $Γ^{*}$ source 96 is complete.

End of proof.

Construction of a Model

Explanation

Right now we are not concerned about $=$ source 16, i.e., we only want to show that a consistent set $Γ$ source 17 of sentences not containing $=$ source 18 is satisfiable. We first extend $Γ$ source 18 to a consistent, complete, and saturated set $Γ^{*}$ source 19. In this case, the definition of a model $M (Γ^{*})$ source 20 is simple: We take the set of closed terms of $L^{'}$ source 21 as the domain. We assign every constant to itself, and make sure that more generally, for every closed term $t$ source 23, ${⟦ t ⟧}^{M (Γ^{*})} = t$ source 23. The predicates are assigned extensions in such a way that an atomic sentence is true in $M (Γ^{*})$ source 25 iff it is in $Γ^{*}$ source 26. This will obviously make all the atomic sentences in $Γ^{*}$ source 27 true in $M (Γ^{*})$ source 27. The rest are true provided the $Γ^{*}$ source 28 we start with is consistent, complete, and saturated.

Definition of the term model

Term model

Let $Γ^{*}$ source 39 be a complete and consistent, saturated set of sentences in a language $L$ source 40. The term model $M (Γ^{*})$ source 41 of $Γ^{*}$ source 41 is the structure defined as follows:

The domain $| M (Γ^{*}) |$ source 44 is the set of all closed terms of $L$ source 45.
The interpretation of a constant $c$ source 46 is $c$ source 46 itself: $c^{M (Γ^{*})} = c$ source 47.
The function $f$ source 48 is assigned the function which, given as arguments the closed terms $t_{1}$ source 49, and so on, $t_{n}$ source 49, has as value the closed term $f (t_{1}, \dots, t_{n})$ source 50:
$f^{M (Γ^{*})} (t_{1}, \dots, t_{n}) = f (t_{1}, \dots, t_{n})$ source 51
If $R$ source 54 is an $n$ source 54-place predicate, then
$⟨ t_{1}, \dots, t_{n} ⟩ \in R^{M (Γ^{*})} iff R (t_{1}, \dots, t_{n}) \in Γ^{*} .$ source 55

source 37

Reader correction SAR-002: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. We will now check that we indeed have ${⟦ t ⟧}^{M (Γ^{*})} = t$ source 76.

Lemma evaluating closed terms in the term model

Let $M (Γ^{*})$ source 79 be the term model of Reference to the definition of the term model, then ${⟦ t ⟧}^{M (Γ^{*})} = t$ source 80.

source 78

Proof

The proof is by induction on $t$ source 83, where the base case, when $t$ source 83 is a constant, follows directly from the definition of the term model. For the induction step assume $t_{1}, \dots, t_{n}$ source 85 are closed terms such that ${⟦ t_{i} ⟧}^{M (Γ^{*})} = t_{i}$ source 86 and that $f$ source 86 is an $n$ source 86-ary function. Then

Display for the term-value induction step

The three-row display evaluates a compound term by applying the interpreted function to the values of its arguments, replaces those values by the terms themselves, and obtains the original compound term.

$\begin{matrix} {⟦ f (t_{1}, \dots, t_{n}) ⟧}^{M (Γ^{*})} & = f^{M (Γ^{*})} ({⟦ t_{1} ⟧}^{M (Γ^{*})}, \dots, {⟦ t_{n} ⟧}^{M (Γ^{*})}) \\ = f^{M (Γ^{*})} (t_{1}, \dots, t_{n}) \\ = f (t_{1}, \dots, t_{n}), \end{matrix}$ source 88

source 88

and so by induction this holds for every closed term

t

source 95.

End of proof.

{FOL}{

Explanation

A structure $M$ source 101Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. may make an existentially quantified sentence $\exists x A (x)$ source 102Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. true without there being an instance $A (t)$ source 103Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. that it makes true. A structure $M$ source 104Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. may make all instances $A (t)$ source 105Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. of a universally quantified sentence $\forall x A (x)$ source 106Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. true, without making $\forall x A (x)$ source 107Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. true. This is because in general not every element of $| M |$ source 108Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. is the value of a closed term ( $M$ source 109Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. may not be covered). This is the reason the satisfaction relation is defined via variable assignments. However, for our term model $M (Γ^{*})$ source 111Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. this wouldn't be necessary—because it is covered. This is the content of the next result.

Proposition characterizing quantifiers in the term model

Let $M (Γ^{*})$ source 118Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. be the term model of Reference to the definition of the term model.

$M (Γ^{*}) ⊨ \exists x A (x)$ source 120Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. iff $M (Γ^{*}) ⊨ A (t)$ source 121Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. for at least one closed term $t$ source 121Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged.. $M (Γ^{*}) ⊨ \forall x A (x)$ source 122Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. iff $M (Γ^{*}) ⊨ A (t)$ source 123Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. for all closed terms $t$ source 123Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged..

source 116

Proof

By Reference to the semantic proposition for quantified formulas, $M (Γ^{*}) ⊨ \exists x A (x)$ source 131Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. iff for at least one variable assignment $s$ source 132Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged., $M (Γ^{*}), s ⊨ A (x)$ source 132Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged.. As $| M (Γ^{*}) |$ source 133Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. consists of the closed terms of $L$ source 133Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged., this is the case iff there is at least one closed term $t$ source 134Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. such that $s (x) = t$ source 135Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. and $M (Γ^{*}), s ⊨ A (x)$ source 135Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged.. By Reference to the substitution and assignment extensionality proposition, $M (Γ^{*}), s ⊨ A (x)$ source 137Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. iff $M (Γ^{*}), s ⊨ A (t)$ source 137Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged., where $s (x) = t$ source 138Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged.. By Reference to the proposition equating sentence truth and assignment satisfaction, $M (Γ^{*}), s ⊨ A (t)$ source 139Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. iff $M (Γ^{*}) ⊨ A (t)$ source 139Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged., since $A (t)$ source 140Reader correction: Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. is a sentence.

Exercise.

End of proof.

}

Exercise: complete the term model quantifier proof

Complete the proof of Reference to the proposition characterizing quantifiers in the term model.

source 158

Truth Lemma for the term model without identity

Truth Lemma

Suppose $A$ source 164 does not contain $=$ source 164. Then $M (Γ^{*}) ⊨ A$ source 165 iff $A \in Γ^{*}$ source 165.

source 163

Proof

We prove both directions simultaneously, and by induction on $A$ source 169.

Case: $M (Γ^{*}) ⊭ ⊥$ source 172 by definition of satisfaction. On the other hand, $⊥ \notin Γ^{*}$ source 173 since $Γ^{*}$ source 174 is consistent.

Case: $M (Γ^{*}) ⊨ R (t_{1}, \dots, t_{n})$ source 183 iff $⟨ t_{1}, \dots, t_{n} ⟩ \in R^{M (Γ^{*})}$ source 183 (by the definition of satisfaction) iff $R (t_{1}, \dots, t_{n}) \in Γ^{*}$ source 185 (by the construction of $M (Γ^{*})$ source 186).

Case: $M (Γ^{*}) ⊨ A$ source 194 iff $M (Γ^{*}) ⊭ B$ source 195 (by definition of satisfaction). By induction hypothesis, $M (Γ^{*}) ⊭ B$ source 197 iff $B \notin Γ^{*}$ source 198. Since $Γ^{*}$ source 198 is consistent and complete, $B \notin Γ^{*}$ source 199 iff $\neg B \in Γ^{*}$ source 200.

Case: $M (Γ^{*}) ⊨ A$ source 219 iff $M (Γ^{*}) ⊨ B$ source 220 or $M (Γ^{*}) ⊨ C$ source 221 (by definition of satisfaction) iff $B \in Γ^{*}$ source 222 or $C \in Γ^{*}$ source 222 (by induction hypothesis). This is the case iff $(B \lor C) \in Γ^{*}$ source 223 (by Reference to the proposition characterizing complete consistent sets Reference to the disjunction clause for complete consistent sets).

Case: $M (Γ^{*}) ⊨ A$ source 252 iff $M (Γ^{*}) ⊨ B (t)$ source 253 for at least one term $t$ source 253 (Reference to the proposition characterizing quantifiers in the term model). By induction hypothesis, this is the case iff $B (t) \in Γ^{*}$ source 255 for at least one term $t$ source 255. By Reference to the proposition characterizing quantifiers in a saturated set, this in turn is the case iff $\exists x B (x) \in Γ^{*}$ source 257.

End of proof.

Exercise: complete the Truth Lemma proof

Complete the proof of Reference to the term-model Truth Lemma without identity.

source 265

Identity

Definition of the term-model congruence relation

Let $Γ^{*}$ source 27 be a consistent and complete set of sentences in $L$ source 28. We define the relation $\approx$ source 28 on the set of closed terms of $L$ source 29 by

t \approx t^{'} iff t = t^{'} \in Γ^{*}

source 30

source 26

Proposition establishing the congruence properties of approx

The relation $\approx$ source 37 has the following properties:

$\approx$ source 39 is reflexive.
$\approx$ source 40 is symmetric.
$\approx$ source 41 is transitive.
If $t \approx t^{'}$ source 42, $f$ source 42 is a function, and $t_{1}$ source 42, and so on, $t_{i - 1}$ source 43, $t_{i + 1}$ source 43, and so on, $t_{n}$ source 43 are closed terms, then
$f (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n}) \approx f (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n}) .$ source 44
If $t \approx t^{'}$ source 48, $R$ source 48 is a predicate, and $t_{1}$ source 48, and so on, $t_{i - 1}$ source 49, $t_{i + 1}$ source 49, and so on, $t_{n}$ source 49 are closed terms, then
Display of predicate congruence under approx
The two-line display says that a predicate atom with t in one argument position belongs to Gamma star exactly when the corresponding atom with the related term t prime belongs.
1. $\begin{matrix} R (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n}) \in Γ^{*} iff \\ R (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n}) \in Γ^{*} . \end{matrix}$ source 50
source 50

source 35

Proof

Since $Γ^{*}$ source 58 is consistent and complete, $t = t^{'} \in Γ^{*}$ source 58 iff $Γ^{*} ⊢ t = t^{'}$ source 59. Thus it is enough to show the following:

$Γ^{*} ⊢ t = t$ source 62 for all closed terms $t$ source 62.
If $Γ^{*} ⊢ t = t^{'}$ source 63 then $Γ^{*} ⊢ t^{'} = t$ source 63.
If $Γ^{*} ⊢ t = t^{'}$ source 64 and $Γ^{*} ⊢ t^{'} = {t^{'}}^{'}$ source 64, then $Γ^{*} ⊢ t = {t^{'}}^{'}$ source 65.
If $Γ^{*} ⊢ t = t^{'}$ source 66, then
$Γ^{*} ⊢ f (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n}) = f (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n})$ source 67Reader correction: The frozen source has two consecutive commas in the first function-term argument list. The reader removes the extra comma; the source formula and source MathML remain available for comparison.
for every $n$ source 71-place function $f$ source 71 and closed terms $t_{1}$ source 71, and so on, $t_{i - 1}$ source 72, $t_{i + 1}$ source 72, and so on, $t_{n}$ source 72.
If $Γ^{*} ⊢ t = t^{'}$ source 73 and $Γ^{*} ⊢ R (t_{1}, \dots, t_{i - 1}, t, t_{i + 1}, \dots, t_{n})$ source 74, then $Γ^{*} ⊢ R (t_{1}, \dots, t_{i - 1}, t^{'}, t_{i + 1}, \dots, t_{n})$ source 76 for every $n$ source 77-place predicate $R$ source 77 and closed terms $t_{1}$ source 77, and so on, $t_{i - 1}$ source 78, $t_{i + 1}$ source 78, and so on, $t_{n}$ source 78.

End of proof.

Exercise: complete the congruence proof

Complete the proof of Reference to the congruence proposition for the relation approx.

source 82

Definition of equivalence classes and the quotient term set

Suppose $Γ^{*}$ source 87 is a consistent and complete set in a language $L$ source 88, $t$ source 88 is a closed term, and $\approx$ source 88 as in the previous definition. Then:

{[t]}_{\approx} = {t^{'} : t^{'} \in Trm (L), t \approx t^{'}}

source 90

and

Trm (L) /_{\approx} = {{[t]}_{\approx} : t \in Trm (L)}

source 93.

source 86

Definition of the factored term model

Let $M = M (Γ^{*})$ source 98 be the term model for $Γ^{*}$ source 99 from Reference to the definition of the term model. Then $M /_{\approx}$ source 99 is the following structure:

$| M /_{\approx} | = Trm (L) /_{\approx}$ source 102.
$c^{M /_{\approx}} = {[c]}_{\approx}$ source 103
$f^{M /_{\approx}} ({[t_{1}]}_{\approx}, \dots, {[t_{n}]}_{\approx}) = {[f (t_{1}, \dots, t_{n})]}_{\approx}$ source 104
$⟨ {[t_{1}]}_{\approx}, \dots, {[t_{n}]}_{\approx} ⟩ \in R^{M /_{\approx}}$ source 106 iff $M ⊨ R (t_{1}, \dots, t_{n})$ source 108, i.e., iff $R (t_{1}, \dots, t_{n}) \in Γ^{*}$ source 108.

source 96

Explanation

Note that we have defined $f^{M /_{\approx}}$ source 114 and $R^{M /_{\approx}}$ source 115 for elements of $Trm (L) /_{\approx}$ source 116 by referring to them as ${[t]}_{\approx}$ source 117, i.e., via representatives $t \in {[t]}_{\approx}$ source 117. We have to make sure that these definitions do not depend on the choice of these representatives, i.e., that for some other choices $t^{'}$ source 120 which determine the same equivalence classes ( ${[t]}_{\approx} = {[t^{'}]}_{\approx}$ source 121), the definitions yield the same result. For instance, if $R$ source 122 is a one-place predicate, the last clause of the definition says that ${[t]}_{\approx} \in R^{M /_{\approx}}$ source 124 iff $M ⊨ R (t)$ source 125. If for some other term $t^{'}$ source 125 with $t \approx t^{'}$ source 125, $M ⊭ R (t)$ source 126, then the definition would require ${[t^{'}]}_{\approx} \notin R^{M /_{\approx}}$ source 127. If $t \approx t^{'}$ source 128, then ${[t]}_{\approx} = {[t^{'}]}_{\approx}$ source 128, but we can't have both ${[t]}_{\approx} \in R^{M /_{\approx}}$ source 129 and ${[t]}_{\approx} \notin R^{M /_{\approx}}$ source 130. However, Reference to the congruence proposition for the relation approx guarantees that this cannot happen.

Proposition that the quotient structure is well defined

$M /_{\approx}$ source 136 is well defined, i.e., if $t_{1}$ source 136, and so on, $t_{n}$ source 137, ${t_{1}}^{'}$ source 137, and so on, ${t_{n}}^{'}$ source 137 are closed terms, and $t_{i} \approx {t_{i}}^{'}$ source 138 then

${[f (t_{1}, \dots, t_{n})]}_{\approx} = {[f ({t_{1}}^{'}, \dots, {t_{n}}^{'})]}_{\approx}$ source 140, i.e.,
$f (t_{1}, \dots, t_{n}) \approx f ({t_{1}}^{'}, \dots, {t_{n}}^{'})$ source 142
and
$M ⊨ R (t_{1}, \dots, t_{n})$ source 146 iff $M ⊨ R ({t_{1}}^{'}, \dots, {t_{n}}^{'})$ source 147, i.e.,
$R (t_{1}, \dots, t_{n}) \in Γ^{*} iff R ({t_{1}}^{'}, \dots, {t_{n}}^{'}) \in Γ^{*} .$ source 148

source 135

Proof

Follows from Reference to the congruence proposition for the relation approx by induction on $n$ source 156.

End of proof.

As in the case of the term model, before proving the truth lemma we need the following lemma.

Lemma evaluating terms in the quotient model

Let $M = M (Γ^{*})$ source 163, then ${⟦ t ⟧}^{M /_{\approx}} = {[t]}_{\approx}$ source 164.

source 162

Proof

The proof is similar to that of Reference to the term-model value lemma.

End of proof.

Exercise: complete the quotient term-value proof

Complete the proof of Reference to the quotient-model term-value lemma.

source 171

Truth Lemma for the quotient model with identity

$M /_{\approx} ⊨ A$ source 177 iff $A \in Γ^{*}$ source 177 for all sentences $A$ source 178.

source 175

Proof

By induction on $A$ source 182, just as in the proof of Reference to the term-model Truth Lemma without identity. The only case that needs additional attention is when $A \equiv t = t^{'}$ source 183.

Display of the identity case of the quotient Truth Lemma

The display follows three equivalent conditions: the quotient model satisfies t equals t prime, their equivalence classes are equal, t is related to t prime by approx, and the equality sentence belongs to Gamma star.

$\begin{matrix} M /_{\approx} ⊨ t = t^{'} & iff {[t]}_{\approx} = {[t^{'}]}_{\approx} (by definition of M /_{\approx}) \\ iff t \approx t^{'} (by definition of {[t]}_{\approx}) \\ iff t = t^{'} \in Γ^{*} (by definition of \approx). \end{matrix}$ source 185

source 185

End of proof.

The Completeness Theorem

First formulation of the Completeness Theorem

Completeness Theorem

Let $Γ$ source 21 be a set of sentences. If $Γ$ source 21 is consistent, it is satisfiable.

source 19

Proof

Suppose $Γ$ source 26 is consistent. By Reference to the Henkin saturation extension lemma, there is a saturated consistent set $Γ^{'} \supseteq Γ$ source 28. By Reference to Lindenbaum's extension lemma, there is a $Γ^{*} \supseteq Γ^{'}$ source 29 which is consistent and complete.

Since $Γ^{'} \subseteq Γ^{*}$ source 32, for each formula $A (x)$ source 33, $Γ^{*}$ source 33 contains a sentence of the form $\exists x A (x) \to A (c)$ source 35 and so $Γ^{*}$ source 37 is saturated. If $Γ$ source 37 does not contain $=$ source 38, then by Reference to the term-model Truth Lemma without identity, $M (Γ^{*}) ⊨ A$ source 40 iff $A \in Γ^{*}$ source 40. From this it follows in particular that for all $A \in Γ$ source 41, $M (Γ^{*}) ⊨ A$ source 42, so $Γ$ source 43 is satisfiable. If $Γ$ source 44 does contain $=$ source 44, then by Reference to the quotient-model Truth Lemma with identity, for all sentences $A$ source 45, $M /_{\approx} ⊨ A$ source 46 iff $A \in Γ^{*}$ source 46. In particular, $M /_{\approx} ⊨ A$ source 47 for all $A \in Γ$ source 47, so $Γ$ source 48 is satisfiable.

End of proof.

Semantic-to-syntactic formulation of completeness

Completeness Theorem, Second Version

For all $Γ$ source 53 and sentences $A$ source 53: if $Γ ⊨ A$ source 53 then $Γ ⊢ A$ source 54.

source 51

Proof

Note that the $Γ$ source 58's in Reference to the semantic-to-syntactic completeness corollary and Reference to the Completeness Theorem are universally quantified. To make sure we do not confuse ourselves, let us restate Reference to the Completeness Theorem using a different variable: for any set of sentences $Δ$ source 61, if $Δ$ source 62 is consistent, it is satisfiable. By contraposition, if $Δ$ source 63 is not satisfiable, then $Δ$ source 63 is inconsistent. We will use this to prove the corollary.

Suppose that $Γ ⊨ A$ source 66. Then $Γ \cup {\neg A}$ source 66 is unsatisfiable by Reference to the proposition relating entailment to unsatisfiability. Taking $Γ \cup {\neg A}$ source 67 as our $Δ$ source 68, the previous version of Reference to the Completeness Theorem gives us that $Γ \cup {\neg A}$ source 69 is inconsistent. By

Reference to the proposition relating derivability to inconsistency for axiomatic deduction Reference to the proposition relating derivability to inconsistency for sequent calculus Reference to the proposition relating derivability to inconsistency for natural deduction Reference to the proposition relating derivability to inconsistency for tableaux, $Γ ⊢ A$ source 80.

End of proof.

Exercise: derive the first completeness formulation

Use Reference to the semantic-to-syntactic completeness corollary to prove Reference to the Completeness Theorem, thus showing that the two formulations of the completeness theorem are equivalent.

source 84

Exercise: audit the rules used by completeness

In order for a derivation system to be complete, its rules must be strong enough to prove every unsatisfiable set inconsistent. Which of the rules of derivation were necessary to prove completeness? Are any of these rules not used anywhere in the proof? In order to answer these questions, make a list or diagram that shows which of the rules of derivation were used in which results that lead up to the proof of Reference to the Completeness Theorem. Be sure to note any tacit uses of rules in these proofs.

source 100

The Compactness Theorem

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 of finite satisfiability

A set $Γ$ source 30 of formulas is finitely satisfiable iff every finite $Γ_{0} \subseteq Γ$ source 30 is satisfiable.

source 29

Compactness Theorem in two forms

Compactness Theorem

Reader correction TR024-SOURCE-PROSE-001: The frozen source calls both Gamma and A sentences, although the theorem uses Gamma as a set of sentences. The reader supplies the missing type distinction; the source line is unchanged. The following hold for any sentences $Γ$ source 35Reader correction: The frozen source calls both Gamma and A sentences, although the theorem uses Gamma as a set of sentences. The reader supplies the missing type distinction; the source line is unchanged. and $A$ source 35Reader correction: The frozen source calls both Gamma and A sentences, although the theorem uses Gamma as a set of sentences. The reader supplies the missing type distinction; the source line is unchanged.:

$Γ ⊨ A$ source 37 iff there is a finite $Γ_{0} \subseteq Γ$ source 37 such that $Γ_{0} ⊨ A$ source 38.
$Γ$ source 39 is satisfiable iff it is finitely satisfiable.

source 33

Proof

We prove (2). If $Γ$ source 45 is satisfiable, then there is a structure $M$ source 46 such that $M ⊨ A$ source 47 for all $A \in Γ$ source 47. Of course, this $M$ source 48 also satisfies every finite subset of $Γ$ source 49, so $Γ$ source 49 is finitely satisfiable.

Now suppose that $Γ$ source 52 is finitely satisfiable. Then every finite subset $Γ_{0} \subseteq Γ$ source 53 is satisfiable. By soundness ( Reference to the soundness corollary that satisfiability implies consistency for axiomatic deduction Reference to the soundness corollary that satisfiability implies consistency for sequent calculus Reference to the soundness corollary that satisfiability implies consistency for natural deduction Reference to the soundness corollary that satisfiability implies consistency for tableaux), every finite subset is consistent. Then $Γ$ source 63 itself must be consistent by

Reference to the proof theoretic compactness proposition for axiomatic deduction Reference to the proof theoretic compactness proposition for sequent calculus Reference to the proof theoretic compactness proposition for natural deduction Reference to the proof theoretic compactness proposition for tableaux. By completeness (Reference to the Completeness Theorem), since $Γ$ source 74 is consistent, it is satisfiable.

End of proof.

Exercise: prove the finite entailment form of compactness

Prove (1) of Reference to the Compactness Theorem in two forms.

source 79

Compactness example producing a non-covered model

In every model $M$ source 92 of a theory $Γ$ source 92, each term $t$ source 92 of course picks out a element of $| M |$ source 93. Can we guarantee that it is also true that every element of $| M |$ source 94 is picked out by some term or other? In other words, are there theories $Γ$ source 95 all models of which are covered? The compactness theorem shows that this is not the case if $Γ$ source 97 has infinite models. Here's how to see this: Let $M$ source 98 be an infinite model of $Γ$ source 98, and let $c$ source 98 be a constant not in the language of $Γ$ source 99. Let $Δ$ source 99 be the set of all sentences $c \neq t$ source 100 for $t$ source 100 a term in the language $L$ source 101 of $Γ$ source 101, i.e.,

Δ = {c \neq t : t \in Trm (L)} .

source 102

A finite subset of

Γ \cup Δ

source 105 can be written as

Γ^{'} \cup Δ^{'}

source 105, with

Γ^{'} \subseteq Γ

source 106 and

Δ^{'} \subseteq Δ

source 106. Since

Δ^{'}

source 107 is finite, it can contain only finitely many terms. Let

a \in | M |

source 108 be a element of

| M |

source 108 not picked out by any of them, and let

M^{'}

source 109 be the structure that is just like

M

source 110, but also

c^{M^{'}} = a

source 110. Since

a \neq {⟦ t ⟧}^{M}

source 111 for all

t

source 111 occurring in

Δ^{'}

source 111,

M^{'} ⊨ Δ^{'}

source 112. Since

M ⊨ Γ

source 112,

Γ^{'} \subseteq Γ

source 112, and

c

source 113 does not occur in

Γ

source 113, also

M^{'} ⊨ Γ^{'}

source 114. Together,

M^{'} ⊨ Γ^{'} \cup Δ^{'}

source 114 for every finite subset

Γ^{'} \cup Δ^{'}

source 115 of

Γ \cup Δ

source 115. So every finite subset of

Γ \cup Δ

source 116 is satisfiable. By compactness,

Γ \cup Δ

source 117 itself is satisfiable. So there are models

M ⊨ Γ \cup Δ

source 118. Every such

M

source 118 is a model of

Γ

source 119, but is not covered, since

{⟦ c ⟧}^{M} \neq {⟦ t ⟧}^{M}

source 119 for all terms

t

source 120 of

L

source 120.

source 91

Compactness example producing an infinitesimal

Consider a language $L$ source 124 containing the predicate $<$ source 124, constants $0$ source 125, $1$ source 125, and functions $+$ source 125, $\times$ source 125, and $-$ source 126. Let $Γ$ source 126 be the set of all sentences in this language true in the structure $Q$ source 127 with domain $ℚ$ source 127 and the obvious interpretations. $Γ$ source 128 is the set of all sentences of $L$ source 129 true about the rational numbers. Of course, in $ℚ$ source 129 (and even in $ℝ$ source 130), there are no numbers $r$ source 130 which are greater than $0$ source 130 but less than $1 / k$ source 131 for all $k \in Z^{+}$ source 131. Such a number, if it existed, would be an infinitesimal: non-zero, but infinitely small. The compactness theorem can be used to show that there are models of $Γ$ source 134 in which infinitesimals exist. We do not have a function for division in our language (division by zero is undefined, and functions have to be interpreted by total functions). However, we can still express that $r < 1 / k$ source 137, since this is the case iff $r \cdot k < 1$ source 138. Now let $c$ source 138 be a new constant and let $Δ$ source 138 be

{0 < c} \cup {c \times \bar{k} < 1 : k \in Z^{+}}

source 139

(where

\bar{k} = (1 + (1 + \dots + (1 + 1) \dots))

source 143 with

k

source 144

1

source 144's). For any finite subset

Δ_{0}

Δ

K

source 145Reader correction: The frozen sentence combines 'for all' with 'have' and has no grammatical subject for the bound. The reader states that every displayed inequality in the finite subset has index k below K; the source is unchanged. Reader correction TR024-SOURCE-PROSE-002: The frozen sentence combines 'for all' with 'have' and has no grammatical subject for the bound. The reader states that every displayed inequality in the finite subset has index k below K; the source is unchanged. such that for all the sentences

c \times \bar{k} < 1

source 146Reader correction: The frozen sentence combines 'for all' with 'have' and has no grammatical subject for the bound. The reader states that every displayed inequality in the finite subset has index k below K; the source is unchanged. in

Δ_{0}

k < K

Q

source 147 to

Q^{'}

source 147 with

c^{Q^{'}} = 1 / K

source 147 we have that

Q^{'} ⊨ Γ_{0} \cup Δ_{0}

source 148 for any finite

Γ_{0} \subseteq Γ

source 149, and so

Γ \cup Δ

source 149 is finitely satisfiable (Exercise: prove this in detail). By compactness,

Γ \cup Δ

source 150 is satisfiable. Any model

S

source 151 of

Γ \cup Δ

source 151 contains an infinitesimal, namely

c^{S}

source 152.

source 123

Exercise: obtain a nonstandard arithmetic element

In the standard model of arithmetic $N$ source 158, there is no element $k \in | N |$ source 159 which satisfies every formula $\bar{n} < x$ source 159 (where $\bar{n}$ source 160 is $0^{' \dots'}$ source 160 with $n$ source 160 $'$ source 161'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 $N$ source 163 are also true in a structure $N^{'}$ source 164 that contains a element which does satisfy every formula $\bar{n} < x$ source 165.

source 157

Compactness example separating infinitude from finitude

We know that first-order logic with identity can express that the size of the domain must have some minimal size: The sentence $A_{\geq n}$ source 173 (which says “there are at least $n$ source 173 distinct objects”) is true only in structures where $| M |$ source 174 has at least $n$ source 175 objects. So if we take

Δ = {A_{\geq n} : n \geq 1}

source 176

then any model of

Δ

source 179 must be infinite. Thus, we can guarantee that a theory only has infinite models by adding

Δ

source 180 to it: the models of

Γ \cup Δ

source 181 are all and only the infinite models of

Γ

source 182.

So first-order logic can express infinitude. The compactness theorem shows that it cannot express finitude, however. For suppose some set of sentences $Λ$ source 186 were satisfied in all and only finite structures. Then $Δ \cup Λ$ source 187 is finitely satisfiable. Why? Suppose $Δ^{'} \cup Λ^{'} \subseteq Δ \cup Λ$ source 188 is finite with $Δ^{'} \subseteq Δ$ source 189 and $Λ^{'} \subseteq Λ$ source 189. Let $n$ source 190 be the largest number such that $A_{\geq n} \in Δ^{'}$ source 190. $Λ$ source 191, being satisfied in all finite structures, has a model $M$ source 192 with finitely many but $\geq n$ source 192 elements. But then $M ⊨ Δ^{'} \cup Λ^{'}$ source 193. By compactness, $Δ \cup Λ$ source 193 has an infinite model, contradicting the assumption that $Λ$ source 195 is satisfied only in finite structures.

source 170

A Direct Proof of the Compactness Theorem

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 $Γ$ source 18 of sentences, expanded it to a consistent, saturated, and complete set $Γ^{*}$ source 20 of sentences, and then showed that in the term model $M (Γ^{*})$ source 22 constructed from $Γ^{*}$ source 23, all sentences of $Γ$ source 23 are true, so $Γ$ source 24 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 characterizing complete finitely satisfiable sets

Suppose $Γ$ source 33 is complete and finitely satisfiable. Then:

$(A \land B) \in Γ$ source 35 iff both $A \in Γ$ source 36 and $B \in Γ$ source 36.

$(A \lor B) \in Γ$ source 38 iff either $A \in Γ$ source 39 or $B \in Γ$ source 39.

$(A \to B) \in Γ$ source 41 iff either $A \notin Γ$ source 42 or $B \in Γ$ source 42.

source 31

Exercise: prove the finite-satisfiability clauses directly

Prove Reference to the proposition characterizing complete finitely satisfiable sets. Avoid the use of $⊢$ source 48.

source 47

Finite-satisfiability Henkin extension lemma

Every finitely satisfiable set $Γ$ source 60 can be extended to a saturated finitely satisfiable set $Γ^{'}$ source 61.

source 59

Exercise: prove the finite-satisfiability Henkin lemma

Prove Reference to the finite-satisfiability Henkin extension lemma. (Hint: The crucial step is to show that if $Γ_{n}$ source 68 is finitely satisfiable, so is $Γ_{n} \cup {D_{n}}$ source 68, without any appeal to derivations or consistency.)

source 66

Proposition characterizing quantified instances under finite satisfiability

Suppose $Γ$ source 75 is complete, finitely satisfiable, and saturated.

$\exists x A (x) \in Γ$ source 77 iff $A (t) \in Γ$ source 77 for at least one closed term $t$ source 78. $\forall x A (x) \in Γ$ source 79 iff $A (t) \in Γ$ source 79 for all closed terms $t$ source 80.

source 74

Exercise: prove the finite-satisfiability quantifier clauses

Prove Reference to the finite-satisfiability proposition for quantified instances.

source 86

Finite-satisfiability Lindenbaum extension lemma

Every finitely satisfiable set $Γ$ source 92 can be extended to a complete and finitely satisfiable set $Γ^{*}$ source 94.

source 91

Exercise: prove the finite-satisfiability Lindenbaum lemma

Prove Reference to the finite-satisfiability Lindenbaum extension lemma. (Hint: the crucial step is to show that if $Γ_{n}$ source 100 is finitely satisfiable, then either $Γ_{n} \cup {A_{n}}$ source 101 or $Γ_{n} \cup {\neg A_{n}}$ source 101 is finitely satisfiable.)

source 98

Direct Compactness Theorem

Compactness

$Γ$ source 116 is satisfiable if and only if it is finitely satisfiable.

source 115

Proof

If $Γ$ source 121 is satisfiable, then there is a structure $M$ source 122 such that $M ⊨ A$ source 123 for all $A \in Γ$ source 123. Of course, this $M$ source 124 also satisfies every finite subset of $Γ$ source 125, so $Γ$ source 125 is finitely satisfiable.

Now suppose that $Γ$ source 128 is finitely satisfiable. By Reference to the finite-satisfiability Henkin extension lemma, there is a finitely satisfiable, saturated set $Γ^{'} \supseteq Γ$ source 130. By Reference to the finite-satisfiability Lindenbaum extension lemma, $Γ^{'}$ source 131 can be extended to a complete and finitely satisfiable set $Γ^{*}$ source 132, and $Γ^{*}$ source 132 is still saturated. Construct the term model $M (Γ^{*})$ source 134 as in Reference to the definition of the term model. Note that Reference to the proposition characterizing quantifiers in the term model did not rely on the fact that $Γ^{*}$ source 137 is consistent (or complete or saturated, for that matter), but just on the fact that $M (Γ^{*})$ source 138 is covered. The proof of the Truth Lemma (Reference to the term-model Truth Lemma without identity) goes through if Reader correction TR024-SOURCE-SELECTION-001: The frozen conditional assigns this sentence's period to its unused non-first-order branch. The reader restores the terminal period after the FOL replacement list; the source is unchanged. we replace references to Reference to the proposition characterizing complete consistent sets and Reference to the proposition characterizing quantifiers in a saturated set by references to Reference to the proposition characterizing complete finitely satisfiable sets and Reference to the finite-satisfiability proposition for quantified instances

End of proof.

Exercise: write the direct-proof Truth Lemma

Write out the complete proof of the Truth Lemma (Reference to the term-model Truth Lemma without identity) in the version required for the proof of Reference to the direct Compactness Theorem.

source 146

The Löwenheim–Skolem Theorem

The Löwenheim–Skolem Theorem says that if a theory has an infinite model, then it also has a model that is at most denumerable. An immediate consequence of this fact is that first-order logic cannot express that the size of a structure is nonenumerable: any sentence or set of sentences satisfied in all nonenumerable structures is also satisfied in some enumerable structure.

Downward Lowenheim Skolem Theorem

If $Γ$ source 21 is consistent then it has a enumerable model, i.e., it is satisfiable in a structure whose domain is either finite or denumerable.

source 20

Proof

If $Γ$ source 27 is consistent, the structure $M$ source 27 delivered by the proof of the completeness theorem has a domain $| M |$ source 28 that is no larger than the set of the terms of the language $L$ source 29. So $M$ source 30 is at most denumerable.

End of proof.

Downward Lowenheim Skolem Theorem without identity

If $Γ$ source 34 is a consistent set of sentences in the language of first-order logic without identity, then it has a denumerable model, i.e., it is satisfiable in a structure whose domain is infinite and enumerable.

source 33

Proof

If $Γ$ source 41 is consistent and contains no sentences in which identity appears, then the structure $M$ source 42 delivered by the proof of the completeness theorem has a domain $| M |$ source 43 identical to the set of terms of the language $L^{'}$ source 44. So $M$ source 44 is denumerable, since $Trm (L^{'})$ source 45 is.

End of proof.

Example: Skolem's Paradox

Skolem's Paradox

Zermelo–Fraenkel set theory $ZFC$ source 49 is a very powerful framework in which practically all mathematical statements can be expressed, including facts about the sizes of sets. So for instance, $ZFC$ source 51 can prove that the set $ℝ$ source 52 of real numbers is nonenumerable, it can prove Cantor's Theorem that the power set of any set is larger than the set itself, etc. If $ZFC$ source 54 is consistent, its models are all infinite, and moreover, they all contain elements about which the theory says that they are nonenumerable, such as the element that makes true the theorem of $ZFC$ source 57 that the power set of the natural numbers exists. By the Löwenheim–Skolem Theorem, $ZFC$ source 59 also has enumerable models—models that contain “nonenumerable” sets but which themselves are enumerable.

source 48

Reading preferences

How to use Read

Introduction

Outline of the Proof

Complete Consistent Sets of sentence

Definition of a complete set of sentences

Proposition characterizing complete consistent sets

Proof

Exercise: complete the complete consistent set proof

Henkin Expansion

Proposition preserving consistency under language expansion

Definition of a saturated set

Definition of the Henkin witness sentences

Henkin saturation extension lemma

Proof

Display defining the Henkin extension sequence

Proposition characterizing quantifiers in a saturated set

Proof

Lindenbaum's Lemma

Lindenbaum extension lemma

Proof

Construction of a Model

Definition of the term model

Lemma evaluating closed terms in the term model

Proof

Display for the term-value induction step

Proposition characterizing quantifiers in the term model

Proof

Exercise: complete the term model quantifier proof

Truth Lemma for the term model without identity

Proof

Exercise: complete the Truth Lemma proof

Identity

Definition of the term-model congruence relation

Proposition establishing the congruence properties of approx

Display of predicate congruence under approx

Proof

Exercise: complete the congruence proof

Definition of equivalence classes and the quotient term set

Definition of the factored term model

Proposition that the quotient structure is well defined

Proof

Lemma evaluating terms in the quotient model

Proof

Exercise: complete the quotient term-value proof

Truth Lemma for the quotient model with identity

Proof

Display of the identity case of the quotient Truth Lemma

The Completeness Theorem

First formulation of the Completeness Theorem

Proof

Semantic-to-syntactic formulation of completeness

Proof

Exercise: derive the first completeness formulation

Exercise: audit the rules used by completeness

The Compactness Theorem

Definition of finite satisfiability

Compactness Theorem in two forms

Proof

Exercise: prove the finite entailment form of compactness

Compactness example producing a non-covered model

Compactness example producing an infinitesimal

Exercise: obtain a nonstandard arithmetic element

Compactness example separating infinitude from finitude

A Direct Proof of the Compactness Theorem

Proposition characterizing complete finitely satisfiable sets

Exercise: prove the finite-satisfiability clauses directly

Finite-satisfiability Henkin extension lemma

Exercise: prove the finite-satisfiability Henkin lemma

Proposition characterizing quantified instances under finite satisfiability

Exercise: prove the finite-satisfiability quantifier clauses

Finite-satisfiability Lindenbaum extension lemma

Exercise: prove the finite-satisfiability Lindenbaum lemma

Direct Compactness Theorem

Proof

Exercise: write the direct-proof Truth Lemma

The Löwenheim–Skolem Theorem

Downward Lowenheim Skolem Theorem

Proof

Downward Lowenheim Skolem Theorem without identity