## Stream: new members

### Topic: How to prove law of excluded middle from double negation?

#### agro1986 (Oct 28 2019 at 14:51):

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 (Oct 28 2019 at 14:52):

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.

in Lean at least

#### Bryan Gin-ge Chen (Oct 28 2019 at 14:56):

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

#### agro1986 (Oct 28 2019 at 15:08):

@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 (Oct 28 2019 at 15:10):

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

#### Reid Barton (Oct 28 2019 at 15:13):

(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 (Oct 28 2019 at 15:15):

It's easier with the nesting structure displayed

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


#### Kenny Lau (Oct 28 2019 at 15:18):

| ¬ (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 (Oct 28 2019 at 15:19):

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

#### Kenny Lau (Oct 28 2019 at 15:20):

¬I basically says:

 φ⊢⊥
-----
¬φ


#### agro1986 (Nov 01 2019 at 13:09):

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

Last updated: May 16 2021 at 05:21 UTC