Proving double negation elimination implies LEM

Stream: lean4

[James Sully]

From Theorem Proving in Lean 4:

One consequence of the law of the excluded middle is the principle of double-negation elimination:

open Classical

theorem dne {p : Prop} (h : ¬¬p) : p :=
  Or.elim (em p)
    (fun hp : p => hp)
    (fun hnp : ¬p => absurd hnp h)

Double-negation elimination allows one to prove any proposition, p, by assuming ¬p and deriving false, because that amounts to proving ¬¬p. In other words, double-negation elimination allows one to carry out a proof by contradiction, something which is not generally possible in constructive logic.
As an exercise, you might try proving the converse, that is, showing that em can be proved from dne.

I have no idea how to approach this exercise.

theorem emFromDne {p : Prop} (dne : ¬¬p → p) : (p ∨ ¬p) :=
  sorry

any hints?

[Floris van Doorn]

IIRC you want to prove this with the quantifiers a bit differently: (∀ p, ¬¬ p → p) → ∀ p, p ∨ ¬ p

[James Sully]

are you sure? quantifiers are chapter 4, this exercise is from chapter 3!

[James Sully]

https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#classical-logic

[Reid Barton]

emFromDne is not provable constructively

[James Sully]

yep, that seems to be the point of this section of the chapter, not that I entirely understand that point

[Floris van Doorn]

Yes, the exercise probably has to be moved/removed.

If you want to go a bit deeper: take a look at the Free Heyting Algebra on one variable. These are all the propositions you can state with one (propositional) variable, up to constructive equivalence. The ordering relation corresponds to the implications you can constructively prove. Since ¬¬ p → p is higher than p ∨ ¬ p, you can prove the former from the latter, but not the other way around.

[James Sully]

Ok, I don't really understand that, but I'll take your word for it that I should move on.

[James Sully]

appreciate the help!

[James Sully]

Do you know of a good easy to grok introduction to the distinction between constructive and classical logic?

[Dan Velleman]

I think what is meant in Theorem Proving in Lean is that if you take dne as an axiom, then you can prove em:

axiom dne {p : Prop} (h : ¬¬p) : p

theorem em {p : Prop} : p ∨ ¬p :=

[Michiel Huttener]

Floris van Doorn said:

Yes, the exercise probably has to be moved/removed.

For what it's worth: I read this part last week and was also confused. Here is my elementary solution:

theorem dne {p : Prop} (h : ¬¬p) : p := sorry

-- Exercise 9 in "Examples of Propositional Validities"
theorem demorgan {p q: Prop} : ¬(p ∨ q) → ¬p ∧ ¬q :=
  fun h : ¬(p ∨ q) => ⟨fun hp : p => h (Or.inl hp), fun hq : q => h (Or.inr hq)⟩

theorem em {p : Prop} : p ∨ ¬p :=
  suffices hnn : ¬¬(p ∨ ¬ p) from dne hnn
  fun hn =>
    let h := demorgan hn
    have hp : p := dne (h.right)
    have hnp : ¬p := h.left
    hnp hp

I think if the extra explanation by @Dan Velleman was provided in the text, it would be clear what to do.