Formal · II
Predicate logic
calculus praedicatorum · ‘the logic of what is said of what’
Extends propositional logic with predicates, terms, and the two quantifiers ∀ and ∃. The standard apparatus of first-order logic — the natural home for arguments about objects and the properties or relations they bear.
Orientation
What propositional logic cannot see
In propositional logic, the canonical Socratic syllogism is not formalisable as a valid argument. The premises ‘All men are mortal’ and ‘Socrates is a man’ are distinct atomic propositions; nothing in propositional syntax connects them to ‘Socrates is mortal’. The shared structure — that the first premise is a general claim about men, and that Socrates is one of them — is invisible.
Predicate logic exposes that structure. The first premise becomes ∀x (M(x) → Mo(x)); the second M(s); the conclusion Mo(s). Now the inference is licensed by the rules below.
Vocabulary
What is added
Predicate logic keeps the propositional connectives and the propositional rules. It adds the apparatus below.
- Constantsa, b, c, …
- Names of particular individuals. ‘Socrates’ might be a constant.
- Variablesx, y, z, …
- Placeholders ranged over by quantifiers; never named individuals.
- PredicatesP, Q, R, … (with arity)
- Express properties (unary) or relations (binary, ternary, …). M(x) for ‘x is mortal’; L(x, y) for ‘x loves y’.
- Functionsf, g, … (optional)
- Map tuples of objects to objects. ‘father-of(x)’ is a unary function.
- Universal quantifier∀x P(x)
- ‘For every x, P(x)’. True when P holds of every object in the domain.
- Existential quantifier∃x P(x)
- ‘There exists an x such that P(x)’. True when P holds of at least one object.
- Identityx = y
- Usually treated as a logical primitive: x and y refer to the same object.
Rules
Quantifier rules
Four rules govern the introduction and elimination of the quantifiers. Two have side-conditions (the freshness or arbitrariness of the constant) that make a difference to the soundness of natural-deduction proofs.
Universal instantiation
From the universal claim, any individual instance follows. (a is any constant.)
∀x P(x)∴P(a)Universal generalisation
If P holds of an arbitrary individual a, P holds of every individual. a must not appear in any open assumption.
P(a)∴∀x P(x)Existential generalisation
From an instance, the existence claim follows.
P(a)∴∃x P(x)Existential instantiation
From an existential claim, name the witness with a fresh constant c. c must not already appear in the proof.
∃x P(x)∴P(c)
Equivalences
Quantifier equivalences
The predicate-level analogues of De Morgan's laws and of distribution. The asymmetry on distribution is worth remembering: ∀ distributes over ∧ and ∃ distributes over ∨, but the cross-cases do not yield equivalences.
Quantifier negation
Negation swaps the quantifier and lands inside. The predicate analogue of De Morgan's laws.
¬∀x P(x) ≡ ∃x ¬P(x)¬∃x P(x) ≡ ∀x ¬P(x)Quantifier interchange (∧ / ∨)
∀ distributes over ∧; ∃ distributes over ∨. The other two cases (∀/∨ and ∃/∧) only give one-way implications, not equivalences.
∀x (P(x) ∧ Q(x)) ≡ ∀x P(x) ∧ ∀x Q(x)∃x (P(x) ∨ Q(x)) ≡ ∃x P(x) ∨ ∃x Q(x)
Worked proof
Socrates, formally
From ∀x (M(x) → Mo(x)) and M(s), derive Mo(s).
- 1.∀x (M(x) → Mo(x))premise
- 2.M(s)premise
- 3.M(s) → Mo(s)universal instantiation, 1
- 4.Mo(s)modus ponens, 3, 2
Universal instantiation supplies the conditional for the particular case; modus ponens (a propositional rule, still available) carries the inference home. Every step is licensed by an explicit rule.
Lineage
Origins and what lies past it
Predicate logic was invented in essentially its modern form by Gottlob Frege in Begriffsschrift(1879). Frege's two-dimensional notation was eventually replaced by the linear notation of Peano and Russell, but the substance is his. The combination of propositional connectives, quantifiers, and predicates is what almost everyone now means by ‘logic’ without qualification.
First-order predicate logic quantifies over individuals. Higher-order logic quantifies over predicates and functions — over properties of properties, sets of sets — and is correspondingly more expressive. The price is that first-order logic is sound and complete (Gödel 1929), while higher-order logic is not: there is no recursive proof system that proves every semantically valid formula. For most working purposes first-order is enough.