Valid Moves ⊢
Chapter 9 · pp. 402–473

Predicate Logic: Truth-Trees

Chapter 4's trees, extended to quantifiers. The new twist: a universal sentence can never be used up, so some trees go on forever, and there's no mechanical test that always finishes.

The four quantifier rules
~∃D~ (∃x)P ▷ (∀x)~ P
~∀D~ (∀x)P ▷ (∃x)~ P
∃D(∃x)P ✓ ▷ P(a/x), a foreign
∀D(∀x)P ▷ P(a/x), any a, never ✓
Section 9.1

Truth-tree rules for PL

pp. 402–409 · exercises 9.1E

All nine SL rules carry over. Four rules handle quantifiers.

  • ~∃D and ~∀D move a negation inside a quantifier, flipping it. Both are non-branching and check the sentence off.
  • ∃D: from (∃x)P enter P(a/x), where a is foreign to the branch (occurs nowhere on it). Check it off. Using an old constant would assume, without warrant, that the witness is a thing already discussed.
  • ∀D: from (∀x)P enter any instance P(a/x), on one or more open branches. Universals are never checked off: there are always more instances.

Completed open branches, revised

A finite open branch is completed when each sentence on it is a literal, a checked-off compound that isn't universal, or a universal (∀x)P with at least one instance on the branch and an instance P(a/x) for every constant a on the branch. The "at least one" clause matters: without it, {(∀x)(Fx & ~ Fx)} would have an open tree.

A completed open branch yields a model: one UD member per constant, and the atomic sentences on the branch fix the extensions.

Why the foreign-constant rule

{(∃x)Bx, (∃x)~ Bx} is consistent: something is B and something else isn't. If ∃D could reuse a constant, both could be instantiated with a, closing the tree with Ba and ~ Ba. The restriction stops that.

Strategy carries over from Chapter 4: non-branching first, closings next. Decompose existentials before universals, so the universals can use the new constants.

Sections 9.2–9.3

Trees for consistency and other properties

pp. 410–424 · exercises 9.2E–9.3E

Tests are built exactly as in 4.2. A closed tree for {~ P} shows P is quantificationally true; a closed tree for Γ ∪ {~ P} shows Γ ⊨ P; a closed tree for {~ (P ≡ Q)} shows equivalence.

The difference from SL: a finite set may have no finite tree. A consistent set like {(∀y)(∃z)Fyz} sets up a loop with ∃D: each universal instance yields an existential, which brings a new constant, which needs a new universal instance. The branch never closes and never completes.

What a tree can tell you

Closed treeInconsistent. Settled.
Completed open branchConsistent. Settled, with a model.
Still growingNothing yet. It may never finish.
Section 9.4

Fine-tuning: systematic trees

pp. 425–440 · exercises 9.4E
Existential Decomposition-2 (∃D2)From (∃x)P, branch: one branch for P(a/x) with each constant a already on the branch, plus one branch with a foreign constant. The rule is due to George Boolos.

∃D2 lets the witness be something already named, while still allowing a new thing. With it, every set that has a finite model has a tree with a completed open branch.

The System

  1. Stage 1. Decompose all truth-functional compounds and existential sentences (with ∃D2), including ones this produces.
  2. Stage 2. Instantiate every universal with every constant on each open branch through it (with a if there's none), including universals added along the way.
  3. Repeat. Stop when the tree closes or an open branch completes.

Systematic trees always find a closed tree when one exists and a completed open branch when there's a finite model. The cost: they can be much bigger than a clever hand-built tree.

∃D versus ∃D2

For {(∀y)(∃z)Fyz}, ∃D never ends. With ∃D2 the first instance is Faa on one branch, a one-member model where a bears F to itself, so the tree finishes in three lines. Compare the two in the builder below.

Sections 9.5–9.6

Truth-trees for PLE

pp. 441–473 · exercises 9.5E–9.6E

For identity and functors:

  • ∀D may instantiate with any closed term, so from (∀x)~ Bx and Bf(c) you can enter ~ Bf(c).
  • Identity Decomposition (=D): if t1 = t2 is on a branch with a sentence P containing t1, you may enter P with t2 in place of t1.
  • A branch also closes when it contains ~ t = t.
  • Completed open branches need closure under =D as well.

9.6 combines this with ∃D2 to give systematic trees for PLE.

About the builder

The builder below handles PL fully. It accepts identity sentences and closes branches containing ~ a = a, but it doesn't apply =D or instantiate with functor terms. Do PLE trees by hand for now.

Tool

PL truth-tree builder

Click a highlighted sentence to decompose it. For a universal, choose which constant to use. "Finish" works on one open branch at a time, the one with the fewest constants, and stops at 80 lines.

Existentials:
Practice

Practice sets for Chapter 9

For our session

Discussion questions

  1. Why are existentials checked off but universals never are?
  2. Build a tree for {(∀y)(∃z)Fyz} with ∃D and watch the loop. Then use ∃D2. What model does the open branch describe?
  3. Why does the definition of a completed open branch require at least one instance of each universal?
  4. Church's theorem says there's no decision procedure for PL. How does that show up in trees?
  5. Systematic trees are guaranteed to work but can be huge. When would you use one?
Your notes

Questions for our session

Saved in this browser only.

Supplementary reading

Nothing assigned from other texts for this chapter yet.