Propositions as Types, Annotated

Passage-by-passage annotations for section 3.1 of Theorem Proving in Lean 4.

These annotations are best read side by side with the original section in the book. The Lean code examples there are interactive: hover over any expression to see its type, and click the "try it" button to open it in a live editor.

Progression

In most languages, writing code and proving it correct are separate activities. If you want to make claims about some code you've written, you reach for a separate system: a test framework, a type checker, a contract library. And if you want to prove those claims hold, you reach for yet another tool: a model checker, a formal verification system, a proof assistant that sits alongside your code but is not part of it. The text begins by pointing this out.

§1One strategy for proving assertions about objects defined in the language of dependent type theory is to layer an assertion language and a proof language on top of the definition language.

A quick note of what is ahead: the section builds a working system, using valid Lean code, with separate types for propositions (Prop), proofs (Proof p), and explicit axioms (axiom modus_ponens). It all compiles and type-checks, but it's actually a pedagogical detour: Lean's type system already does all of this natively. The section builds the verbose version first, so you can see what it's doing, and then collapses it all down to concise, idiomatic Lean.

§2But there is no reason to multiply languages in this way: dependent type theory is flexible and expressive, and there is no reason we cannot represent assertions and proofs in the same general framework.

This is the core value proposition of Lean. Instead of three separate languages, dependent type theory collapses all three into one. In Lean, a proposition is a type. A proof is a term1 of that type. The same mechanism that defines functions is the mechanism that states theorems and proves them.

§3For example, we could introduce a new type, Prop, to represent propositions, and introduce constructors to build new propositions from others.

The framework gives us a special type called Prop. Values that have type Prop are themselves propositions. And we get constructors (like And, Or, Not, Implies) that take propositions and produce new propositions.

The type signatures

#check And
  | And (a b : Prop) : Prop

"What is And?" It's a function2 that takes two propositions and returns a proposition. Given propositions a and b, And a b is itself a proposition: the claim that both a and b are true.

#check Or
  | Or (a b : Prop) : Prop

"What is Or?" Same shape. Two propositions in, one proposition out. Or a b is the claim that at least one of a or b is true.

#check Not
  | Not (a : Prop) : Prop

"What is Not?" One proposition in, one proposition out. Not a is the claim that a is false.

Unlike And, Or, and Not (which are built into Lean), Implies is defined3 in the section as a thin wrapper around the function arrow.

-- Hidden behind the eye icon in the section's interactive code blocks
def Implies (a b : Prop) : Prop := a → b

#check Implies
  | Implies (p q : Prop) : Prop

"What is Implies?" Same shape as the others: two propositions in, one proposition out. But look at the definition: Implies a b is literally just a → b, the ordinary function arrow. This will matter later, when the section collapses Implies back into →.

Propositions in, propositions out. None of them prove anything; they just build new claims from old ones.

Applying the constructors

variable (p q r : Prop)

The variable4 command declares p, q, and r as propositions so we can use them in the examples below.

#check And p q
  | p ∧ q : Prop

Apply And to two specific propositions. The result is p ∧ q, which has type Prop. Note that Lean displays it with the ∧ symbol instead of writing And p q.

#check Or (And p q) r
  | p ∧ q ∨ r : Prop

Constructors compose. Feed And p q into Or alongside r, and you get a new proposition: "p and q, or r." Still a Prop.

#check Implies (And p q) (And q p)
  | Implies (p ∧ q) (q ∧ p) : Prop

"If p and q, then q and p." This is the commutativity claim for And. It's a Prop: a statement, not a proof. Nobody has proved it here; we've just built the proposition.

§4We could then introduce, for each element p : Prop, another type Proof p, for the type of proofs of p.

Here we are still building the naive approach. For every proposition p, create a separate type called Proof p. The notation Proof p means Proof(p), the same syntax we saw applying And, Or, and Implies earlier. Proof is a function from Prop to Type: hand it a proposition, get back a type. Once the structure below is declared, Lean can build an element of Proof p from any existing proof of p using the constructor. So Proof p is not an empty shell; it's a wrapper around a proof of p.

