What the axioms are

Technical version: The three axioms· Classical logic from choice· Quotient types

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

Every proof Lean accepts rests on two things: the rules of Lean's logic, and whatever axioms the proof uses, statements assumed without proof. Lean itself provides three. This page says what each one says in plain words, why the third makes Lean's logic the classical logic most mathematicians use, and how to ask Lean which axioms a given theorem depends on.

Rules and axioms

The rules of Lean's logic say how types, functions and inductive definitions work, and how proofs are built from them. Much can be proved with these rules alone, with no axioms at all, as the example at the end of this page shows.

An axiom is something more. In Lean it is a new constant of a given type, simply postulated. When the type is a proposition, the axiom is an assumed proof of it. That makes axioms dangerous. Lean cannot check that an axiom is consistent with the rest of the logic, and an axiom that is false lets every statement be proved. Any proof that relies on an axiom is only as good as the axiom.

For this reason Lean keeps track of the axioms beneath every theorem, so that they can be audited. And the three that Lean provides are well studied; Lean's reference manual describes them as known to be consistent.

Propositional extensionality

The first axiom, propositional extensionality (Lean's name is propext), says: if two propositions imply each other, they are equal.

In plain words, a proposition is identified by when it is true, not by how it is worded. "p and true" holds in exactly the cases where p holds, so by this axiom it is the same proposition as p, and one may be replaced by the other anywhere. This fits the reading of a proposition as a type that is either empty, when it is false, or has a single element, when it is true. It is also acceptable to constructive mathematicians.

Quotient soundness

The second axiom concerns quotients. A quotient is a new type made from an old one by declaring some of its values to count as the same. The fractions 1/2 and 2/4 are different pairs of numbers but the same rational number; the numbers 3 and 10 are different, but the same when counting in sevens. The page on quotient types treats the construction.

Lean's logic provides the construction itself. The axiom, quotient soundness (Quot.sound), supplies the one fact that makes it a real quotient: values declared to count as the same become equal in the quotient.

A useful consequence follows from it: function extensionality, the principle that two functions giving equal results on every input are equal. In Lean this is a theorem proved from quotients, not a separate axiom.

Choice

The third axiom, choice (Classical.choice), says: from the bare knowledge that a type has at least one value, one may obtain a value of it.

In plain words: if you know that something exists, you may name one, without saying how to find it. Mathematicians use this freely. For a program it is strange, because the knowledge that something exists, being a proof, carries no information about where to look. The authors of Theorem Proving in Lean 4 describe choice as entirely at odds with a computational reading, and Lean requires any definition that uses it to produce data to be marked noncomputable.

Why choice makes the logic classical

Without axioms, Lean's logic is constructive. To prove "P or Q" one must supply a proof of one side and say which, as the page on propositions as types describes. In such a logic the law of the excluded middle, "every proposition is either true or false", cannot be proved in general, because nothing tells us which side holds.

Choice changes this. A result known as Diaconescu's theorem, after a paper by Radu Diaconescu of 1975, shows that choice together with the two extensionality principles proves the law of the excluded middle. Lean's core library proves it that way, and with it the familiar classical methods: proof by contradiction, proof by cases on whether a statement holds, and the elimination of double negation. So the three axioms together give the classical logic that most of mathematics is written in. The page on classical logic from choice gives the proof.

The price is paid in computation, not in correctness. Proofs are dropped when Lean compiles a program, so a program whose proofs use any of the three axioms still runs; what Lean cannot compile is a definition that obtains data from choice. When Lean's kernel evaluates an expression, the axioms can also stop the evaluation before it reaches an answer.

Asking Lean

The command #print axioms, followed by the name of a theorem or definition, lists every axiom it depends on, directly or through other theorems it uses. Here are three small theorems: that "p and q" implies "q and p"; that "p and true" is the same proposition as p; and the law of the excluded middle, taken from Lean's core library.

theorem swap (p q : Prop) : p ∧ q → q ∧ p := fun ⟨hp, hq⟩ => ⟨hq, hp⟩
theorem same_prop (p : Prop) : (p ∧ True) = p := propext ⟨fun h => h.1, fun h => ⟨h, trivial⟩⟩
theorem either (p : Prop) : p ∨ ¬p := Classical.em p
#print axioms swap
#print axioms same_prop
#print axioms either

Lean 4.34.1 prints:

'swap' does not depend on any axioms
'same_prop' depends on axioms: [propext]
'either' depends on axioms: [propext, Classical.choice, Quot.sound]

The first proof uses only the rules of the logic. The second uses propositional extensionality, by name. The third uses all three axioms, because Lean's proof of the excluded middle goes through choice and the two extensionality principles.

Other names that can appear

The list printed by #print axioms is the place to look for anything that weakens a proof.

• sorryAx appears when a proof, or a theorem it relies on, is unfinished. Lean lets a proof be left open with the word sorry while work goes on; such a proof proves nothing.
• A name containing _native means that part of the proof was settled by running compiled code, so the result also trusts Lean's compiler and not only Lean's kernel.
• Any other name is an axiom someone added, and the theorem holds only if that axiom is true.

Lean's reference manual recommends exactly this check: a finished theorem should report no axioms beyond the three standard ones. Principia Machina applies the same test to its own Lean sources; see the move to Lean.

Next

• Two kinds of equality: the two kinds of equality in Lean, and why the difference matters.