## Stream: Coq users

### Topic: double negated LEM

#### Marc Hermes (Jun 07 2021 at 21:22):

First, for some context: There was an exercise for students where they were supposed to show

``````Definition LEM := forall X, X \/ ~X.

Lemma nexn_iff_nnall X (p : X -> Prop) : LEM ->
(~ exists x, ~ p x) <-> ~~(forall x, p x).
``````

After playing with it a little bit I noticed that:

``````Definition LEM := forall X, X \/ ~X.

Lemma nexn_iff_nnall : ~~LEM <->
(forall X (p : X -> Prop), (~~forall x, p x) <-> (~ exists x, ~ p x)).
Proof.
split.
- intros H X p. split.
+ firstorder.
+ intros nE nF.
apply H. intros lem.
apply nF. intros x.
destruct (lem (p x)); [tauto|].
exfalso. apply nE.
now exists x.
- intros H.
specialize (H Prop (fun X => X \/ ~X)).
apply H. intros []. tauto.
Qed.
``````

But I have no clue what to make of `~~LEM`. I have not come across anything related to it yet. Any thoughts / interesting pointers that come to mind?

#### Cody Roux (Jun 08 2021 at 01:11):

one nice intuition is that the De Morgan laws, which swap `/\` and `\/` under negation, work in one direction intuitionistically.

#### Marc Hermes (Jun 08 2021 at 09:00):

@Cody Roux I don't see what the connection to `~~LEM` is

#### Christian Doczkal (Jun 08 2021 at 09:51):

One thing to note here is that there are many statements that are not provable in intuitionistic logic but that are strictly weaker than `LEM`. Also note that one can make arbitrary case distinctions whenever one is proving `False` (or a negation), since the following is easily provable.

``````Lemma EMF (Q : Prop) : ((Q \/ ~Q) -> False) -> False.
``````

Similarly, one can strip double negations from assumptions as you have done. One possible pointer is "intermediate logics". However, they usually talk about axiom schemes one adds to intuitionsitic propositional logic, and `~~LEM` doesn't quite fit this schema due to the top-level negation.

#### Marc Hermes (Jun 08 2021 at 10:33):

@Pierre-Marie Pédrot Ah yes! This is the kind of pointer I was hoping for. Thanks!

#### Christian Doczkal (Jun 08 2021 at 10:33):

Yes, indeed, that's a much better pointer. Thanks @Pierre-Marie Pédrot.

Last updated: Jan 31 2023 at 14:03 UTC