[SOLVED] The missing De Morgan's law

The missing De Morgan's law

Coq uses constructive logic, which means that if you try to fill out De Morgan's laws, you'll end up missing 2. Namely, you can't prove:

Theorem deMorgan_nand P Q (andPQ : ~(P /\ Q)) : P \/ Q.
Abort.

Theorem deMorgan_nall {A} (P : A -> Prop) (allPa : ~forall a, P a) : exists a, ~P a.
Abort.

This makes sense, because you've have to compute whether it was the left or right item of the or, which you can't do in general.

Looking at "Classical Mathematics for a Constructive World" (https://arxiv.org/pdf/1008.1213.pdf) has the definitions

Definition orW P Q := ~(~P /\ ~Q).
Definition exW {A} (P : A -> Prop) := ~forall a, ~P a.

similar to De Morgan's law. This suggests an alternative formulation.

Theorem deMorgan_nand P Q (andPQ : ~(P /\ Q)) : orW (~P) (~Q).
  hnf; intros nnPQ; destruct nnPQ as [ nnP nnQ ].
  apply nnP; clear nnP; hnf; intros p.
  apply nnQ; clear nnQ; hnf; intros q.
  apply (andPQ (conj p q)).  
Qed.

Theorem deMorgan_nall {A} (P : A -> Prop) (allPa : ~forall a, P a) : exW (fun a => ~P a).
Abort.

But, it doesn't work with negating forall. In particular, it gets stuck on trying to convert ~~P a into P a. So, despite in the nand case converting ~~P into P, it doesn't seem to work with forall. You can also show that there is some element of a that has P a.

Similarly, you could try to show

Theorem deMorgan_nexn {A} (P : A -> Prop) (exPa : ~exists a, ~P a) : ~~forall a, P a.
Abort.

but that gets stuck in that once you have the argument a, the conclusion is no longer False, so you can't use ~~P -> P.

So, if you can't prove deMorgan_nall, is there any theorem like it? Or is ~forall a, P a already as simplified as it can get? More generally, when the conclusion is False, that allows for using the law of excluded middle (P \/ ~P). Is there any counterpart to that that works when the proposition takes an argument, that is P : A -> Prop instead of P : Prop ?

Solution

The principle you are looking for is known as double negation shift. It is not valid in intuitionistic logic in general. Despite looking fairly innocuous at first, as its conclusion is a doubly-negated formula, it is actually quite potent. Indeed, DNS is essentially what is needed in order to interpret the axiom of choice through the double-negation translation.

Edit by scubed:

So, that means I have to add an axiom to handle this case. Using the axiom,

Axiom deMorgan_allnn : forall {A} (P : A -> Prop) (allPa : forall a, ~~P a), ~~forall a, P a.

Theorem deMorgan_nall {A} (P : A -> Prop) (allPa : ~forall a, P a) : exW (fun a => ~P a).
  hnf; intros ex1; apply deMorgan_allnn in ex1.
  apply ex1; clear ex1; hnf; intros all2.
  apply (allPa all2).
Qed.