In code, this is a structure declaration5:

structure Proof (p : Prop) : Type where
  proof : p

#check Proof
  | Proof (p : Prop) : Type

Note the result type is Type, not Prop. Propositions live in Prop; their proofs live in Type. Two separate worlds. Like Implies, this is a pedagogical scaffolding the section will soon simplify. We will keep those concepts distinct in the language for now.

§5An "axiom" would be a constant of such a type.

Axioms are one way to give Proof p an inhabitant. An axiom declares a constant of type Proof p for some proposition p. It doesn't construct evidence; it asserts that evidence exists. Unlike the structure constructor, which packages an already-existing proof of p, an axiom simply postulates such evidence.

axiom and_commut (p q : Prop) :
  Proof (Implies (And p q) (And q p))

The and_commut axiom asserts that commutativity of And holds, but provides no proof. It's a naked declaration: Proof (Implies (And p q) (And q p)) is the type, and and_commut is a constant of that type, conjured into existence by axiom.

#check and_commut p q
  | and_commut p q : Proof (Implies (p ∧ q) (q ∧ p))

§6In addition to axioms, however, we would also need rules to build new proofs from old ones. For example, in many proof systems for propositional logic, we have the rule of modus ponens: From a proof of Implies p q and a proof of p, we obtain a proof of q.

Axioms (§5) let you declare truths, but a proof system also needs rules: ways to derive new proofs from existing ones. The first rule the section introduces is modus ponens, the most basic rule of inference in logic: if you know that p implies q, and you know p is true, then you know q is true. "If it's raining, the ground is wet" + "it's raining" = "the ground is wet."

axiom modus_ponens (p q : Prop) :
  Proof (Implies p q) →
  Proof p →
  Proof q

Three things going in: two propositions (p, q), a proof that p implies q, and a proof of p. One thing coming out: a proof of q.6 The → arrows here connect proof types (Proof ... → Proof ... → Proof ...), not propositions. Compare with the → inside Implies p q, which connects propositions (p → q where p q : Prop). Same symbol, different levels of the type system. But like §5, this is an axiom: it declares that combining two proofs this way is possible, without showing how. No :=, no body, no implementation.

§7Systems of natural deduction for propositional logic also typically rely on the following rule: Suppose that, assuming p as a hypothesis, we have a proof of q. Then we can "cancel" the hypothesis and obtain a proof of Implies p q.

This is the converse move to modus ponens: the deduction theorem. If you can get from p to q, you've earned p → q. The section calls it implies_intro:

axiom implies_intro (p q : Prop) :
  (Proof p → Proof q) →
  Proof (Implies p q)

Let's break this down token by token:

Putting it together: given propositions p and q, given a function that converts proofs of p into proofs of q, produce a proof that p implies q.

Binders and arrows both contribute arguments to one curried chain. The fully explicit type of implies_intro is:

implies_intro : (p : Prop) → (q : Prop) →
  (Proof p → Proof q) →
  Proof (Implies p q)

Read as a programmer, each argument consumes one layer of the curried chain:

The only reason we write (p q : Prop) as a binder instead of two more arrows is so we can reference p and q by name later in the type. Otherwise it's syntactic sugar for the same curried chain.

The hypothesis implies_intro asks for is a function, Proof p → Proof q. Not a specific proof of p and a specific proof of q; a function. This matters: two separate proofs don't establish a connection between p and q. A function does. It says: give me any proof of p and I will produce a proof of q. The universality is the function itself.

But notice that Proof p → Proof q and Proof (Implies p q) are different things in the verbose system:

implies_intro bridges them: it takes the computational fact (I have a function that transforms proofs) and produces the logical fact (the implication holds). This bridge is exactly what §9 and §10 will eliminate. Once Proof and Implies are gone, a term of type p → q is a proof of p → q. The two worlds were the same world all along.

The name implies_intro follows a convention from natural deduction. Each logical connective7 has two kinds of rules: introduction rules create a connective; elimination rules use one. implies_intro introduces an implication (it produces a →). Modus ponens eliminates one (it takes a → apart). The section uses this pattern8 throughout.

