Zulip Chat Archive

Stream: new members

Topic: double negation implies excluded middle??


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

view this post on Zulip Mario Carneiro (Nov 07 2018 at 08:58):

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

view this post on Zulip Mario Carneiro (Nov 07 2018 at 09:00):

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

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

view this post on Zulip Rob Lewis (Nov 07 2018 at 09:00):

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

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

view this post on Zulip Shaun Steenkamp (Nov 07 2018 at 09:55):

Thanks for your help!


Last updated: May 13 2021 at 06:15 UTC