Quantifiers
This chapter introduces the core concepts of quantifiers in Lean, which are pivotal in expressing logical statements. Quantifiers allow us to make general statements about elements of a type. The universal quantifier (∀) asserts that a property holds for all elements of a type, while the existential quantifier (∃) states that there exists at least one element of the type for which the property holds. Through examples and exercises, this chapter will help us understand how to use these quantifiers effectively in Lean.
Predicates
For simplicity, we will assume that A is an arbitrary type and P is a predicate on P, i.e., P : A → Prop, which is a function mapping elements of A to logical propositions.
Examples of predicates
Given a type A, we can define various predicates on it. One trivial example is the predicate that always evaluates to False, meaning it never holds for any element of A. Similarly, we can define a predicate that always evaluates to True, meaning it holds for every element of A. These can be expressed as follows:
Predicates.lean
In the definitions above, the underscore _ is a placeholder for an arbitrary input of type A, indicating that the function ignores its argument and always returns a constant value—either False or True. This underscores the fact that PFalse and PTrue do not depend on any particular element of A, but rather define predicates that are uniformly false or true for all elements of A.
Operations on predicates
Given two predicates P, Q : A → Prop, we can define their conjunction, a new predicate that holds for an element a : A if and only if both P a and Q a are true. This is captured by the following definition:
And.lean
Here, the function PAnd takes two predicates P and Q and returns a new predicate PAnd P Q on A. This new predicate holds at a : A if and only if both P a and Q a hold.
In Lean, the notation keyword allows us to define custom symbolic representations for functions and expressions, improving readability and aligning with standard mathematical conventions. It introduces shorthand notation for existing definitions, making logical and algebraic expressions more intuitive.
For example, we can define a custom infix operator ∧ for the conjunction of two predicates:
Here, notation specifies that P ∧ Q should be interpreted as PAnd P Q. The numbers 65 and 66 indicate precedence levels, ensuring that expressions involving ∧ are parsed correctly relative to other operators. The lhs and rhs keywords designate the left-hand side and right-hand side of the notation, ensuring proper binding behavior.
By using notation, we can write logical expressions in a way that closely resembles traditional mathematical notation, making proofs and definitions more readable. To verify the notation, we can check the type of P ∧ Q:
Lean confirms that P ∧ Q is a predicate on A, reinforcing that this notation correctly represents the conjunction of two predicates.
Building on the previous example, we can similarly define other fundamental logical operations on predicates. These include the disjunction P ∨ Q; the implication P → Q; the biconditional P ↔︎ Q; and the negation ¬P. Each of these operations extends our ability to reason about predicates.
Universal Quantifier
The ∀ command (typed as \forall) represents the universal quantifier. It is used to express statements of the form ∀ (a : A), P a, which reads as “for every a of type A, the proposition P a holds.” This enables us to make general statements about all elements of a given type. Specifically, if P is a predicate on A, then ∀ (a : A), P a is of type Prop. The proposition ∀ (a : A), P a is true if P a is true for every element a of type A. The following three forms serve to denote the universal quantifier in Lean.
In the second form, the type of the variable is not explicitly stated, as Lean can infer it from context. In the third form, the quantifier binding is implicit, indicated by curly braces {}. This allows Lean to automatically infer the value of a whenever possible, reducing the need for explicit annotations.
To prove a statement of the form ∀ (a : A), P a, we typically use the intro tactic (or just write a lambda function directly in term mode). This introduces an arbitrary element a of type A and requires us to prove P a for that arbitrary a.
On the other hand, if we have a hypothesis h : ∀ (a : A), P a and we want to use it for a specific value a : A, we can apply h on a to get P a.
The specialize tactic is used to apply a hypothesis that is a universally quantified statement to specific arguments. This allows us to instantiate a general hypothesis with particular values, making it easier to work with in our proof. When we have a hypothesis of the form h : ∀ (a : A), P a, we can use specialize to apply h to a specific value a : A, resulting in a new hypothesis h : P a. This is particularly useful when we want to focus on a specific instance of a general statement.
Existential Quantifier
The ∃ command (typed as \exists) represents the existential quantifier. It is used to express statements of the form ∃ (a : A), P a, which reads as “for some a of type A, the proposition P a holds.” This enables us to make particular statements about elements of a given type. Specifically, if P is a predicate on A, then ∃ (a : A), P a is of type Prop. The proposition ∃ (a : A), P a is true if P a is true for some element a of type A. The following three forms serve to denote the existential quantifier in Lean.
Unlike the universal quantifier, the existential quantifier does not support implicit binding. Attempting to write ∃ {a : A}, P a results in an error because Lean requires the bound variable a to be explicitly declared.
If we #print Exists, Lean returns
inductive Exists.{u} : {α : Sort u} → (α → Prop) → Prop
number of parameters: 2
constructors:
Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists pThis code defines the existential quantifier as an inductive type, Exists. It has two parameters: α : Sort u, the type of the witness, and p : α → Prop, the predicate that the witness must satisfy. The function type (α → Prop) → Prop ensures that Exists takes a predicate p : α → Prop and returns a proposition asserting the existence of an element of α that satisfies p.
The single constructor, Exists.intro, constructs a proof of Exists p given a witness a : α and a proof that a satisfies p. Lean infers α and p from context, so to obtain an element of type Exists p, it suffices to provide a and a proof of p a. Here’s an example of how the constructor works:
Since Exists is an inductive type, we can use cases on a proof of this type to extract both the witness and the proof that it satisfies the predicate P.
Exists.lean
Another alternative is to use Exists.elim the eliminator for the Exists type, allowing us to use the witness and the proof of predicate on the witness.
Exercises
The following propositions are common identities involving quantifiers.
Exercises.lean
namespace Exercises
open Classical
variable (a b c : A)
variable (R : Prop)
theorem E1 : (∃ (a : A), R) → R := by sorry
theorem E2 (a : A) : R → (∃ (a : A), R) := by sorry
theorem E3 : (∃ (a : A), P a ∧ R) ↔ (∃ (a : A), P a) ∧ R := by sorry
theorem E4 : (∃ (a : A), (P ∨ Q) a) ↔ (∃ (a : A), P a) ∨ (∃ (a : A), Q a) := by sorry
theorem E5 : (∀ (a : A), P a) ↔ ¬(∃ (a : A), (¬P) a) := by sorry
theorem E6 : (∃ (a : A), P a) ↔ ¬ (∀ (a : A), (¬P) a) := by sorry
theorem E7 : (¬∃ (a : A), P a) ↔ (∀ (a : A), (¬P) a) := by sorry
theorem E8 : (¬∀ (a : A), P a) ↔ (∃ (a : A), (¬P) a) := by sorry
theorem E9 : (∀ (a : A), P a → R) ↔ (∃ (a : A), P a) → R := by sorry
theorem E10 (a : A) : (∃ (a : A), P a → R) → (∀ (a : A), P a) → R := by sorry
theorem E11 (a : A) : (∃ (a : A), R → P a) → (R → ∃ (a : A), P a) := by sorry