Together, the two rules are mirror images:

These two rules map directly onto the two fundamental operations of programming. They're the two moves that will survive when the layers collapse.

§8This approach would provide us with a reasonable way of building assertions and proofs. Determining that an expression t is a correct proof of assertion p would then simply be a matter of checking that t has type Proof p.

This is a pause-and-take-stock sentence. Everything from §3 through §7 (Prop, Proof, Implies, axioms, modus_ponens, implies_intro) is enough to express any assertion and build any proof, provided you're willing to write everything out the verbose way. This sentence marks the end of construction; what follows in the section is simplification, not new power.

The second half of the sentence is the real payload. "Checking that t is a correct proof of p" sounds philosophical. "Checking that t has type Proof p" sounds mechanical. The section is saying they are the same thing. Proof checking is type checking. A compiler already knows how to do the second, so it already knows how to do the first.

Concretely: suppose we've declared two propositions and two hypotheses.

variable (p q : Prop)
variable (hpq : Proof (Implies p q))
variable (hp : Proof p)

Now we can build an expression t by applying modus_ponens and ask Lean what its type is.

#check modus_ponens p q hpq hp
  | modus_ponens p q hpq hp : Proof q

But what does modus_ponens p q hpq hp actually mean? Each space-separated term feeds another argument into a curried function. We can trace the application step by step:

#check modus_ponens
  | modus_ponens (p q : Prop) : Proof (Implies p q) → Proof p → Proof q

#check modus_ponens p
  | modus_ponens p (q : Prop) : Proof (Implies p q) → Proof p → Proof q

#check modus_ponens p q
  | modus_ponens p q : Proof (Implies p q) → Proof p → Proof q

#check modus_ponens p q hpq
  | modus_ponens p q hpq : Proof p → Proof q

#check modus_ponens p q hpq hp
  | modus_ponens p q hpq hp : Proof q

Each line feeds one more argument; each arrow in the type disappears. At step 3, with the implication proof consumed, we have a function that just needs a Proof p. At step 4, that final argument goes in, and we're left with Proof q: a proof of q.

That's the whole idea of this sentence. "Is modus_ponens p q hpq hp a valid proof of q?" becomes "does modus_ponens p q hpq hp have type Proof q?" Lean answers by checking types, the same way it would catch "hello" + 1. Proof validity falls out of ordinary type checking.

This is the first quiet statement of the Curry-Howard correspondence9. Propositions are types. Proofs are terms. "Is this proof valid?" is "does this term have this type?" Everything in the rest of §3.1 is the section chipping away at the wrapper (dropping Proof, collapsing Implies into →, reusing function application as modus ponens) so that the correspondence stops being a reduction and becomes a literal identification.

The complete system

Here is every declaratiin the section has introduced, assembled in one place:

def Implies (a b : Prop) : Prop := a → b

structure Proof (p : Prop) : Type where
  proof : p

axiom and_commut (p q : Prop) :
  Proof (Implies (And p q) (And q p))

axiom modus_ponens (p q : Prop) :
  Proof (Implies p q) →
  Proof p →
  Proof q

axiom implies_intro (p q : Prop) :
  (Proof p → Proof q) →
  Proof (Implies p q)

variable (p q : Prop)
variable (hpq : Proof (Implies p q))
variable (hp : Proof p)

#check modus_ponens p q hpq hp
  | modus_ponens p q hpq hp : Proof q

#check implies_intro p p (fun hp : Proof p => hp)
  | implies_intro p p (fun hp => hp) : Proof (Implies p p)

One definition, one structure, two axioms, three variables, and two proofs. The first applies modus_ponens to existing hypotheses. The second constructs a proof that p implies itself, using implies_intro with a function10 that takes a proof of p and hands it right back: the identity function. The entire verbose system exists so that we can express fun hp => hp.

Everything from §3 through §8 in nineteen lines. The section's next move is to show that most of this machinery is redundant.

