Stream: Coq users

Topic: double negated LEM

view this post on Zulip 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).
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?

view this post on Zulip 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.

view this post on Zulip Marc Hermes (Jun 08 2021 at 09:00):

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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 08 2021 at 10:19):

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

view this post on Zulip 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!

view this post on Zulip Christian Doczkal (Jun 08 2021 at 10:33):

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

Last updated: Oct 13 2024 at 01:02 UTC