• Docència
    • Àlgebra Lineal i Geometria
    • Recull de qüestions
    • Recursos
    • Direcció de treballs
    • Innovació Docent
  • Recerca
    • Publicacions
    • Conferències
  • Codi
    • An Introduction to Lean 4
    • Taller de Lean 4
    • Galeria TikZ
    • Hipotrocoide
    • Evolució espacial dels virus
  • Enllaços
    • Grup d’Investigació
    • Grup d’Innovació Docent
    • Seminari Predoc
    • Congrés Investmat
  1. Quantifiers
  • Source Code
  • An Introduction to Lean 4
  • Basic Syntax
  • Propositions
  • Quantifiers
  • Equalities
  • Functions
  • Choice
  • Subtypes
  • Relations
  • Quotients
  • Natural numbers
  • Orders
  • Empty and Unit types
  • Product and Sum types
  • Lists and Monoids

Sections

  • Predicates
    • Examples of predicates
    • Operations on predicates
  • Universal Quantifier
  • Existential Quantifier
  • Exercises

Quantifiers

Autor

Enric Cosme

Modificat

02/04/2025

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.

Predicate.lean
variable (A : Type)
variable (P Q : A → Prop)

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
-- False predicate
def PFalse {A : Type} : A → Prop := fun _ => False
-- True predicate
def PTrue {A : Type} : A → Prop := fun _ => True

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
-- Conjunction of two predicates
def PAnd {A : Type} (P Q : A → Prop) : A → Prop := by
  intro a
  exact P a ∧ Q a

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:

And.lean
notation : 65 lhs:65 " ∧ " rhs:66 => PAnd lhs rhs

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:

And.lean
#check 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.

ForAll.lean
#check ∀ (a : A), P a
#check ∀ a, P a
#check ∀ {a : A}, P a

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.

ForAll.lean
theorem T1 : ∀ (a : A), P a := by
  intro a
  sorry

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.

ForAll.lean
variable (a : X)
variable (h : ∀ (a : A), P a)
#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 : ∀ (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.

ForAll.lean
theorem T2 (a : A) (h : ∀ (a : A), P a) : 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 ∃ (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.

Exists.lean
#check ∃ (a : A), P a
#check ∃ a, P a
#check Exists P

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 p

This 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:

Exists.lean
theorem T3 (a : A) (h : P a) : ∃ (a : A), P a := by
  exact Exists.intro a 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 : ∃ (a : A), P a) (h2 : ∀ (a : A), P a → Q) : Q := by
  cases h1
  rename_i a h3
  specialize h2 a
  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 : ∃ (a : A), P a) (h2 : ∀ (a : A), P a → 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 (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

2025 Enric Cosme Llópez

Dr. Moliner, 50 | 46100, Burjassot, València

Dissenyat amb & Quarto