cs.thefarshad
hard

Quantifier Rules & Identity

Natural deduction for predicate logic — the four quantifier rules, their restrictions, and identity.

Natural deduction extends to predicate logic with four quantifier rules — an introduction and elimination for each of ∀\forall and ∃\exists. The proof player below runs two predicate derivations step by step (choose “Universal instantiation” and “Existential reasoning”).

Given∀x (Px → Qx)Pa
ProveQa
Strategy: A premise is universal: instantiate it to the name a (∀E), then →E.
Try the derivation yourself first, then reveal the step-by-step proof.

The four quantifier rules

  • ∀\forallE (universal instantiation). From ∀x Px\forall x\,Px infer PaPa for any name aa. If it holds of everything, it holds of each thing.
  • ∃\existsI (existential generalization). From PaPa infer ∃x Px\exists x\,Px. If some particular thing is PP, then something is PP.
  • ∀\forallI (universal generalization). From PaPa — where aa is arbitrary — infer ∀x Px\forall x\,Px. The catch (the rule’s restriction): aa must not appear in any premise or undischarged assumption, so nothing special was assumed about it.
  • ∃\existsE (existential instantiation). From ∃x Px\exists x\,Px, open a subderivation assuming PaPa for a fresh name aa (one used nowhere else); whatever you derive that does not mention aa can be exported. This is how you reason from “something is P” without knowing which thing.

The “Existential reasoning” example — ∀x(Px→Qx), ∃x Px⊢∃x Qx\forall x(Px\rightarrow Qx),\ \exists x\,Px \vdash \exists x\,Qx — combines ∃\existsE, ∀\forallE, and ∃\existsI in one proof.

Why the restrictions matter

The restrictions are not bureaucracy — drop them and you can “prove” false things. Without the freshness condition on ∃\existsE you could move from “someone is a spy” to a claim about a named person; without the arbitrariness condition on ∀\forallI you could generalize a property of one specific object to everything. The conditions keep ⊢\vdash matching ⊨\models.

Identity

Add the predicate == for “is the same object as”, with two rules:

  • ==I (reflexivity): a=aa = a may be asserted on any line.
  • ==E (substitution): from a=ba = b and a statement about aa, infer the same statement with bb put for aa (equals may replace equals).

Identity lets predicate logic express counting and uniqueness — “there is exactly one PP” is ∃x (Px∧∀y (Py→y=x))\exists x\,(Px \land \forall y\,(Py \rightarrow y = x)).

Takeaways

  • Four rules: ∀\forallE (any name), ∃\existsI (generalize), ∀\forallI (arbitrary name), ∃\existsE (fresh-name subderivation).
  • The arbitrariness (∀\forallI) and freshness (∃\existsE) restrictions keep the system sound.
  • Identity adds ==I (reflexivity) and ==E (substitution), enabling uniqueness/counting claims.

References

  • Paul Teller, A Modern Formal Logic Primer, Prentice Hall (1989) — free at tellerprimer.ucdavis.edu, whose predicate rules and restrictions this follows. Proofs and explanations here are original.