## Stream: new members

### Topic: Proving EM from DNE

#### Daniel James (Apr 07 2023 at 02:59):

I've been reading Theorem Proving in Lean and in section 3.5 it mentions proving the law of the excluded middle from the double negative elimination principle.

I started with this:

variable p : Prop
example : (¬¬p→ p) ↔ p ∨ ¬p := sorry


but was only able to prove EM -> DNE and not the other way around.
I did some research and this seems to say its not possible with this formulation so I tried changing it to this:

example : (∀ q, ¬¬q → q) ↔ (∀ p, p ∨ ¬p) := sorry


With this I have only managed to get this far. Is this possible? Does anyone have any hints? Thanks!

example : (∀ q, ¬¬q → q) ↔ (∀ p, p ∨ ¬p) :=
iff.intro
(assume h,
assume q,
suffices h₂ : ¬¬(q ∨ ¬q), from h (q ∨ ¬q),
assume h₂,
sorry)
(assume h,
assume q,
assume hnnq,
or.elim (h q)
(assume hq, hq)
(assume hnq, absurd hnq hnnq))


#### Mario Carneiro (Apr 07 2023 at 03:05):

Yes, that is possible and you started the proof correctly

#### Mario Carneiro (Apr 07 2023 at 03:05):

The hint is to try proving ¬q

#### Daniel James (Apr 07 2023 at 03:08):

Ah good to know it is possible!

#### Daniel James (Apr 07 2023 at 03:11):

It just seems like the only thing I can do from here is suffices h₃ : q ∨ ¬q, from h₂ h₃, which is just back to square one.

oh but is it?

#### Mario Carneiro (Apr 07 2023 at 03:12):

try proving the ¬q case

#### Daniel James (Apr 07 2023 at 03:12):

well we do have an extra hypothesis which is helpful (?)

#### Daniel James (Apr 07 2023 at 03:12):

Alright starting from here

example : (∀ q, ¬¬q → q) ↔ (∀ p, p ∨ ¬p) :=
iff.intro
(assume h,
assume q,
suffices h₂ : ¬¬(q ∨ ¬q), from h (q ∨ ¬q),
assume h₂,
suffices h₃ : q ∨ ¬q, from h₂ h₃,
or.inr
(_))
(assume h,
assume q,
assume hnnq,
or.elim (h q)
(assume hq, hq)
(assume hnq, absurd hnq hnnq))


Ah! I got it!!

#### Daniel James (Apr 07 2023 at 03:14):

Ok I think this should be it

example : (∀ q, ¬¬q → q) ↔ (∀ p, p ∨ ¬p) :=
iff.intro
(assume h,
assume q,
suffices h₂ : ¬¬(q ∨ ¬q), from h (q ∨ ¬q),
assume h₂,
suffices h₃ : q ∨ ¬q, from h₂ h₃,
or.inr
(assume hq,
suffices h₃ : q ∨ ¬q, from h₂ h₃,
or.inl hq))
(assume h,
assume q,
assume hnnq,
or.elim (h q)
(assume hq, hq)
(assume hnq, absurd hnq hnnq))


But I'm getting an error message on the iff

what message?

#### Daniel James (Apr 07 2023 at 03:15):

alot

type mismatch at application
iff.intro
(λ (h : ∀ (q : Prop), ¬¬q → q) (q : Prop),
(λ (h₂ : ¬¬(q ∨ ¬q)), h (q ∨ ¬q))
(λ (h₂ : ¬(q ∨ ¬q)),
(λ (h₃ : q ∨ ¬q), h₂ h₃) (or.inr (λ (hq : q), (λ (h₃ : q ∨ ¬q), h₂ h₃) (or.inl hq)))))
term
λ (h : ∀ (q : Prop), ¬¬q → q) (q : Prop),
(λ (h₂ : ¬¬(q ∨ ¬q)), h (q ∨ ¬q))
(λ (h₂ : ¬(q ∨ ¬q)),
(λ (h₃ : q ∨ ¬q), h₂ h₃) (or.inr (λ (hq : q), (λ (h₃ : q ∨ ¬q), h₂ h₃) (or.inl hq))))
has type
(∀ (q : Prop), ¬¬q → q) → ∀ (q : Prop), ¬¬(q ∨ ¬q) → q ∨ ¬q
but is expected to have type
(∀ (q : Prop), ¬¬q → q) → ∀ (p : Prop), p ∨ ¬p