§9Some simplifications are possible, however. To start with, we can avoid writing the term Proof repeatedly by conflating Proof p with p itself. In other words, whenever we have p : Prop, we can interpret p as a type, namely, the type of its proofs. We can then read t : p as the assertion that t is a proof of p.

This is the first of two simplifications. The verbose system from §3 through §8 kept propositions and their proofs in separate worlds: propositions lived in Prop, proofs lived in Type via the Proof wrapper. The simplification says: let p serve double duty. When p : Prop, the expression t : p simultaneously means "t is a term of type p" and "t is a proof of proposition p." No wrapper needed.

Concretely, every Proof wrapper in the system just disappears:

This works because the type system already distinguishes Prop from Type. Lean knows p is a proposition (because p : Prop), so there's no ambiguity in reading t : p as "proof of p" rather than "value of type p."

§10Moreover, once we make this identification, the rules for implication show that we can pass back and forth between Implies p q and p → q. In other words, implication between propositions p and q corresponds to having a function that takes any element of p to an element of q. As a result, the introduction of the connective Implies is entirely redundant: we can use the usual function space constructor p → q from dependent type theory as our notion of implication.

Second simplification. §9 dropped Proof; now Implies goes too. Remember the definition from §3: Implies a b := a → b. That := is doing all the work now. With the Proof wrapper already gone, every Implies p q in a type can be replaced by p → q, because that's literally what it was defined to be.

Watch both simplifications compound across the full system:

-- Verbose (§3–§8)
hp : Proof p
hpq : Proof (Implies p q)
modus_ponens p q hpq hp : Proof q

-- After §9: drop Proof
hp : p
hpq : Implies p q
modus_ponens p q hpq hp : q

-- After §10: drop Implies
hp : p
hpq : p → q
hpq hp : q

The last block is the punchline. hpq hp is function application: apply the function hpq : p → q to the argument hp : p and get back a value of type q. No modus_ponens axiom needed; no Implies constructor needed; no Proof wrapper needed. What took three declarations and two axioms in the verbose system is just f(x).

§11This is the approach followed in the Calculus of Constructions, and hence in Lean as well. The fact that the rules for implication in a proof system for natural deduction correspond exactly to the rules governing abstraction and application for functions is an instance of the Curry-Howard isomorphism, sometimes known as the propositions-as-types paradigm.

The section is now naming what we identified in §8 (sidenote 9). Two names for the same observation: the Curry-Howard isomorphism is the structural fact (implication is function type, modus ponens is application, implies_intro is lambda); the propositions-as-types paradigm is the design philosophy built on that fact. The "Calculus of Constructions" is the formal system Lean is built on; it takes propositions-as-types as a foundational principle rather than a simplification applied after the fact.

§12In fact, the type Prop is syntactic sugar for Sort 0, the very bottom of the type hierarchy described in the last chapter. Moreover, Type u is also just syntactic sugar for Sort (u+1). Prop has some special features, but like the other type universes, it is closed under the arrow constructor: if we have p q : Prop, then p → q : Prop.

A technical aside. Prop isn't something the section invented; it's built into Lean's type universe hierarchy as Sort 0. Type is Sort 1, Type 1 is Sort 2, and so on. The hierarchy was covered earlier in the book; for our purposes, the important point is that Prop was always a first-class part of the type system.

The practical consequence: Prop is closed under →. If p and q are propositions, then p → q is also a proposition.

#check (p → q)
  | p → q : Prop

This is why dropping Implies in §10 worked. The arrow doesn't escape from Prop into Type; it stays within the world of propositions. No special connective needed.

§13There are at least two ways of thinking about propositions as types. To some who take a constructive view of logic and mathematics, this is a faithful rendering of what it means to be a proposition: a proposition p represents a sort of data type, namely, a specification of the type of data that constitutes a proof. A proof of p is then simply an object t : p of the right type.

Under the constructive reading, "true" and "inhabited" are the same thing. A proposition p is true exactly when you can construct a t : p. There is no separate notion of truth that exists independently of proof.

