## Stream: new members

### Topic: dne implies em

#### Luis O'Shea (Oct 20 2019 at 23:20):

TPiL 3.5 suggests proving em (excluded middle) using dne (double-negation elimination). I found this trickier than expected (as a Lean noob) and was wondering what tricks I'm missing. Below is my attempt. Some concrete questions include: Did I really need to define demorgan_nor? Do I need to use the inference symbol (_) so much? Is my attempt too long?

variables p q : Prop

lemma demorgan_nor (h : ¬(p ∨ q)) : ¬p ∧ ¬q :=
⟨ assume : p, h $or.inl this, assume : q, h$ or.inr this ⟩

section
open classical

theorem dne (h : ¬¬p) : p :=
or.elim (em p)
(assume : p, this)
(assume : ¬p, absurd this h)

end

lemma nnem : ¬¬(p ∨ ¬p) :=
assume h : ¬(p ∨ ¬p),
have hpnp : ¬p ∧ ¬¬p, from demorgan_nor _ _ h,
have hnpp : ¬p ∧ p, from and.intro hpnp.left (dne _ hpnp.right),
hnpp.left hnpp.right

theorem em_alt : p ∨ ¬p := dne _ $nnem _  #### Kenny Lau (Oct 20 2019 at 23:34): you shouldn't use classical because that is the point, I think. #### Kenny Lau (Oct 20 2019 at 23:35): you don't need _ if you make the variables implicit #### Luis O'Shea (Oct 20 2019 at 23:35): you shouldn't use classical because that is the point, I think. I only used classical to prove dne #### Mario Carneiro (Oct 20 2019 at 23:36): you should be able to prove nnem without dne or any classical stuff #### Kenny Lau (Oct 20 2019 at 23:38): Spoilers: . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . axiom dne {p : Prop} : ¬¬p → p theorem em {p : Prop} : p ∨ ¬p := dne$ assume h : ¬(p ∨ ¬p),
have hnp : ¬p, from assume hp : p, h $or.inl hp, h$ or.inr hnp


#### Luis O'Shea (Oct 20 2019 at 23:39):

you should be able to prove nnem without dne or any classical stuff

Duh! Yes:

lemma nnem : ¬¬(p ∨ ¬p) :=
assume h : ¬(p ∨ ¬p),
have hpnp : ¬p ∧ ¬¬p, from demorgan_nor _ _ h,
hpnp.right hpnp.left


#### Kenny Lau (Oct 20 2019 at 23:39):

Golfed version:
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

axiom dne {p : Prop} : ¬¬p → p

theorem em {p : Prop} : p ∨ ¬p :=
dne $λ h, h$ or.inr $λ hp, h$ or.inl hp


#### Luis O'Shea (Oct 20 2019 at 23:46):

Thanks! So regarding avoiding _s, is it generally preferable to write variable {p : Prop} rather than variable p : Prop? (Or if not when is one preferred over the other?)

#### Mario Carneiro (Oct 20 2019 at 23:49):

The braces mean "let lean figure it out", i.e. always put a _ in that slot. The convention is to make the variable implicit if it can be deduced from the type of later assumptions (not counting the conclusion). So that means dne should have p implicit but em should have it explicit

Last updated: May 17 2021 at 22:15 UTC