How to prove law of excluded middle from double negation?

Stream: new members

[agro1986]

The tutorial here: https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html#classical-logic gives the challenge "As an exercise, you might try proving the converse, that is, showing that em (excluded middle) can be proved from dne (double negation)."

I'm able to make the skeleton:

variable (p: Prop)
axiom dne: ¬¬p → p

theorem em: p ∨ ¬p := sorry

However I really have no clue on how to prove it. I found a proof here: https://proofwiki.org/wiki/Double_Negation_Elimination_implies_Law_of_Excluded_Middle

But isn't line 2 and 5 basically invoking the technique of excluded middle?

If anyone would give hint on how to prove it in Lean, I would be helpful. Thanks

[Reid Barton]

But isn't line 2 and 5 basically invoking the technique of excluded middle?

No, because "if p, then false" is the definition of ¬p.

[Kenny Lau]

in Lean at least

[Bryan Gin-ge Chen]

This is a pretty popular question here, if you want some spoilers, search zulip for "dne em".

[agro1986]

@Reid Barton On that link, line 2 is "assume p". After the writer established that it leads to contradiction, on line 5 the writer said "so assume not p". That means the writer used "p or not p" to prove "p or not p"?

[Reid Barton]

Line 5 is stating that we have "not p", because we proved (lines 2-4) that "p" implies false.

[Reid Barton]

(This style of proof is hard to follow, in my opinion, if you don't already know what is supposed to be happening.)

[Reid Barton]

It's easier with the nesting structure displayed

| ¬ (p ∨ ¬ p)
| | p
| | p ∨ ¬ p
| | ⊥
| ¬ p
| p ∨ ¬ p
| ⊥
¬ ¬ (p ∨ ¬ p)
p ∨ ¬ p

[Kenny Lau]

| ¬ (p ∨ ¬ p)   [assumtion]
| | p             [assumption]
| | p ∨ ¬ p       [∨I.L 2]
| | ⊥             [¬E 1 3]
| ¬ p           [¬I 2-4]
| p ∨ ¬ p       [∨I.R 5]
| ⊥             [¬E 1 6]
¬ ¬ (p ∨ ¬ p) [¬I 1-7]
p ∨ ¬ p       [¬¬E 8]

[Kenny Lau]

I is introduction and E is elimination and L is left and R is right and the numbers are line numbers

[Kenny Lau]

¬I basically says:

 φ⊢⊥
-----
  ¬φ

[agro1986]

@Kenny Lau @Reid Barton after playing around and mulling it over I finally understand it!!! Thanks a lot for the kind explanation!