2.1 Propositions as Types

Lean identifies propositions with types and proofs with terms. This identification is the foundation of all proof construction in Lean. It is precise and operational. You do not reason about propositions abstractly. You construct inhabitants of types.

Problem

You want a model where logical statements can be manipulated with the same rules used for programs, so that proofs can be constructed, checked, and composed mechanically.

Core Principle

A proposition is a type in the universe Prop. A proof of that proposition is a term of that type.

If P : Prop, then a proof of P is a term p : P.

This is not an analogy. It is the actual representation used by the kernel.

Basic Examples

A simple proposition:

variable (P : Prop)

A proof of P -> P:

theorem id_prop (P : Prop) : P -> P := by
  intro h
  exact h

Here the type is P -> P. The proof is a function that takes h : P and returns h. The implication is implemented as a function type.

The same proof in term form:

theorem id_prop_term (P : Prop) : P -> P :=
  fun h => h

The distinction between proof and program disappears. This is just a function.

Logical Connectives as Types

Each logical connective has a type-theoretic interpretation.

Implication:

P -> Q

This is the type of functions from P to Q.

Conjunction:

P ∧ Q

This is a structure containing both a proof of P and a proof of Q.

Disjunction:

P ∨ Q

This is a tagged union containing either a proof of P or a proof of Q.

Negation:

¬ P

This is defined as:

P -> False

A proof of ¬ P is a function that turns any proof of P into a contradiction.

Working with Goals

Lean always maintains a goal of the form:

⊢ P

This means you must construct a term of type P.

If the goal is:

⊢ P -> Q

you apply:

intro h

which transforms the goal into:

h : P
⊢ Q

You have assumed P and must now produce Q.

If the goal is:

⊢ P ∧ Q

you apply:

constructor

which splits the goal into:

⊢ P
⊢ Q

Each logical form corresponds to a construction rule.

Context and Assumptions

The local context stores available terms:

h₁ : P
h₂ : Q
⊢ R

Each hypothesis is a usable term. If the goal is exactly one of them, you can solve it directly:

exact h₁

This matches the type of the goal.

Universes and `Prop`

Lean separates propositions from general data types:

Prop for logical statements
Type for computational data

A key property of Prop is proof irrelevance. Any two proofs of the same proposition are considered interchangeable at the level of computation. This allows Lean to erase proofs during execution.

Example: Combining Propositions

theorem and_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  cases h with
  | intro hp hq =>
    constructor
    · exact hq
    · exact hp

This proof extracts both components and rebuilds them in reverse order.

Term-Level View

The same proof can be written explicitly:

theorem and_swap_term (P Q : Prop) : P ∧ Q -> Q ∧ P :=
  fun h =>
    match h with
    | And.intro hp hq => And.intro hq hp

This makes the data structure explicit. A conjunction is a pair, and the proof rearranges that pair.

Common Pattern

Every proof reduces to constructing a term:

If the goal is a function, build a function
If the goal is a pair, build a pair
If the goal is a sum, choose a side
If the goal is False, derive contradiction

This is the working rule of the chapter.

Pitfalls

Confusing propositions with booleans. Prop is not Bool. A proof of P is not a truth value.

Expecting implicit computation. Proof construction is explicit unless automation is invoked.

Ignoring types. Every failure in Lean is a type mismatch.

Takeaway

Propositions are types. Proofs are terms. Logical reasoning becomes type construction. Once this model is internalized, Lean proofs become predictable and compositional.