Coq arrow type in universal hypotesis with existential goal

Question

I have the following theorem to prove:

Goal (exists x, ~P x) <-> ~(forall x, P x).

After a split

unfold not. split.

the first implication is very easy, basically we have to use the x introduced from the forall in the existential quantifier

intros. destruct H. apply H. apply (H0 x).

but on the other side I cannot proceed this way, and I think there should be an idea I cannot find. Any suggestion?

Answer 1

Well, this one is genuinely stuck for good reasons: I believe it is not provable in intuitionistic logic.

The problem, as you figured out, is that to progress by backward reasoning, you need to provide a witness right now, and to progress by forward reasoning, you need to get your hand on an absurd hypothesis. So this goal is stuck.

The problem is that the negation of the universal quantifier does not give you an existential witness of the negated property.

There are many ways to prove it once you introduce classical axioms. Here is a clumsy one with the excluded middle law:

Parameter T : Type.
Parameter P : T -> Prop.

Axiom EM : forall (A : Prop), A \/ ~ A.

Goal (exists x, ~P x) <-> ~(forall x, P x).
Proof.
  split; intro H.
  destruct H as [x H]. intro A. apply H. easy.
  destruct (EM (exists x, ~ P x)) as [?|NE].
  easy.
  elim H. intro x. destruct (EM (P x)) as [Px|NPx].
  easy.
  elim NE. exists x. easy.
Qed.