tag

#quantifiers

3 pages tagged

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.12 Universal Quantifiers

A universal statement asserts that a property holds for every element of a type. In Lean, a proof of a universally quantified statement is a function that takes an arbitrary element and returns a proof of the property for that element. The usual notation: ∀ x : α, P x is implemented as a dependent function type. Problem You want to prove or use a statement of the form: ∀...
lean proof-assistant type-theory logic proof-theory quantifiers May 3, 2026
Programming › Lean › Chapter 2. Propositions and Proofs ›

2.11 Existential Quantifiers

An existential statement says that some object exists with a given property. In Lean, a proof of Exists P contains two pieces of data: a witness and a proof that the witness satisfies the predicate. The usual mathematical notation: ∃ x, P x means: Exists (fun x => P x) Problem You want to prove or use a statement of the form: ∃ x : α, P x To prove...
lean proof-assistant type-theory logic proof-theory quantifiers May 3, 2026
Maths › 03. Logic and Foundations ›

2.2 Quantifiers

Quantifiers are the symbols that allow first order logic to express statements about many objects at once, and they are the main feature that separates first order logic from propositional logic. Universal and Existential Quantifiers There are two basic quantifiers: $$ \forall $$ and: $$ \exists $$ The universal quantifier $\forall$ is read as "for all", and it is used to state that a formula holds for every object in...
logic first order logic quantifiers scope variables May 2, 2026