This is a departure from how most people think about truth. In everyday reasoning, the Riemann hypothesis is true or false right now, regardless of whether anyone has proved it. A constructivist wouldn't say that: until someone constructs a proof, the question is genuinely open.

The passage calls a proposition a "specification" because it specifies what data you'd need to produce. The proof is the data that meets the spec.

§14Those not inclined to this ideology can view it, rather, as a simple coding trick. To each proposition p we associate a type that is empty if p is false and has a single element, say *, if p is true. In the latter case, let us say that (the type associated with) p is inhabited. It just so happens that the rules for function application and abstraction can conveniently help us keep track of which elements of Prop are inhabited. So constructing an element t : p tells us that p is indeed true. You can think of the inhabitant of p as being the "fact that p is true." A proof of p → q uses "the fact that p is true" to obtain "the fact that q is true."

The other reading. Here, a proposition is already true or false independently of anyone proving it. The type system is just bookkeeping: associate an empty type with false propositions, an inhabited type with true ones. Constructing t : p doesn't make p true; it records that p is true.

Why exactly one inhabitant? Because under this view, the proof carries no interesting content; it's a marker, not data. All you care about is whether p is true, not how it was proved. One element is enough to signal "true"; zero signals "false." This connects directly to §15, where Lean formalizes the idea: any two proofs of the same proposition are definitionally equal.

§15Indeed, if p : Prop is any proposition, Lean's kernel treats any two elements t1 t2 : p as being definitionally equal, much the same way as it treats (fun x => t) s and t[s/x] as definitionally equal. This is known as proof irrelevance, and is consistent with the interpretation in the last paragraph. It means that even though we can treat proofs t : p as ordinary objects in the language of dependent type theory, they carry no information beyond the fact that p is true.

This is the formal rule behind §14's "single element." If t1 : p and t2 : p, the kernel treats them as the same thing. Not equivalent, not isomorphic: definitionally equal, the way (fun x => x + 1) 3 and 4 are definitionally equal. The kernel cannot distinguish them.

The practical consequence: Lean erases proofs at compile time. If two proofs are indistinguishable, there is no reason to keep them around at runtime. A proof that a list is sorted certifies the fact but carries no information about how to sort it.

§16The two ways we have suggested thinking about the propositions-as-types paradigm differ in a fundamental way. From the constructive point of view, proofs are abstract mathematical objects that are denoted by suitable expressions in dependent type theory. In contrast, if we think in terms of the coding trick described above, then the expressions themselves do not denote anything interesting. Rather, it is the fact that we can write them down and check that they are well-typed that ensures that the proposition in question is true. In other words, the expressions themselves are the proofs.

This sharpens the §13/§14 contrast into a single question: does the expression denote a proof, or is it the proof?

For practical purposes (writing Lean, using the proof assistant) it doesn't matter which view you hold. The next passage makes exactly that point.

§17In the exposition below, we will slip back and forth between these two ways of talking, at times saying that an expression "constructs" or "produces" or "returns" a proof of a proposition, and at other times simply saying that it "is" such a proof. This is similar to the way that computer scientists occasionally blur the distinction between syntax and semantics by saying, at times, that a program "computes" a certain function, and at other times speaking as though the program "is" the function in question. In any case, all that really matters is the bottom line. To formally express a mathematical assertion in the language of dependent type theory, we need to exhibit a term p : Prop. To prove that assertion, we need to exhibit a term t : p. Lean's task, as a proof assistant, is to help us to construct such a term, t, and to verify that it is well-formed and has the correct type.

The philosophical distinction from §13 through §16 is real, but practically inert. Both views produce the same code, the same type checks, the same results. The section is giving you permission to stop worrying about which interpretation is "right."

The bottom line, restated: express a claim as p : Prop, prove it by constructing t : p, and let Lean verify that t has the right type. That's the entire workflow. Everything in section 3.1 was building toward this sentence.

If you've worked with a type checker, you've already been doing proof. The gap between "this program is well-typed" and "this theorem is proved" is not a gap at all; it's the same operation, applied to different inputs. Here are the important ideas, as a before-and-after comparison: