## Stream: new members

### Topic: proving em from dne

#### 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


#### 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

#### 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.

#### 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.

#### 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.

#### 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

#### Kevin Buzzard (Jun 06 2019 at 20:53):

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

#### 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: ?

#### 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

#### 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

#### 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

#### 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

#### 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!

#### Kevin Buzzard (Jun 06 2019 at 20:59):

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

#### Luis Berlioz (Jun 06 2019 at 21:00):

:smiley: ok, thanks a lot!

Last updated: May 16 2021 at 05:21 UTC