Use tactic mode

#### Daniel James (Apr 07 2023 at 03:21):

I'm in the part of the book that hasn't introduced tactics yet.

#### Daniel James (Apr 07 2023 at 03:21):

So I am trying to do it without them

#### Daniel James (Apr 07 2023 at 03:21):

even if it is significantly more tedious

#### Kevin Buzzard (Apr 07 2023 at 03:22):

And far more prone to errors of the form you just posted

#### Kevin Buzzard (Apr 07 2023 at 03:22):

I always tell my students not to believe what they read in books

#### Kevin Buzzard (Apr 07 2023 at 03:22):

Books don't always do it the easiest way

#### Daniel James (Apr 07 2023 at 03:23):

The suffices seems to be breaking it. This has a similar error.

example : (∀ q, ¬¬q → q) ↔ (∀ p, p ∨ ¬p) :=
iff.intro
(assume h,
assume q,
suffices h₂ : ¬¬(q ∨ ¬q), from h (q ∨ ¬q),
sorry)
(assume h,
assume q,
assume hnnq,
or.elim (h q)
(assume hq, hq)
(assume hnq, absurd hnq hnnq))


#### Kevin Buzzard (Apr 07 2023 at 03:23):

Doing it not in tactic mode won't teach you anything other than the fact that it's a pain not doing it in tactic mode

#### Daniel James (Apr 07 2023 at 03:25):

idk. I feel like after doing these excercises without tactic mode I understand the type system much better. And this is the last one in the chapter.

#### Kevin Buzzard (Apr 07 2023 at 03:26):

I guess you should take my comments with a pinch of salt then because I have no desire to understand the type system, I just want to prove theorems

#### Mario Carneiro (Apr 07 2023 at 03:31):

A strategy to get more localized errors is to replace individual subterms with _, and try to ensure that there are no errors other than on _

#### Daniel James (Apr 07 2023 at 03:31):

Oh I know what's going on. You can't just pull q ∨ ¬q out of nowhere. That's the thing we are trying to prove.

#### Daniel James (Apr 07 2023 at 03:32):

Yup

example : (∀ q, ¬¬q → q) ↔ (∀ p, p ∨ ¬p) :=
iff.intro
(assume h,
assume p,
suffices h₂ : ¬¬(q ∨ ¬q), from sorry,
assume h₂ : ¬(q ∨ ¬q),
suffices h₃ : q ∨ ¬q, from h₂ h₃,
or.inr
(assume hq,
suffices h₃ : q ∨ ¬q, from h₂ h₃,
or.inl hq))
(assume h,
assume q,
assume hnnq,
or.elim (h q)
(assume hq, hq)
(assume hnq, absurd hnq hnnq))


This works

#### Mario Carneiro (Apr 07 2023 at 03:32):

I think the issue is the subterm h (q ∨ ¬q)

right

#### Mario Carneiro (Apr 07 2023 at 03:32):

that's not a proof of q ∨ ¬q

#### Mario Carneiro (Apr 07 2023 at 03:33):

it is a proof of ¬¬(q ∨ ¬q) -> q ∨ ¬q

#### Mario Carneiro (Apr 07 2023 at 03:33):

you need to apply it to h2 that you just introduced

#### Mario Carneiro (Apr 07 2023 at 03:35):

adding more show will also help localize the errors

#### Daniel James (Apr 07 2023 at 03:35):

Hmm. Very close

type mismatch at application
h h₂
term
h₂
has type
¬¬(q ∨ ¬q) : Prop
but is expected to have type
Prop : Type


#### Daniel James (Apr 07 2023 at 03:37):

So if I understand correctly this means that h₂ is a proof of ¬¬(q ∨ ¬q) not the statement itself.

#### Mario Carneiro (Apr 07 2023 at 03:48):

yes, h takes two arguments, a proposition and then a proof of its double negation

#### Mario Carneiro (Apr 07 2023 at 03:48):

the former can be inferred from the latter so h _ h₂ should suffice

#### Daniel James (Apr 07 2023 at 03:49):

Ah! That fixed it! Thank you very much for your help

Last updated: Dec 20 2023 at 11:08 UTC