Is the formula $\neg\neg\forall x (\neg P(x) \,\vee\, \neg\neg P(x))$ provable in intuitionistic logic? I understand that in propositional logic, $\neg\neg Q$ is intuitionistically provable whenever $Q$ is classically provable, but here there is a universal quantifier complicating things.
 A: This is not an intuitionistic tautology.  To see this, consider the Kripke frame where:

*

*$\mathbb{P}$ is the set of functions from a finite subset of $\mathbb{N}$ to $\{ 0, 1 \}$, ordered by inclusion (as subsets of $\mathbb{N} \times \{ 0, 1 \}$; or equivalently, we say $f \le g$ if and only if $\operatorname{dom}(f) \subseteq \operatorname{dom}(g)$ and $g |_{\operatorname{dom}(f)} = f$).

*The universe of discourse is the presheaf $K$ where $K(f) = \mathbb{N}$ for all $f$.

*$P$ is the predicate defined such that $f \Vdash P(n)$ if and only if $(n, 1) \in f$ (or equivalently, $n \in \operatorname{dom}(f)$ and $f(n) = 1$).

Then for this setup, we can verify:

*

*$f \Vdash \lnot P(n)$ if and only if $n \in \operatorname{dom}(f)$ and $f(n) = 0$.

*$f \Vdash \lnot\lnot P(n)$ if and only if $n \in \operatorname{dom}(f)$ and $f(n) = 1$.

*Therefore, $f \Vdash \lnot P(n) \lor \lnot\lnot P(n)$ if and only if $n \in \operatorname{dom}(f)$.

*It follows that for all $f$, $f \not\Vdash \forall n (\lnot P(n) \lor \lnot\lnot P(n))$, since for any $f\in \mathbb{P}$, its domain is not all of $\mathbb{N}$.

*Therefore, for all $f$, $f \Vdash \lnot \forall n (\lnot P(n) \lor \lnot\lnot P(n))$.

*Thus, for example for the empty function $\emptyset$, $\emptyset \not\Vdash \lnot\lnot \forall n (\lnot P(n) \lor \lnot\lnot P(n))$.

This then shows that $\lnot\lnot \forall x (\lnot P(n) \lor \lnot\lnot P(n))$ cannot be provable in intuitionistic logic.
