Semantic preliminaries for PL and PLE
The book first proves a stock of facts that seem obvious but are needed later. The section can be skimmed at first; just know what each result says.
- 11.1.1: a variable assignment treats P(a/x) exactly as the assignment that sends x to a's referent treats P. Substituting a name is like pointing the variable at the named thing.
- 11.1.3: for a sentence, either every variable assignment satisfies it or none does, so sentences are simply true or false on an interpretation.
- 11.1.4 and 11.1.5: (∀x)P entails each of its instances, and each instance entails (∃x)P. These justify ∀E and ∃I.
- 11.1.6–11.1.9: interpretations that agree on the symbols in a sentence agree on its truth-value, and a constant that occurs nowhere relevant can be reinterpreted freely. These justify the restrictions on ∀I and ∃E.
11.2 extends these to complex terms and identity in PLE.
Why "fresh" constants work
If a doesn't occur in Γ or in (∃x)P, we may reinterpret a as whatever witnesses (∃x)P without changing the truth-value of anything in Γ. That's the semantic fact behind ∃E's restrictions, and behind ∃D in trees.
The soundness of PD, PD+ and PDE
The proof copies 6.3: induction on line numbers, showing each line is entailed by the open assumptions it lies within. The truth-functional rules were handled in Chapter 6. The new work is the four quantifier rules, and especially the restrictions on ∀I and ∃E, which use 11.1.8–11.1.10 to reinterpret the instantiating constant.
Soundness for PD+ adds QN and the replacement rules applied to subformulas; PDE adds =I and =E.
The ∀I case, in words
Suppose P(a/x) follows from assumptions Γ that don't mention a. Take any interpretation making Γ true and any member u of the UD. Reinterpret a as u: Γ stays true (a isn't in it), so P(a/x) is true, so u satisfies P. Since u was arbitrary, (∀x)P is true.
The completeness of PD, PD+ and PDE
As in 6.4, everything rests on one lemma: a set consistent in PD is quantificationally consistent (11.4.2). The construction is Henkin's, with one new ingredient. Whenever an existential sentence is added, a witness instance with a new constant goes in too, making the set ∃-complete. To guarantee there are always unused constants, first double every subscript, so all the odd-subscripted constants are free.
The model is then built from the constants themselves: one member of the UD per constant, and a predicate is true of the things whose names make an atomic sentence in the set.
The proof of 11.4.2, step by step
- 11.4.3Doubling every constant's subscript keeps a consistent set consistent.
- 11.4.4An evenly subscripted consistent set extends to one that is maximally consistent and ∃-complete.
- 11.4.5–7Such a set is quantificationally consistent: its constants and atomic sentences give a model.
- 11.4.8So the original set is quantificationally consistent.
Exercises prove Löwenheim's theorem from this, and the Löwenheim–Skolem theorem: every consistent set of PL has a model whose UD is the positive integers. Both fail for PLE.
Soundness and completeness of the tree method
Every decomposition rule is consistency-preserving: if the sentences on a branch can all be true, at least one extension of that branch can be too. This is the Consistent Branch Lemma (11.5.2). A consistent set therefore always keeps an open branch, so a closed tree means inconsistency.
By contraposition: an open systematic tree has either a completed open branch or an infinite one (Infinite Branch Lemma, 11.6.2), and either way the branch describes a model. This is why the System's careful staging matters.
What still can't be done
Completeness doesn't give a decision procedure. If Γ is consistent but has only infinite models, the systematic tree never finishes, and at no point can you tell it never will. Church's theorem (8.2) says no method can always tell.
Compare SL: Chapter 6's results plus the finiteness of truth-tables give a full decision procedure.
Practice for Chapter 11
Discussion questions
- Which steps of Chapter 6's completeness proof carry over unchanged, and what had to be added for quantifiers?
- Why double the subscripts? What would go wrong without spare constants?
- Löwenheim–Skolem says a consistent set of PL has a model on the positive integers. Why does this fail once we add identity?
- Completeness says every valid argument has a derivation. Why doesn't that give us a way to decide validity?
- Soundness of trees rests on rules being consistency-preserving. Check this for ∃D. Why is the foreign-constant requirement needed?
Questions for our session
Saved in this browser only.