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.

For simplicity, we will assume that X is an arbitrary type and P is a predicate on X, i.e., P : X → Prop, which is a function mapping elements of X to logical propositions.

Predicate.lean

variable (X : Type)
variable (P : X → Prop)

Universal Quantifier

The ∀ command (typed as \forall) represents the universal quantifier. It is used to express statements of the form ∀ (x : X), P x, which reads as “for every x of type X, the proposition P x holds.” This enables us to make general statements about all elements of a given type. Specifically, if P is a predicate on X, then ∀ (x : X), P x is of type Prop. The proposition ∀ (x : X), P x is true if P x is true for every element x of type X. The following two forms serve to denote the universal quantifier in Lean.

ForAll.lean

#check ∀ (x : X), P x
#check ∀ x, P x

To prove a statement of the form ∀ (x : X), P x, we typically use the intro tactic (or just write a lambda function directly in term mode). This introduces an arbitrary element x of type X and requires us to prove P x for that arbitrary x.

ForAll.lean

theorem T1 : ∀ (x : X), P x := by
  intro x
  sorry

On the other hand, if we have a hypothesis h : ∀ (x : X), P x and we want to use it for a specific value a : X, we can apply h on a to get P a.

ForAll.lean

variable (a : X)
variable (h : ∀ (x : X), P x)
#check h 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 : ∀ (x : X), P x, we can use specialize to apply h to a specific value a : X, 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.

ForAll.lean

theorem T2 (a : X) (h : ∀ (x : X), P x) : P a := by
  specialize h a
  exact h

Existential Quantifier

The ∃ command (typed as \exists) represents the existential quantifier. It is used to express statements of the form ∃ (x : X), P x, which reads as “for some x of type X, the proposition P x holds.” This enables us to make particular statements about elements of a given type. Specifically, if P is a predicate on X, then ∃ (x : X), P x is of type Prop. The proposition ∃ (x : X), P x is true if P x is true for some element x of type X. The following three forms serve to denote the universal quantifier in Lean.

Exists.lean

#check ∃ (x : X), P x
#check ∃ x, P x
#check Exists P

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 p

This code defines the existential quantifier as an inductive type, Exists, with a universe parameter u. The parameter {α : Sort u} represents the type of the witness, allowing Exists to work with types from any universe level. 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 inductive definition of Exists has two parameters: α : Sort u, the type of the witness, and p : α → Prop, the predicate that the witness must satisfy. The single constructor, Exists.intro, constructs a proof of Exists p given a witness w : α and a proof that w satisfies p. Lean infers α and p from context, so to obtain an element of type Exists p, it suffices to provide w and a proof of p w. Here’s an example of how the constructor works:

Exists.lean

theorem T3 (x : X) (h : P x) : ∃ (x : X), P x := by
  exact Exists.intro x h

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

variable (Q : Prop)
theorem T4 (h1 : ∃ (x : X), P x) (h2 : ∀ (x : X), P x → Q) : Q := by
  cases h1
  rename_i x h3
  specialize h2 x
  exact h2 h3

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.

Exists.lean

theorem T5 (h1 : ∃ (x : X), P x) (h2 : ∀ (x : X), P x → Q) : Q := by
  apply Exists.elim h1
  exact h2

Exercises

The following propositions are common identities involving quantifiers.

Exercises.lean

namespace Exercises
open Classical
variable (x y z : X)
variable (Q : X → Prop)
variable (R : Prop)

theorem E1 : (∃ (x : X), R) → R := by sorry

theorem E2 (x : X) : R → (∃ (x : X), R) := by sorry

theorem E3 : (∃ (x : X), P x ∧ R) ↔ (∃ (x : X), P x) ∧ R := by sorry

theorem E4 : (∃ (x : X), P x ∨ Q x) ↔ (∃ (x : X), P x)  ∨ (∃ (x : X), Q x) 
:= by sorry

theorem E5 : (∀ (x : X), P x) ↔ ¬ (∃ (x : X), ¬ P x) := by sorry

theorem E6 : (∃ (x : X), P x) ↔ ¬ (∀ (x : X), ¬ P x) := by sorry

theorem E7 : (¬ ∃ (x : X), P x) ↔ (∀ (x : X), ¬ P x) := by sorry

theorem E8 : (¬ ∀ (x : X), P x) ↔ (∃ (x : X), ¬ P x) := by sorry

theorem E9 : (∀ (x : X), P x → R) ↔ (∃ (x : X), P x) → R := by sorry

theorem E10 (x : X) : (∃ (x : X), P x → R) ↔ (∀ (x : X), P x) → R 
:= by sorry

theorem E11 (x : X) : (∃ (x : X), R  →  P x) ↔ (R → ∃ (x : X), P x) 
:= by sorry

end Exercises