Lean theorem prover/Foundations/The three axioms

Plain-language version: What the axioms are

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Lean's type theory, with its dependent functions, universes, inductive types and quotients, is extended in the core library by three axioms: propositional extensionality (propext), the soundness of quotients (Quot.sound) and global choice (Classical.choice). An axiom is a constant with a type and no definition; it does not reduce, and the compiler cannot generate code for it. Lean records, for every definition and theorem, which axioms it depends on, and prints the list on request. This page states the three as Lean prints them, says what each makes possible, shows the dependency audit on examples, and sets out the further axioms that are not mathematics at all.

As Lean prints them

#print propext
#print Quot.sound
#print Classical.choice

axiom propext : ∀ {a b : Prop}, (a ↔ b) → a = b
axiom Quot.sound.{u} : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b
axiom Classical.choice.{u} : {α : Sort u} → Nonempty α → α

In Lean 4.34.1 propext is stated in the file Init/Core.lean, and the other two in Init/Prelude.lean. As rules, with $a,b:\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{p}$:

$\frac{\Gamma ⊢h:a\leftrightarrow b}{\Gamma ⊢\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{p}\mathrm{e}\mathrm{x}\mathrm{t}h:a=b}\frac{\Gamma ⊢p:rab}{\Gamma ⊢\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{s}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{d}p:\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{m}\mathrm{k}ra=\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{m}\mathrm{k}rb}\frac{\Gamma ⊢h:\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{e}\mathrm{m}\mathrm{p}\mathrm{t}\mathrm{y}\alpha }{\Gamma ⊢\mathrm{C}\mathrm{l}\mathrm{a}\mathrm{s}\mathrm{s}\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{l}\mathrm{.}\mathrm{c}\mathrm{h}\mathrm{o}\mathrm{i}\mathrm{c}\mathrm{e}h:\alpha }$

The first two conclude equations, which are propositions. The third concludes an element of an arbitrary type. That difference decides how each one interacts with computation.

What each makes possible

Propositional extensionality says that logically equivalent propositions are equal, so that one may be replaced by the other in any context. The reference manual notes that the ordinary connectives respect logical equivalence provably, without the axiom, but that it is needed for an unknown predicate P : Prop → Prop applied to equivalent arguments, and for equality between propositions itself. It is valid intuitionistically. Theorem Proving in Lean 4 adds that it agrees with set-theoretic readings in which every proposition is either empty or a one-element set.

Quotient soundness identifies the classes of related elements in a quotient type. It is also the only axiom behind function extensionality, which Lean proves as a theorem from quotients; the proof is on propositional equality. With propext it gives an extensional theory of sets represented as predicates: two predicates true of the same elements are equal.

Global choice turns a proof that a type is inhabited into an element of it. Nonempty α is a proposition, and a proof of it carries no information about which element exists. Classical.choice nevertheless returns one, and returns the same one for any proof, since all proofs of a proposition are equal. Theorem Proving in Lean 4 derives from it the principle of indefinite description, and, with the other two axioms, excluded middle, the decidability of every proposition and Hilbert's epsilon operator. That derivation is classical logic from choice.

The first two can block evaluation in Lean's kernel, because a cast along an equation proved by an axiom does not reduce, but they are compatible with compiled code, which erases proofs. Choice is not: it manufactures data from a proposition, and definitions that use it for data must be marked noncomputable.

The audit: #print axioms

#print axioms lists every axiom a constant depends on, directly or through the definitions and theorems it uses. Five small theorems show the range from none to all three:

theorem two_add_two : 2 + 2 = 4 := rfl

theorem and_swap (p q : Prop) : p ∧ q ↔ q ∧ p :=
  ⟨fun ⟨hp, hq⟩ => ⟨hq, hp⟩, fun ⟨hq, hp⟩ => ⟨hp, hq⟩⟩

theorem and_swap_eq (p q : Prop) : (p ∧ q) = (q ∧ p) :=
  propext (and_swap p q)

theorem add_zero_fun : (fun n : Nat => n + 0) = (fun n => n) :=
  funext fun _ => rfl

