Is this relationship between forall and exists provable in Coq/intuitionistic logic?

Question

Is the following theorem provable in Coq? And if not, is there a way to prove it isn't provable?

Theorem not_for_all_is_exists:
    forall (X : Set) (P : X -> Prop), ~(forall x : X, ~ P x) -> (exists x: X, P x).

I know this related relationship is true:

Theorem forall_is_not_exists : (forall (X : Set) (P : X -> Prop), (forall x, ~(P x)) -> ~(exists x, P x)).
Proof.
  (* This could probably be shortened, but I'm just starting out. *)
  intros X P.
  intros forall_x_not_Px.
  unfold not.
  intros exists_x_Px.
  destruct exists_x_Px as [ witness proof_of_Pwitness].
  pose (not_Pwitness := forall_x_not_Px witness).
  unfold not in not_Pwitness.
  pose (proof_of_False := not_Pwitness proof_of_Pwitness).
  case proof_of_False.
Qed.

But I'm not sure that helps me without double negative elimination. I've also played around with proving the theorem in question, with different approaches, to no avail. I'm just learning Coq, so it could be I'm just missing something obvious, however.

N.B. I'm well aware that this is true in classical logic, so I'm not looking for a proof that adds additional axioms to the underlying system.

Answer 1

It's not provable, because it's equivalent to double negation elimination (and the other classical axioms).

My Coq skills are very rusty currently, but I can quickly illustrate why your theorem implies double negation elimination.

In your theorem, instantiate X to unit and P to fun _ => X for an arbitrary X : Prop. Now we have ~(unit -> ~ X) -> exists (u : unit), X. But because of the triviality of unit this is equivalent to ~ ~ X -> X.

The backwards implication can be proved with a straightforward application of double negation elimination on ~ ~ (exists x, P x).

My Agda is much better, so I can at least show the proofs there (don't know if that's helpful, but it might back up my claims a bit):

open import Relation.Nullary
open import Data.Product
open import Data.Unit
open import Data.Empty
open import Function

∀∃ : Set _
∀∃ = (A : Set)(P : A → Set) → ¬ (∀ x → ¬ P x) → ∃ P

Dneg : Set _
Dneg = (A : Set) → ¬ ¬ A → A

to : ∀∃ → Dneg
to ∀∃ A ¬¬A = proj₂ (∀∃ ⊤ (const A) (λ f → ¬¬A (f tt)))

fro : Dneg → ∀∃
fro dneg A P f = dneg (∃ P) (f ∘ curry)

Answer 2

Your not_for_all_is_exists proposition is not provable in Coq. I recommend reading the beginning of Dirk Van Dalen's "Logic and Structure" Chapter 5. for a more in-depth explanation.

In intuitionistic logic (and systems such a Coq), to prove exists x, P x you have to provide a method (or algorithm) that will construct the actual x such that P x holds.

Assuming not (forall x, not (P x)) has roughly the interpretation "if I assume that P doesn't hold for all x, then I get a contradiction", but this is weaker than your desired conclusion, building a model will reveal that the assumption does not contain enough information to pick the a witness for P.

However, it must be said that this principle holds in Coq for restricted classes of P and X, a particular example is when P is a decidable predicate and X a finite type.