Valid Moves ⊢
Chapter 10 · pp. 474–544

Predicate Logic: Derivations

SD plus four quantifier rules gives PD. The interesting part is the restrictions on ∀I and ∃E, which make sure the instantiating constant really is arbitrary.

Typing derivations in PL
Derive: Ss
| (∀y)(Py ⊃ Sy)    Assumption
| Ps               Assumption
| Ps ⊃ Ss          1 ∀E
| Ss               2, 3 ⊃E

ASCII: (Ax) (∀x), (Ex) (∃x), rules UE UI EE EI. Here = is identity; use <-> for ≡.

Section 10.1

The derivation system PD

pp. 474–491 · exercises 10.1E

PD keeps every rule of SD and adds an elimination and introduction rule for each quantifier. Each involves a quantified sentence and a substitution instance of it; the constant used is the instantiating constant.

  • ∀E: from (∀x)P, enter any instance P(a/x). Let the goal tell you which constant to pick.
  • ∃I: from an instance P(a/x), enter (∃x)P. Since P(a/x) replaces every x, from Laa you can reach (∃x)Lxa, (∃x)Lax or (∃x)Lxx.
  • ∀I: from P(a/x), enter (∀x)P, provided (i) a occurs in no open assumption and (ii) a doesn't occur in (∀x)P.
  • ∃E: from (∃x)P and a subderivation assuming P(a/x) and ending in Q, enter Q, provided (i) a occurs in no open assumption, (ii) a doesn't occur in (∃x)P, and (iii) a doesn't occur in Q.

The restrictions all express one idea: when you reason about a, nothing you've assumed may single a out. Then what holds of a holds of anything.

What each restriction blocks

∀I (i): from Fb as an assumption, infer (∀x)FxOne thing being F doesn't make everything F.
∀I (ii): from (∀x)Lxh get Lhh, then (∀x)LxxEveryone loving h doesn't mean everyone loves themselves.
∃E (iii): from (∃z)Fz, assume Fb and conclude FbSomething being F doesn't make b F.
∃E (i): the witness gets a constant already in an open assumptionThat would identify the witness with something we've assumed facts about.
Section 10.2

Syntactic properties in PD, and strategy

pp. 492–520 · exercises 10.2E

Derivability, validity, theorems, equivalence and inconsistency in PD are defined exactly as in SD. A derivation establishes them; Chapter 11 proves PD is sound and complete.

Strategies for quantifiers

  • Goal (∀x)P: derive an instance P(a/x) with a fresh constant, then ∀I. Choose a constant that appears in no open assumption and not in the goal.
  • Goal (∃x)P: derive an instance, then ∃I.
  • Accessible (∃x)P: start ∃E early. Assume an instance with a brand-new constant and aim for the goal itself inside the subderivation.
  • Accessible (∀x)P: use ∀E with whatever constants the goal and other lines need.
  • Negated quantifiers usually call for ~I or ~E, or in PD+, QN.

A worked shape: ∃ to ∃

1 | (∀x)(Fx ⊃ Gx)   Assumption
2 | (∃x)Fx          Assumption
3 | | Fa            A / ∃E
4 | | Fa ⊃ Ga       1 ∀E
5 | | Ga            3, 4 ⊃E
6 | | (∃x)Gx        5 ∃I
7 | (∃x)Gx          2, 3–6 ∃E

a is new at line 3 and gone by line 7, so all three ∃E restrictions hold.

Section 10.3

The derivation system PD+

pp. 521–525 · exercises 10.3E

PD+ adds SD+'s rules (MT, HS, DS and the replacement rules) and one new replacement rule, Quantifier Negation. Replacement rules apply to subformulas too, even open ones inside a quantifier, so it matters to identify subformulas correctly: (∀x)[Lx ⊃ (∀y)(Bxy ⊃ Jxy)] is not of the form P ⊃ (Q ⊃ R) inside.

PD is the elegant system; PD+ is the practical one. They prove the same things.

Quantifier Negation (QN)

~ (∀x)P ◁▷ (∃x)~ P
~ (∃x)P ◁▷ (∀x)~ P
Section 10.4

The derivation system PDE

pp. 526–544 · exercises 10.4E

PDE adds identity rules and lets ∀E and ∃I use any closed term, including complex terms like f(a) or g(a,b).

  • =I: enter (∀x)x = x on any line, citing nothing. It isn't an assumption; it's true on every interpretation. Then ∀E gives a = a.
  • =E: from t1 = t2 and a sentence P, enter P with one or more occurrences of t1 replaced by t2, or the other way round.

These rules handle definite descriptions: from "the Roman general who defeated Pompey conquered Gaul" and "Caesar is a Roman general who defeated Pompey", PDE derives "Caesar conquered Gaul".

Symmetry of identity

1 | | a = b          A / ⊃I
2 | | (∀x)x = x      =I
3 | | a = a          2 ∀E
4 | | b = a          1, 3 =E
5 | a = b ⊃ b = a    1–4 ⊃I

Line 4 replaces only the first a in line 3. Two ∀I steps then give (∀x)(∀y)(x = y ⊃ y = x).

Tool

Derivation checker for PD, PD+ and PDE

The same click-to-build checker as Chapter 5, now with the quantifier rules and all their restrictions, Quantifier Negation and the identity rules. Type the sentence, click the rule, click the lines it cites. Pick an exercise or start your own.

Or type the whole derivation as text

One line per derivation line. Each | is a scope line. Justifications look like Assumption, A / ∃E, 1 ∀E, 2, 3–6 ∃E, =I. ASCII rule names UE, UI, EE, EI also work.

Practice

Practice sets for Chapter 10

For our session

Discussion questions

  1. For each restriction on ∀I and ∃E, build an invalid "derivation" that the restriction blocks.
  2. Why can ∀E and ∃I instantiate with any constant at all, while ∀I and ∃E can't?
  3. Derive (∀x)Fx ⊃ (∃x)Fx. Which assumption of the semantics (Chapter 8) does this theorem depend on?
  4. =I enters a sentence citing nothing. How is that different from an assumption?
  5. Try to derive (∃x)(∀y)Lxy from (∀y)(∃x)Lxy. Where exactly does it break?
Your notes

Questions for our session

Saved in this browser only.

Supplementary reading

Nothing assigned from other texts for this chapter yet.