Zulip Chat Archive

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