First-order intuitionistic logic question

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$?

Answer 1

$$ \neg \neg \forall x(p(x)\lor \neg 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 \neg p(n)$ is false in $w_{n-1}$, and therefore $\forall x(p(x)\lor \neg p(x))$ is false everywhen, so its double negation is equally false.