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.
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)