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).
Proof. Admitted.
```

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?

one nice intuition is that the De Morgan laws, which swap `/\`

and `\/`

under negation, work in *one* direction intuitionistically.

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

is

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.

see also https://ncatlab.org/nlab/show/double-negation+shift

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

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

Last updated: Jun 15 2024 at 08:01 UTC