### Quantifiers #### [Universal Quantifiers](https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/docs/en/notes/chapter04/quantifiers.md#universal-quantifiers) - Name: universal quantifier - Symbol: `∀` (read as "for all") - Editor shortcut: `\forall` - Meaning: given a type `α` and a unary predicate `p : α → Prop`, the proposition `∀ (x : α), p x` stands for "For all `x` of type `α`, `p x` holds." - Definition in Lean: if `p` is an arbitrary expression, `∀ (x : α), p` is an alternative notation for `(x : α) → p`. - Rules of inference - Introduction rule: if `p x` holds for every term `x : α`, then `∀ (x : α), p x` holds. (_universal generalization_) - Elimination rule: given `a : α`, `p a` follows from `∀ (x : α), p x`. (_universal instantiation_) #### [Existential Quantifiers](https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/docs/en/notes/chapter04/quantifiers.md#existential-quantifiers) - Name: existential quantifier - Name in Lean: `Exists` - Symbol: `∃` (read as "exists") - Editor shortcut: `\ex`, `\exists` - Meaning: given a type `α` and a unary predicate `p : α → Prop`, the proposition `∃ (x : α), p x` stands for "There exists a term `x` of type `α` where `p x` holds." - Rules of inference - Introduction rule: given `a : α`, `∃ (x : α), p x` follows from `p a`. (_existential introduction_) - Elimination rule: `q` follows from `∃ (x : α), p x` and `∀ (a : α), p a → q`. (_existential elimination_) --- **Source:** [Predicate Logic](https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/docs/en/notes/chapter04/quantifiers.md) **Author:** [[Bulhwi Cha]] **Curator:** [[dducoff]] **Posted Date:** 2026-01-19