[proofplan]
We construct a constant-domain Kripke model with two nodes $r \leq t$ and one individual $a$. The predicate $P(a)$ is forced at the later node $t$ but not at the root $r$. This makes $\exists x\,P(x)$ fail at $r$, while $\neg\neg\exists x\,P(x)$ holds at $r$ because every extension of $r$ has an extension forcing the existential. By soundness of intuitionistic predicate logic for Kripke models, a formula that fails in a Kripke model cannot be intuitionistically derivable.
[/proofplan]
[step:Build a constant-domain Kripke model with one delayed witness]
Let $L$ be the first-order language containing one unary predicate symbol $P$. Define a Kripke frame $(W,\leq)$ by
\begin{align*}
W := \{r,t\},
\end{align*}
with ordering relation determined by $r \leq r$, $t \leq t$, and $r \leq t$.
Let the constant domain be the nonempty set
\begin{align*}
D := \{a\}.
\end{align*}
Define the atomic forcing relation $\Vdash$ for formulas of the form $P(b)$, with $b \in D$, by requiring
\begin{align*}
t \Vdash P(a),
\end{align*}
and by requiring that $r$ force no atomic formula $P(b)$ with $b \in D$. This valuation is monotone: if a node $w \in W$ forces $P(b)$ and $w \leq v$, then $v$ also forces $P(b)$, because the only nontrivial forced atomic formula is already forced at the maximal node $t$.
[guided]
We need a Kripke model in which an existential statement is not forced at the root, but cannot be refuted at the root. The smallest possible model has two nodes. Let $W := \{r,t\}$, where $r$ is the root and $t$ is a later node. The order relation is $r \leq r$, $t \leq t$, and $r \leq t$.
The domain must be nonempty, because the existential quantifier ranges over individuals. We take the constant domain
\begin{align*}
D := \{a\}.
\end{align*}
The word "constant" means that the same set $D$ is used at both nodes $r$ and $t$.
Now define the atomic forcing relation. We want the witness $a$ to become available only later, so we stipulate
\begin{align*}
t \Vdash P(a),
\end{align*}
and stipulate that $r$ forces no atomic formula $P(b)$ with $b \in D$. Since $D=\{a\}$, this says precisely that $r \nVdash P(a)$.
Kripke valuations for intuitionistic logic must be persistent: once an atomic formula is forced, it remains forced at all later nodes. This condition holds here. The only forced atomic formula is $P(a)$ at $t$, and $t$ has no proper later node. Hence there is no violation of persistence.
[/guided]
[/step]
[step:Show that the existential conclusion is not forced at the root]
In constant-domain Kripke semantics, a node $w \in W$ forces $\exists x\,P(x)$ exactly when there exists $b \in D$ such that $w \Vdash P(b)$. Since $D=\{a\}$ and $r \nVdash P(a)$, there is no $b \in D$ such that $r \Vdash P(b)$. Therefore
\begin{align*}
r \nVdash \exists x\,P(x).
\end{align*}
[/step]
[step:Show that the double negation antecedent is forced at the root]
We prove that
\begin{align*}
r \Vdash \neg\neg\exists x\,P(x).
\end{align*}
By the Kripke clause for negation, this means that for every node $s \in W$ with $r \leq s$, the node $s$ does not force $\neg\exists x\,P(x)$.
Let $s \in W$ satisfy $r \leq s$. If $s=r$, then $t \geq r$ and $t \Vdash P(a)$, so $t \Vdash \exists x\,P(x)$ by the existential forcing clause. Hence $r$ cannot force $\neg\exists x\,P(x)$.
If $s=t$, then $t \Vdash P(a)$, so again $t \Vdash \exists x\,P(x)$. Since $t \geq t$, the node $t$ cannot force $\neg\exists x\,P(x)$.
Thus no extension $s$ of $r$ forces $\neg\exists x\,P(x)$, and therefore
\begin{align*}
r \Vdash \neg\neg\exists x\,P(x).
\end{align*}
[guided]
The negation clause in Kripke semantics is the key point. A node $w$ forces $\neg A$ exactly when no later node $v \geq w$ forces $A$. Therefore $r$ forces $\neg\neg A$ exactly when every later node $s \geq r$ fails to force $\neg A$.
Here $A$ is the formula $\exists x\,P(x)$. We must check both extensions of $r$, namely $r$ itself and $t$.
First take $s=r$. To show that $r$ does not force $\neg\exists x\,P(x)$, it is enough to find some later node $v \geq r$ that forces $\exists x\,P(x)$. We can take $v=t$. Since $t \Vdash P(a)$ and $a \in D$, the existential forcing clause gives
\begin{align*}
t \Vdash \exists x\,P(x).
\end{align*}
Therefore $r \nVdash \neg\exists x\,P(x)$.
Now take $s=t$. Since $t \Vdash P(a)$ and $a \in D$, the same existential forcing clause gives
\begin{align*}
t \Vdash \exists x\,P(x).
\end{align*}
Because $t \geq t$, the node $t$ has a later node, namely itself, forcing $\exists x\,P(x)$. Hence $t \nVdash \neg\exists x\,P(x)$.
We have shown that every node $s \geq r$ fails to force $\neg\exists x\,P(x)$. By the negation clause applied once more,
\begin{align*}
r \Vdash \neg\neg\exists x\,P(x).
\end{align*}
[/guided]
[/step]
[step:Conclude that the schema is not intuitionistically derivable]
At the root $r$ of the constructed Kripke model, we have
\begin{align*}
r \Vdash \neg\neg\exists x\,P(x)
\end{align*}
and
\begin{align*}
r \nVdash \exists x\,P(x).
\end{align*}
By the Kripke forcing clause for implication, the formula
\begin{align*}
\neg\neg\exists x\,P(x) \to \exists x\,P(x)
\end{align*}
is therefore not forced at $r$.
Soundness of intuitionistic predicate logic for Kripke models says that every intuitionistically derivable formula is forced at every node of every Kripke model in which its nonlogical symbols are interpreted monotonically. The constructed model is such a model, and the displayed formula fails at $r$. Hence the schema is not derivable in first-order intuitionistic predicate logic. This invokes a result not yet resolved to a wiki theorem link: Soundness of intuitionistic logic for Kripke models.
[/step]
