# Zulip Chat Archive

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