theorem em' (p : Prop) : p ∨ ¬p := Classical.em p

#print axioms two_add_two
#print axioms and_swap
#print axioms and_swap_eq
#print axioms add_zero_fun
#print axioms em'

'two_add_two' does not depend on any axioms
'and_swap' does not depend on any axioms
'and_swap_eq' depends on axioms: [propext]
'add_zero_fun' depends on axioms: [Quot.sound]
'em'' depends on axioms: [propext, Classical.choice, Quot.sound]

Here the computation checked by rfl and the logical equivalence need nothing, the equation between propositions needs propext, and the equation between functions needs Quot.sound, through funext. Excluded middle needs all three, because the proof of Classical.em in the core library uses choice, propext and funext.

sorry and sorryAx

The term sorry closes any goal. It elaborates to the axiom sorryAx, which inhabits every type, and so it is used for unfinished work and never belongs in a finished proof.

#print sorryAx

theorem unfinished : 1 = 2 := sorry

theorem uses_unfinished : 2 = 3 := congrArg (· + 1) unfinished

#print axioms uses_unfinished

axiom sorryAx.{u} : (α : Sort u) → Bool → α
'uses_unfinished' depends on axioms: [sorryAx]

Lean warns once, with declaration uses `sorry`, at unfinished, where sorry is written. The theorem uses_unfinished raises no warning of its own, yet it proves a falsehood, and only the axiom list shows why. The reference manual makes the same point about the editor's check marks: they appear even when a dependency uses sorry, and printing the axioms is what detects it.

Axioms that are not mathematics

Any user can write an axiom, and Lean accepts it. Lean cannot check that a new axiom is consistent with the others.

axiom everything_is_equal : ∀ (a b : Nat), a = b

theorem one_eq_two : 1 = 2 := everything_is_equal 1 2

#print axioms one_eq_two

The last line prints 'one_eq_two' depends on axioms: [everything_is_equal]. The theorem is checked and accepted; the audit is what exposes its premise.

An axiom can also be harmless on its own and inconsistent with the standard three. The reference manual's example is a "free theorem" of parametricity, which says that a function polymorphic in the element type of a list commutes with mapping over the list. With excluded middle every proposition is decidable, so a function can test whether its type argument is Nat and behave differently when it is. That function is not parametric, and together with the free theorem it proves False.

The core library itself states three further axioms, Lean.trustCompiler, Lean.ofReduceBool and Lean.ofReduceNat. The reference manual describes them as mathematically trivial: they mark proofs that depend on the correctness of the whole compiler rather than only on Lean's small kernel. The tactic native_decide, which settles a decidable statement by running compiled code, creates a dedicated axiom for each use, stating exactly the fact the compiled code asserted:

theorem big : 123456 * 654321 = 80779853376 := by native_decide

#print axioms big

Lean 4.34.1 prints 'big' depends on axioms: [big._native.native_decide.ax_1_1]. Such a theorem rests on the correctness of the whole compiler, not only on Lean's kernel and the three axioms: each use of the tactic widens what has to be trusted.

Why audit per theorem

The three standard axioms are, in the reference manual's words, "known to be consistent". Carneiro's model of Lean's type theory in set theory, published in 2019, covers all three axioms together; it is described, with its limits, in consistency and the metatheory. Every other axiom is a premise the reader has to accept separately. The manual's guide to validating a proof therefore asks that #print axioms report only propext, Classical.choice and Quot.sound: a sorryAx means an incomplete proof, Lean.trustCompiler means trust in native evaluation, and anything else means a custom axiom on which the result is conditional.

A list of axioms also says what kind of result a theorem is. A theorem whose list omits Classical.choice uses no classical reasoning obtained from it, and one with an empty list holds in the type theory alone. The check can be made permanent. The manual suggests pairing #print axioms with #guard_msgs, so that a change in a library one depends on cannot silently add an axiom:

/-- info: 'two_add_two' does not depend on any axioms -/
#guard_msgs in
#print axioms two_add_two

If the proof of two_add_two ever came to depend on an axiom, the message would change, and this command would fail.

Next

Classical logic from choice follows the third axiom into excluded middle.