# Zulip Chat Archive

## 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 provetheorem notp {p: Prop} (dne: ∀ p, ¬ ¬ p → p) : p ∨ ¬ p := sorrywithout 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