Is the formula $\neg\neg\forall x (\neg P(x) \,\vee\, \neg\neg P(x))$ provable in intuitionistic logic?

Question

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.

Answer 1

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.