LEM Ain't False

Whether or not the Law of the Excluded Middle is true is the subject of much debate. But we know for sure that it’s not false. Let’s see how to prove this in Lean.

First, the statement of the result:

/-- The Law of the Excluded Middle isn't false. -/
theorem em_not_false : ¬¬(p ∨ ¬p) :=
  sorry

That is: it’s not the case that the Law of the Excluded Middle is false.

In Lean (and elsewhere), ¬p is just an abbreviation for the type p → False, which means that em_not_false is a function:

theorem em_not_false : ¬¬(p ∨ ¬p) :=
  fun (hNotEm : ¬(p ∨ ¬p)) =>
    sorry

That is, it’s a function that transforms a hypothesis that EM is False into a proof of False. According to the Curry-Howard Isomorphism, fun (h : p) => ... can be interpreted as Supposing p is True, .... So we’re supposing that EM isn’t True, and in this hypothetical context we need to derive a proof of False.

But before we finish the proof of em_not_false, we should observe that it’s obviously true. And by this I mean that if em were False, our whole theorem-proving edifice would crumble. To see why, let’s add em_false as an axiom:

axiom em_false (p: Prop) : ¬(p ∨ ¬p)

What em_false says is:

For any proposition p, given either a proof of p or a proof of ¬p, I’ll give you a proof of False.

Let’s try it out with the simplest proposition of all:

/--  A proof of `False` using `em_false` and a proof of `True`. -/
theorem false_from_true : False :=
  em_false True (Or.inl trivial)

And with that the jig is up: if we can prove False, we can prove anything at all, a property captured by the elimination principle for False:

#check False.elim
-- {C : Sort u} → False → C

Using false_from_true and False.elim we can prove that 1 is equal to 2:

theorem one_eq_two : 1 = 2 := False.elim false_from_true

That every natural number is equal to 0:

theorem all_zero : ∀ n : Nat, n = 0 := False.elim false_from_true

Along with anything else under the sun.

Finishing the Proof

So having a proof that em is False amounts to having a tool of incredible power. And that’s exactly what hNotEm is in our incomplete proof of em_not_false. Unforunately it’s not as simple as our proof of false_from_true, since we can only use hNotEm with the parameterized p proposition. But it’s not too much more work.

The trick is to use hNotEm to construct proofs of both ¬p and ¬¬p. Once we have these, we can construct a proof of False using absurd. absurd implements the Principle of Explosion, also known as “ex falso quodlibet” (“from a contradiction, anything follows”):

#check absurd
-- {a : Prop} → {b : Sort v} → a → ¬a → b

To see if the general arc of the proof works, we can temporarily strong-arm Lean using sorry:

theorem em_not_false : ¬¬(p ∨ ¬p) :=
  fun (hNotEm : ¬(p ∨ ¬p)) =>
    let hNotP : ¬p := sorry
    let hNotNotP : ¬¬p := sorry
    absurd hNotP hNotNotP

And now it’s simply a matter of proving hNotP and hNotNotP. Writing out the type of hNotEm as a function gives a clue to how we might do this:

hNotEm : (p ∨ ¬p) → False

This says:

Given either a proof of p or a proof of ¬p, I’ll give you a proof of False.

At this point we seem stuck. We don’t have a proof of p or ¬p. But the trick is to use hNotEm inside another “hypothetical”. Specifically, here’s a proof of ¬p using hNotEm:

hNotP : ¬p := fun (h : p) => hNotEm (Or.inl h)

We can prove hNotNotP with the same trick:

hNotNotP : ¬¬p := fun (h : ¬p) => hNotEm (Or.inr h)

And that completes the proof:

theorem em_not_false : ¬¬(p ∨ ¬p) :=
  fun (hNotEm : ¬(p ∨ ¬p)) =>
    let hNotP : ¬p := fun (h : p) => hNotEm (Or.inl h)
    let hNotNotP : ¬¬p := fun (h : ¬p) => hNotEm (Or.inr h)
    absurd hNotP hNotNotP

Notes

In Lean, em is actually a theorem, not an axiom. It’s proven using the axiom of choice, a result known as Diaconescu’s theorem. The axiom of choice is an axiom in Lean.