Proving EM from DNE

Stream: new members

[Daniel James]

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]

Yes, that is possible and you started the proof correctly

[Mario Carneiro]

The hint is to try proving ¬q

[Daniel James]

Ah good to know it is possible!

[Daniel James]

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.

[Mario Carneiro]

oh but is it?

[Mario Carneiro]

try proving the ¬q case

[Daniel James]

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

[Daniel James]

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

[Daniel James]

Ah! I got it!!

[Daniel James]

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

[Mario Carneiro]

what message?

[Daniel James]

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

[Kevin Buzzard]

Use tactic mode

[Daniel James]

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

[Daniel James]

So I am trying to do it without them

[Daniel James]

even if it is significantly more tedious

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Books don't always do it the easiest way

[Daniel James]

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]

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]

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]

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]

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]

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]

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]

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

[Daniel James]

right

[Mario Carneiro]

that's not a proof of q ∨ ¬q

[Mario Carneiro]

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

[Mario Carneiro]

you need to apply it to h2 that you just introduced

[Mario Carneiro]

adding more show will also help localize the errors

[Daniel James]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Daniel James]

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