Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Oct 28 2019 at 14:53):

in Lean at least

view this post on Zulip 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".

view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 28 2019 at 15:20):

¬I basically says:

 φ⊢⊥
-----
  ¬φ

view this post on Zulip 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