Skip to content

Skipping a check: Lean's three axioms, read with an unchecked value

Vitaly Reznik

Every theorem of ZTL in Lean is proved with none of Lean's three standard axioms; the repository's audit checks each one (3 004 on 2026-11-06). This is a choice of method, and its reason was not technical: a proof should build what it claims, not refer to a principle that grants it. That was an intuition. This page adds a reading. My reading: each of the three axioms licenses skipping a check, and ZTL is a logic about what has and has not been checked. Read with ZTL's values, the ZTL version of each fails on an input nobody checked and holds on inputs that were. That is a fact about ZTL, not about Lean; what it supports is the method, not a verdict on the axioms.

On this page proved marks a theorem checked in Lean 4, a proof assistant in which a machine checks every step, using none of the three axioms discussed here. My reading marks what I take the results to mean. Open marks what is not settled.

Terms

  • ZTL's values: T (true, checked), F (false, checked) and Z (not checked: the input of someone else, which may change between two reads). Because it may change, ZTL reads each occurrence of a Z on its own (the dirty rule): p and p with p = Z may be read as "true and false".
  • A connective answers T only if T is forced under every way of reading its inputs, and F otherwise. So "Z and Z" is F, and "not Z" is F too (Z read as true makes "not Z" false). This is ZTL's own definition, stricter than Kleene's; the results below depend on it and on the dirty rule.
  • A value is clean if it is T or F, and dirty if it is Z. Z is the only dirty value.
  • Lean's three standard axioms:
  • propext: two propositions that imply each other are equal.
  • Quot.sound: two elements related by an equivalence have equal classes. (Quotients themselves are built into Lean's kernel; this is the axiom that makes related elements' classes equal.) Function extensionality follows from it together with those built-in quotients: two functions that agree on every input are equal.
  • Classical.choice: from the bare fact that something exists, a particular one may be picked. The law of the excluded middle ("A or not A") follows from it, together with the other two (Diaconescu's theorem).
  • This page reads propext directly, Quot.sound through function extensionality, and Classical.choice both through the excluded middle and, on finite sets, directly.

What is already known

  • In Lean these three are declared as axioms, added because ordinary mathematics uses them (Lean's documentation lists them, and #print axioms shows which a proof uses).
  • Brouwer questioned the excluded middle ("The untrustworthiness of the principles of logic", 1908), above all for infinite totalities. Constructive mathematics in Bishop's style (1967) rejects the general axiom of choice, while usually accepting its countable and dependent forms.
  • None of this is new. What is added here is one reading: each axiom checked against a value that marks "not checked".

Equivalent is not interchangeable, until the inputs are checked

propext lets you swap two statements that imply each other, anywhere.

Take p and p and p. Each is T exactly when the other is, so they imply each other. Now put them under "not". At p = Z, the dirty rule reads the two occurrences of p on their own, so "p and p" is not forced and answers F, and "not F" is T. Yet "not p" is F. So the two statements imply each other, and one context still tells them apart. If both occurrences were read as one (the judge's "if stable"), p and p would just be p, and the example would disappear: the failure is the dirty rule at work. On clean values it cannot happen. Two clean values that are T in the same cases are equal, and equal values can be swapped in any context.

Proved. a = T exactly when a and a = T, for every value a; at Z, "not (Z and Z)" is T and "not Z" is not (ZAxiomsRead.propext_fails_dirty). Without the condition "clean", being T in the same cases does not give equality: F and Z are both "not T" and differ (ZAxiomsRead.propext_needs_clean). For clean a and b it does, and then f(a) = f(b) for every function f (ZAxiomsRead.propext_clean).

Agreeing on every observation is not sameness, except for one connective

Function extensionality says that two functions agreeing on every input are the same. Weaken "every input" to "every input we could check", and ZTL refutes it. x and x and x agree on T and on F, and differ at Z: "Z and Z" is F.

There is a precise boundary. A single connective of ZTL is fixed by its clean values. Its answer at Z is computed from its answers at T and F, so two single connectives that agree on T and F agree everywhere. Two compound formulas need not. The same boundary appears for ZTL read through probabilities: each table is the "certain" end of its probability interval, but only per connective, not per formula (proved there; see How likely, and joined how?).

Proved. x and x = x for every clean x, while "Z and Z" is not Z (ZAxiomsRead.funext_obs_fails). Two one-argument connectives whose ZTL tables agree at T and at F agree everywhere (ZAxiomsRead.funext_obs_lift1). Two two-argument connectives with the same classical table have the same ZTL table, Z cells included (ZAxiomsRead.funext_obs_lift2).

"A or not A" is settled for checked A, and not for unchecked A

Proved. "Z or not Z" is not T (ZAxiomsRead.lem_fails_dirty); for every clean a, "a or not a" is T (ZAxiomsRead.lem_clean).

ZTL's judge passes this on to its readers. When every input of a claim is checked, its report carries a mark saying so, which is where the results above license classical reasoning. With an unchecked input, a probability strictly between 0 and 1, or a search that found nothing, the mark is absent. That is the tool's behaviour, tested, not part of the theorems. You can try it in the studio.

The axiom of choice itself: a value nobody checked, used the same everywhere

The axiom of choice says that every family of non-empty sets has a choice function, one picking an element from each set without saying how. Its content lies in infinite families: for one non-empty set, or finitely many, a pick needs no axiom. What can be read in ZTL is the pick itself. An element that no one can exhibit is, to ZTL, an unchecked value, a Z. But it is not ZTL's ordinary Z, which is read anew at each occurrence: a choice function is one function, so within it the pick is the same element wherever it is used. Read this way, choice hands over an unchecked value with a promise of stability.

Proved (lean/ZChoiceRead.lean, finite lists, none of Lean's three axioms):

  • if a property holds of every element, it holds of the pick however its uses are read (ZChoiceRead.invariant_earned; a sanity check of the encoding rather than a discovery);
  • "the two uses denote the same element" holds at every stable reading and fails at some independent reading once the list has two elements (ZChoiceRead.same_pick);
  • "the pick is this element" holds at one stable reading and fails at another: neither earned nor refuted, OPEN (ZChoiceRead.which_pick);
  • from finitely many non-empty lists, a choice function is built, with no axiom: take each list's first element (ZChoiceRead.finite_choice; a list is given in some order, and that order does the choosing).

My reading. The judge already has a word for the second kind: EARNED IF STABLE, true provided an unchecked value reads the same wherever it is used. So I read the axiom of choice, in ZTL's terms, as that condition stipulated for infinitely many picks at once. That is a reading of the infinite case; the proofs are about finite ones. It also suggests why Banach–Tarski needs choice: its construction uses one set of representatives, the same in every piece, and that sameness is what the stable reading supplies and the dirty reading does not.

The predecessor: Hilbert's ideal elements. This reading has a close ancestor. In the early 1920s Hilbert added to logic the ε-term: εx.P(x), read as some x with P if there is one, governed by one axiom, the critical axiom: if anything has P, then εx.P(x) has P. It is a choice principle built into the logic, an "ideal element", and Ackermann and von Neumann worked on eliminating it in the 1920s. In Grundlagen der Mathematik II (1939) Hilbert and Bernays proved the epsilon theorems: under stated conditions (the conclusion and the non-logical axioms free of ε), what is derivable with ε-terms is derivable without them. The elimination works on proofs, and can make them vastly longer. So, by Hilbert's own theorems, this form of choice adds nothing to statements that do not mention it, which fits the reading above: what holds whatever the pick is needs no pick.

Proved (lean/ZEpsilon.lean, for a non-empty finite list and a property that can be computed): call a pick admissible if it obeys the critical axiom. Then "P holds of the pick" holds for every admissible pick exactly when some element has P (ZEpsilon.eps_iff_exists). One direction is the critical axiom; the other needs a witness, and it is found by searching the list, so no excluded middle is used. For a property that cannot be computed this would not go through: there, the critical axiom is known to bring the excluded middle with it. Which element an admissible pick is stays undetermined (ZEpsilon.eps_which_open), and two admissible picks can differ (ZEpsilon.eps_needs_stable). These are statements about lists in ordinary logic; the ZTL reading of them is the reading above, not formalised here.

My reading. For P(ε) itself, then, earning it for every admissible pick says no more than the ε-free "something has P", a finite, semantic counterpart of what the epsilon theorems do with proofs. What ZTL adds is to make two readings of an unchecked value explicit and to let the judge tell them apart: read anew at each use, like data from someone else, or the same everywhere, like a choice. Hilbert's tradition knew the issue in its own terms: provisional values of ε-terms are revised in the ε-substitution method, and when two ε-terms may be identified is a known question.

Infinity, in the same light

ZTL does not reject infinity. What it declines is to treat a survey of an infinite domain as an act, something done. Its published account (the ZTL paper, v2.1, section 6 and the section on Yablo's paradox) says so in three places:

  • A claim about every member of an infinite domain is T only if every instance is strictly T. No survey can show that. Only a rule can, that is, a proof.
  • Two real numbers given digit by digit: "they differ" is earned as soon as two digits differ. "They are equal" stays unchecked at every finite stage.
  • Yablo's paradox lives only at actual infinity: every finite truncation of it has a consistent assignment, measured there, and the limit is a theorem (ZYablo.lean).

My reading. It is the same pattern as the axioms. An infinite totality treated as finished is a "for all" read as checked when no one checked it. An infinite domain given by a rule is not; its "for all" is earned by proof. So ZTL does not ask whether infinity exists. It asks whether a claim about it was earned. The companion page A root is shown, an absence is proved works this out for equations in whole numbers.

What it means

My reading. Each axiom is a licence to skip a check: equivalent may be swapped, agreement on observations is identity, "A or not A" is settled. ZTL shows that each licence is sound exactly where nothing dirty is involved. So keeping the axioms out is zero trust applied to the foundations themselves. And their checked versions are usable tools, with the condition written in: swap equivalents when the inputs are clean; identify single connectives by their clean values; use "A or not A" on checked statements.

This does not make the axioms false in Lean. Lean with them is consistent relative to ZFC with inaccessible cardinals (Carneiro, 2019), and they hold in its usual set-theoretic model. A proof that uses none of them stays valid if someone adds them later. The claim here is narrower: their readings inside ZTL break on unchecked data. For a corpus whose subject is what has been checked, that is a reason to keep them out by default; it is a reason of method, not a refutation.

Open

  • The reading of choice above is proved for finite sets, where choice needs no axiom. For infinitely many sets it is a reading, not a theorem: the axiom is needed there, and what it costs is shown by Banach–Tarski.
  • Whether the axiom-free fragment of Lean is as strong as Lean with its axioms is not settled. Mario Carneiro, who determined Lean's strength with its axioms (The Type Theory of Lean, 2019), has said on the Lean community forum (2022) that he expects it to be about the same.

The code

In the public ZTL repository, github.com/inventor1975/ZTL:

  • lean/ZAxiomsRead.lean: the eight theorems above, with their #print axioms lines.
  • lean/ZChoiceRead.lean: the reading of choice, five theorems.
  • lean/ZEpsilon.lean: Hilbert's ε on a finite domain, five theorems.
  • lean/ZAlgebra.lean, ZAlgebra.not_selfextensional: the propext failure, as stated in ZTL's algebraic study.
  • SPEC.md, section "Lean's three axioms, read in ZTL".

Written with AI assistance (Claude Opus 5.5, Anthropic): the theorems, programs and this text. Idea, direction, editing and responsibility: Vitaly Reznik.