Module 1 · Lesson 2

Propositions as Types

Lean represents logical propositions as types. Understanding this representation is key to understanding how proofs work.

The Universe of Propositions

Lean has different "universes" for different kinds of types:

lean

1-- Data types live in Type
2#check Nat        -- Nat : Type
3#check String     -- String : Type
4#check List Nat   -- List Nat : Type
5
6-- Propositions live in Prop
7#check True       -- True : Prop
8#check False      -- False : Prop
9#check 2 + 2 = 4  -- 2 + 2 = 4 : Prop

Prop is special: it's the universe of things that are either true or false. Every proposition is a type, but a type specifically designed to express a logical claim.

Equality

The most common proposition is equality:

lean

1-- Equality is a proposition
2#check (5 = 5)        -- 5 = 5 : Prop
3#check (1 + 1 = 2)    -- 1 + 1 = 2 : Prop
4#check (1 + 1 = 3)    -- 1 + 1 = 3 : Prop (still a valid Prop, just false)
5
6-- Equality for any type
7#check ("hello" = "hello")  -- "hello" = "hello" : Prop
8#check ([1,2] = [1,2])      -- [1, 2] = [1, 2] : Prop

Note that 1 + 1 = 3 is a valid proposition—it's just false. You can state it, but you can't prove it.

True and False

lean

1-- True: a proposition that's trivially provable
2#check True       -- True : Prop
3example : True := trivial
4
5-- False: a proposition with no proof
6#check False      -- False : Prop
7-- example : False := ???  -- Impossible! No term has type False

True is a type with exactly one term (trivial).False is a type with no terms—that's what makes it false.

Key Takeaway

A proposition is true if you can construct a term of that type. It's false if no such term exists.

Implication: Functions

The logical "implies" (→) is represented as a function type:

lean

1-- "If A then B" is the type A → B
2-- A proof is a function from proofs of A to proofs of B
3
4example : True → True := fun _ => trivial
5
6-- "If 1 = 1, then 2 = 2"
7example : (1 = 1) → (2 = 2) := fun _ => rfl
8
9-- Read: given a proof of 1 = 1, return a proof of 2 = 2
10-- The proof of 1 = 1 isn't even used—2 = 2 is independently true

To prove an implication, you write a function. The function takes a proof of the hypothesis and produces a proof of the conclusion.

Conjunction: Products

"A and B" is represented as a pair:

lean

1-- And is defined like a structure
2-- structure And (a b : Prop) : Prop where
3--   left : a
4--   right : b
5
6-- To prove A ∧ B, provide proofs of both
7example : True ∧ True := ⟨trivial, trivial⟩
8
9example : (1 = 1) ∧ (2 = 2) := ⟨rfl, rfl⟩
10
11-- Access parts with .left and .right (or .1 and .2)
12example (h : True ∧ (1 = 1)) : True := h.left
13example (h : True ∧ (1 = 1)) : 1 = 1 := h.right

Disjunction: Sum Types

"A or B" is represented as a sum (tagged union):

lean

1-- Or has two constructors
2-- inductive Or (a b : Prop) : Prop where
3--   | inl : a → Or a b
4--   | inr : b → Or a b
5
6-- Prove left side
7example : True ∨ False := Or.inl trivial
8
9-- Prove right side
10example : False ∨ True := Or.inr trivial
11
12-- Either side works
13example : (1 = 1) ∨ (1 = 2) := Or.inl rfl

Negation

"Not A" is defined as "A implies False":

lean

1-- ¬A is defined as A → False
2#print Not  -- def Not (a : Prop) : Prop := a → False
3
4-- To prove ¬A, assume A and derive a contradiction
5example : ¬False := fun h => h  -- If False, then False (trivially)
6
7-- 1 ≠ 2 means (1 = 2) → False
8example : 1 ≠ 2 := by decide

ℹ

The symbol ≠ is notation for ¬(... = ...), which expands to (... = ...) → False.

Quantifiers

Universal: For All (∀)

lean

1-- ∀ x : T, P x is a dependent function type
2-- A proof is a function that works for any x
3
4example : ∀ n : Nat, n = n := fun n => rfl
5
6example : ∀ n : Nat, 0 + n = n := fun n => rfl
7
8-- Multiple quantifiers
9example : ∀ a b : Nat, a + b = b + a := Nat.add_comm

Existential: There Exists (∃)

lean

1-- ∃ x : T, P x is a dependent pair (witness + proof)
2-- Provide a specific x and prove P holds for it
3
4example : ∃ n : Nat, n > 5 := ⟨10, by decide⟩
5
6example : ∃ n : Nat, n + n = 10 := ⟨5, rfl⟩
7
8-- The witness and proof are bundled together
9example : ∃ s : String, s.length = 5 := ⟨"hello", rfl⟩

Deep Dive: Proof Irrelevance

In Prop, all proofs of the same proposition are considered equal. This is called "proof irrelevance."

lean

1-- Two different proofs of the same thing
2example (p q : 1 = 1) : p = q := rfl
3
4-- This is why Prop is special: only truth matters, not how you proved it

This makes sense logically: if you know something is true, you don't carehow it was proven. The fact that it's true is what matters.

Summary Table

Logic	Lean Type	To Prove
A implies B	A → B	Write a function
A and B	A ∧ B	Provide both proofs
A or B	A ∨ B	Provide one proof
Not A	¬A (= A → False)	Derive contradiction
For all x, P(x)	∀ x, P x	Function over all x
Exists x, P(x)	∃ x, P x	Witness + proof

What is a Proof?Next: The Proof State