**The right-to-left direction is not provable in intuitionistic logic**. Coming up with a witness for the existential requires any axiom that moves you to classical logic. For instance, with the principle of excluded middle:

```
Axiom excluded_middle : forall (P : Prop), P \/ ~ P.
Goal forall (X : Type) (p : X -> Prop),
(exists x, ~ p x) <-> ~ (forall x, p x).
Proof.
intros. split.
- intros. destruct H as [x H]. intros nh. apply H. apply (nh x).
- intros Hnfapx.
(* new hyp: Hnfapx : ~ (forall x, p x) *)
pose proof (excluded_middle (exists x, ~ p x)) as [? | Hnexnpx]; [assumption|].
(* new hyp: Hnexnpx : ~ (exists x, ~ p x)
from this (and excluded middle again) we can deduce (forall x, p x)
this contradicts Hnfapx *)
exfalso. apply Hnfapx. intros x.
(* new hyp: x : X
goal: p x *)
pose proof (excluded_middle (p x)) as [? | Hnpx]; [assumption|].
(* new hyp: Hnpx : ~ p x
so there exists x such that ~ p x
this contradicts Hnexnpx *)
exfalso. apply Hnexnpx. exists x. assumption.
Qed.
```

More generally, intuitionistic logic loses (some directions of) the De Morgan laws. Indeed, a De Morgan law expresses a duality between two logical connectives through negation. This is fine in classical logic because double negation cancels out. But that’s not the case in intuitionistic logic: the elimination of double negation (∀ P, ¬¬P → P) is not provable. This principle is, in fact, equivalent to the principle of excluded middle. (However, (∀ P, ¬¬¬P → ¬P) is provable.)

That’s why intuitionistic logic requires both quantifiers ∃ and ∀: none is definable in terms of the other one.

(This was first said as comments; I was expecting someone to come up with a more thorough answer but, since no-one did, I am posting mine now. Thanks @Arthur Azevedo De Amorim for correcting me on which axiom is sufficient.)

`<-`

direction is not provable in intuitionistic logic. Coming up with a witness for the existential requires a variant of the axiom of choice. That’s why intuitionistic logic requires both quantifiers ∃ and ∀: none is definable in terms of the other one.`forall P, P \/ ~ P`

, which is weaker than the axiom of choice.