First-order intuitionistic logic question I know that if $A$ is a theorem of classical propositional logic, then $\neg \neg A$ is a theorem of intuitionistic propositional logic. I read in a previous question I asked ...--prophetes.ai

First-order intuitionistic logic question I know that if $A$ is a theorem of classical propositional logic, then $\neg \neg A$ is a theorem of intuitionistic propositional logic. I read in a previous question I asked long ago, that the corresponding statement for first order logic is false. Can someone give an explicit counterexample $A$?

$$ \
eg \
eg \forall x(p(x)\lor \
eg p(x)) $$ is not a theorem of pure intuitionistic first-order logic.

Namely, it is false in the Kripke model with a countable infinity of worlds $$ w_0 \le w_1 \le w_2 \le \cdots \le w_n \le \cdots $$ where the individuals in each world are $\\{1,2,3,\ldots\\}$, and $p(n)$ is true from world $w_n$ onwards.

Then $p(n)\lor \
eg p(n)$ is _false_ in $w_{n-1}$, and therefore $\forall x(p(x)\lor \
eg p(x))$ is _false everywhen_ , so its double negation is equally false.