Lean theorem prover/Foundations/Classical logic from choice

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

The rules of Lean's type theory, taken alone, are constructive: to assert p ∨ ¬p is to know which of the two disjuncts holds, and for an arbitrary p that is not known. Lean does not add excluded middle as an axiom. It proves it, as the theorem Classical.em, from the axiom of choice together with propositional and function extensionality. The argument is known as Diaconescu's theorem. This page follows the proof as Lean's core library carries it, then the decidability of every proposition that follows from it, the noncomputable marker, and what is lost computationally.

The statement

#check @Classical.em
#print axioms Classical.em

Classical.em : ∀ (p : Prop), p ∨ ¬p
'Classical.em' depends on axioms: [propext, Classical.choice, Quot.sound]

All three axioms of the three axioms appear. Quot.sound enters through funext, which Lean proves from quotients.

The argument

Fix a proposition $p$. Define two predicates on propositions:

$U(x):\equiv (x=\mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e})\vee pV(x):\equiv (x=\mathrm{F}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e})\vee p$

Each is inhabited: $U(\mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e})$ and $V(\mathrm{F}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e})$ hold by their left disjuncts. Choice therefore yields a proposition $u$ with $U(u)$ and a proposition $v$ with $V(v)$. Two facts follow.

First, either $u\ne v$ or $p$. Each of $U(u)$ and $V(v)$ is a disjunction, giving four cases. If either right disjunct holds, $p$ holds. In the remaining case $u=\mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}$ and $v=\mathrm{F}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}$, and since $\mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}\ne \mathrm{F}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}$, $u\ne v$. This step is a case analysis on proofs of disjunctions, and it produces a proposition, so it is permitted.

Second, $p$ implies $u=v$. If $p$ holds, both predicates are true of every $x$, so $U(x)$ and $V(x)$ are equivalent for each $x$. Propositional extensionality makes them equal for each $x$, and function extensionality makes $U=V$. The choice function applied to equal predicates gives equal results, so $u=v$.

Combining the two: if $u\ne v$, the second fact gives $\mathrm{\neg }p$; otherwise $p$. Either way $p\vee \mathrm{\neg }p$.

The core library's proof, in Init/Classical.lean, follows exactly these steps. Below is a copy, lightly condensed, in which one case is closed by an explicit term where the original calls simp:

open Classical in
theorem em' (p : Prop) : p ∨ ¬p :=
  let U (x : Prop) : Prop := x = True ∨ p
  let V (x : Prop) : Prop := x = False ∨ p
  have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
  have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
  let u : Prop := choose exU
  let v : Prop := choose exV
  have u_def : U u := choose_spec exU
  have v_def : V v := choose_spec exV
  have not_uv_or_p : u ≠ v ∨ p :=
    match u_def, v_def with
    | Or.inr h, _ => Or.inr h
    | _, Or.inr h => Or.inr h
    | Or.inl hut, Or.inl hvf =>
      Or.inl fun huv => true_ne_false (hut.symm.trans (huv.trans hvf))
  have p_implies_uv : p → u = v := fun hp =>
    have hpred : U = V :=
      funext fun _ => propext ⟨fun _ => Or.inr hp, fun _ => Or.inr hp⟩
    have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
      rw [hpred]; intros; rfl
    h₀ _ _
  match not_uv_or_p with
  | Or.inl hne => Or.inr (mt p_implies_uv hne)
  | Or.inr h => Or.inl h

#print axioms em'

The last line prints 'em depends on axioms: [propext, Classical.choice, Quot.sound]. The step h₀ is where the choice function is shown to respect equality of predicates. After rewriting U to V, the two sides are choose applied to the same predicate and to two proofs of the same proposition, and rfl closes the goal because those proofs are definitionally equal.

Where the strength comes from

