Zulip Chat Archive

Stream: new members

Topic: proving em from dne


view this post on Zulip Luis Berlioz (Jun 06 2019 at 20:27):

Hi, first question here. In section 3.5 Classical Logic of Theorem Proving in Lean, we're asked to prove excluded middle (em) from (double negative) dne. I'm not sure if I get what we're supposed to show. Please check my answer, particularly I am not sure if my hypothesis should be h: (not not p -> p) or the simpler one (that seems to work) h: not not p. Thanks

open classical

theorem dne {p : Prop} (h : ¬ ¬ p) : p :=
or.elim (em p)
(assume hp : p, hp)
(assume hnp : ¬ p, absurd hnp h)

theorem notp {p: Prop} (h: ( ¬ ¬ p )) :  p  ¬ p :=
have  hpp: p, from dne h,
show p  ¬ p, from or.inl hpp

variable p: Prop
variable k : ¬ ¬ p
#check notp k         -- notp k : p ∨ ¬p

view this post on Zulip Mario Carneiro (Jun 06 2019 at 20:29):

You can either prove notp using by_contradiction, or you can prove

theorem notp {p: Prop} (dne:  p, ¬ ¬ p  p) :  p  ¬ p := sorry

without referencing any classical axioms

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 20:30):

Yes, I would imagine that you're not supposed to be assuming any classical stuff here or else you can just prove excluded middle from nothing.

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 20:31):

theorem notp {p: Prop} (dne: ∀ q, ¬ ¬ q → q) : p ∨ ¬ p := sorry

I think it's a bit less confusing if you use different letters for the free and bound variables, but of course it makes no difference to Lean.

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 20:49):

I found these exercises so weird because as a mathematician I sort-of don't care how to do them but it was still irritating struggling to do them.

view this post on Zulip Luis Berlioz (Jun 06 2019 at 20:50):

I think it's a bit less confusing if you use different letters for the free and bound variables, but of course it makes no difference to Lean.

good point. Thanks

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 20:53):

Check out the bottom of https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html#lab202

view this post on Zulip Luis Berlioz (Jun 06 2019 at 20:54):

You can either prove notp using by_contradiction, or you can prove

theorem notp {p: Prop} (dne:  p, ¬ ¬ p  p) :  p  ¬ p := sorry

without referencing any classical axioms

But using by_contradiction is the same as using em again which defeats the purpose of the exercise. Or does it :thinking: ?

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 20:54):

Proving that excluded middle implies any of those statements is really easy -- excluded middle just lets you break into cases. But proving that each of those statements implies excluded middle can be challenging

view this post on Zulip Luis Berlioz (Jun 06 2019 at 20:56):

yes, but I don't think I can use by_cases or by_contradiction in this problem

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 20:57):

You're allowed to assume dne in this theorem, so you're allowed to use by_contradiction. You just can't use classical.em

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 20:58):

apply dne, intro h is the same as by_contradiction, in fact the former is a bit better because it doesn't need decidability of the goal

view this post on Zulip Sebastien Gouezel (Jun 06 2019 at 20:58):

in fact the former is a bit better because it doesn't need decidability of the goal

Look at what you've become!

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 20:59):

ha ha, I will get back to glueing sheaves :-/

view this post on Zulip Luis Berlioz (Jun 06 2019 at 21:00):

:smiley: ok, thanks a lot!


Last updated: May 16 2021 at 05:21 UTC