double negation implies excluded middle??

Stream: new members

[Shaun Steenkamp]

In section "3.5 Classical Logic" it says that "As an exercise, you might try proving the converse, that is, showing that em can be proved from dne." Can someone give me a proof of this in Lean without using open classical?

[Mario Carneiro]

hint: use it right at the start. That is, ¬ ¬ (p ∨ ¬ p) is provable outright

[Mario Carneiro]

hint 2: try to prove ¬ p from the assumption ¬ (p ∨ ¬ p)

[Rob Lewis]

Notice that Jeremy also gave you a hint here: https://github.com/leanprover/theorem_proving_in_lean/issues/67

[Rob Lewis]

(The same hint Mario is giving. :slight_smile: )

[Shaun Steenkamp]

Okay, I got it! I had to try it in Agda first because I'm still not really familiar with the syntax of Lean

[Shaun Steenkamp]

Thanks for your help!