Zulip Chat Archive

Stream: new members

Topic: double negation implies excluded middle??


Shaun Steenkamp (Nov 07 2018 at 08:56):

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 (Nov 07 2018 at 08:58):

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

Mario Carneiro (Nov 07 2018 at 09:00):

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

Rob Lewis (Nov 07 2018 at 09:00):

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

Rob Lewis (Nov 07 2018 at 09:00):

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

Shaun Steenkamp (Nov 07 2018 at 09:55):

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 (Nov 07 2018 at 09:55):

Thanks for your help!


Last updated: Dec 20 2023 at 11:08 UTC