Predicate Logic in Lean

In this post, we will look at predicate logic and see how to prove propositions that use universal and existential quantifiers in Lean 4. Our textbook continues to be "Starting from Scratch: An Introduction to Lean Language - Hands-on Development of Formal Mathematics Libraries".

What is Predicate Logic?

Predicate logic is a branch of logic that deals with predicates. A predicate is a proposition that contains variables, and its truth value is determined when specific values are substituted for those variables.

When constructing logical formulas using predicates, the following two symbols are introduced:

• **Universal Quantifier (∀)**: Indicates the assumption that "given any arbitrary value". A proposition stating that "for all x, P(x) holds" is written as ∀ x, P x.
• **Existential Quantifier (∃)**: Indicates that there exists at least one value that satisfies the proposition. A proposition stating that "there exists an x such that P(x) holds" is written as ∃ x, P x.

Proving with the Universal Quantifier ∀

In the following example, we prove a proposition that uses a universal quantifier for a predicate P.

def P (n : Nat) : Prop := n = n

example : ∀ a : Nat, P a := by
  intro x
  dsimp [P]

The intro tactic is used to assume a universal quantifier. You can think of it as declaring, "Suppose an arbitrary a is given." After this step, the goal of the proof changes to ⊢ P x.

Next, we apply dsimp [P]. dsimp is a tactic called *Definitional Simplification*, which simplifies the goal by expanding specified definitions. Expanding the definition of P, which is n = n, changes the goal to the trivial equality x = x, and Lean automatically closes the proof.

Proving with the Existential Quantifier ∃

Next, here is an example of a proposition using an existential quantifier.

def even (n : Nat) : Prop := ∃ m : Nat, n = m + m

example : even 4 := by
  exists 2

even is a predicate indicating that a number is even. It represents the proposition that there exists at least one natural number m such that n = m + m for a given n.

To prove a proposition containing an existential quantifier, we use the exists tactic. The proof is completed by providing the specific value whose existence is being claimed. Here, writing exists 2 shows that 4 = 2 + 2 holds when m = 2.

When an Existential Quantifier is Included in the Hypotheses

If an existential quantifier is used in your hypotheses, you can use the obtain tactic to extract the value whose existence is assumed.

example (α : Type) (P Q : α → Prop) (h : ∃ x : α, P x ∧ Q x)
  : ∃ x : α, Q x := by
  obtain ⟨y, hy⟩ := h
  exists y
  exact hy.right

The hypothesis h contains the information that "there exists an x that satisfies P x ∧ Q x". By writing obtain ⟨y, hy⟩ := h, you can extract that value as y : α, and the proof of the proposition that y satisfies as hy.

Subsequently, exists y changes the goal to ⊢ Q y. This means moving to the stage of asserting that "y is indeed the value that satisfies Q x". Since hy holds the proof for P y ∧ Q y, the proof is completed by extracting the right side of the conjunction—namely, Q y—using hy.right.