The essential ingredient is not choice alone but choice combined with extensionality. Constructive systems such as Bishop's constructive analysis and Martin-Löf's type theory affirm a form of the axiom of choice, the statement that $\mathrm{\forall }x\mathrm{\exists }y\varphi (x,y)$ gives a function $f$ with $\mathrm{\forall }x\varphi (x,f(x))$, without affirming excluded middle. Bell's survey explains why there is no conflict. On a constructive reading that choice principle follows from what existence means. The derivation of excluded middle needs more: besides choice, it uses a comprehension principle and the extensionality of functions on predicates, so a constructive system that affirms choice but not excluded middle must give up one of the two; Bell finds a constructive justification for comprehension but none for extensionality. Lean asserts both. Its Classical.choice is a single global choice function on all inhabited types, and propext with funext makes it extensional. Once a choice function must give equal answers on equivalent predicates, it can be made to decide $p$.

Diaconescu first derived excluded middle from the axiom of choice, in 1975, in a category-theoretic setting. Goodman and Myhill's note of 1978 is titled "Choice implies excluded middle". Bell traces the idea of the proof presented above, with two predicates and an extensional choice function, to Goodman and Myhill, whose note built on Diaconescu's result. Lean's documentation names the theorem after Diaconescu.

Decidable and propDecidable

The disjunction p ∨ ¬p is a proposition, and an inductive proposition with two constructors can be eliminated only into propositions. A program therefore cannot branch on it. For branching Lean uses a different type, Decidable p, whose two constructors carry the same information as the two disjuncts but which lives in Type:

#print Decidable
#check @Classical.propDecidable
#eval decide (2 < 3)
example : decide (2 < 3) = true := rfl

inductive Decidable : Prop → Type
number of parameters: 1
constructors:
Decidable.isFalse : {p : Prop} → ¬p → Decidable p
Decidable.isTrue : {p : Prop} → p → Decidable p
Classical.propDecidable : (a : Prop) → Decidable a
true

An if expression asks for a Decidable instance of its condition. For 2 < 3 the instance is an algorithm on natural numbers, so decide (2 < 3) evaluates to true, both in compiled code and by rfl. Classical.propDecidable supplies an instance for every proposition. It is defined by applying Classical.choice to the fact, given by Classical.em, that Decidable a is inhabited. It is a scoped instance of low priority, active only after open Classical, so that where an ordinary instance also applies, the ordinary one is tried first.

Noncomputable definitions

A definition that uses the classical instance to produce data cannot be compiled, and Lean requires it to say so:

open Classical in
noncomputable def classify (p : Prop) : Bool := if p then true else false

theorem classify_true : classify True = true := by
  simp [classify]

#print axioms classify
#print axioms classify_true
#reduce classify True

'classify' depends on axioms: [propext, Classical.choice, Quot.sound]
'classify_true' depends on axioms: [propext, Classical.choice, Quot.sound]
Decidable.rec (fun h => false) (fun h => true) (Classical.choice ⋯)

Without the marker the same definition is refused:

open Classical in
def classify' (p : Prop) : Bool := if p then true else false

Lean reports: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'propDecidable', which is 'noncomputable'.

What is lost

Three things are lost when data is obtained from choice, and one is kept.

Evaluation. #reduce classify True stops at Classical.choice, an axiom with nothing to unfold. The term is a closed Bool that is neither true nor false by computation, although classify_true proves that it equals true. Theorem Proving in Lean 4 describes a "computationally pure" fragment of Lean in which every closed term of type Nat reduces to a numeral; a definition that uses choice for data lies outside it.

Compilation. There is no code to generate for an axiom, so such a definition cannot be run, as the refusal above shows.

Information. A classical existence proof does not say how to find the object, and a function defined with Classical.choose does not say which object it picked. Theorem Proving in Lean 4 illustrates this with a left inverse of an injective function: a function from a classical point of view, unacceptable from a constructive one, since there is in general no way to implement it.

What is kept is classical reasoning in proofs. Proofs are erased when Lean compiles a definition, so excluded middle, proof by contradiction and the other classical principles may be used freely to establish properties of programs that themselves compute. Theorem Proving in Lean 4 puts the line exactly there: classical principles are compatible with code generation so long as they are not used to manufacture data. The noncomputable marker, not the axiom list, shows on which side of the line a definition falls: a theorem proved with excluded middle lists Classical.choice among its axioms, yet the programs it is about still run.

Next

Proof irrelevance and subsingleton elimination explains why a proof of p ∨ ¬p cannot be used to branch, while a proof of an equation can be used to cast.