Is $\lnot\lnot\forall x(A(x)\vee\neg A(x))$ a theorem of intuitionistic logic?

Question

I have a short question. I know that $\neg\neg(A\vee\neg A)$ is a theorem of intuitionistic logic. What about $\neg\neg\forall x(A(x)\vee\neg A(x))$?

Answer 1

No, it is not. To prove this, we can give a countermodel (I'll use Kripke semantics).

For a world $v$ in a Kripke model $M$, the meaning of $M,v\Vdash\lnot\lnot\forall x(A(x)\lor \lnot A(x))$ is: for all worlds $v'\geq v$, there exists a world $v''\geq v'$ such that for all worlds $w\geq v''$ and all $x\in M_{w}$, $A(x)$ holds at $w$ or for all worlds $w'\geq w$, $A(x)$ does not hold at $w'$.

In other words, there is a dense set above $v$ of worlds $v''$ with the property that the truth value of $A(x)$ does not ever "flip" for any element of any world above $v''$.

For our countermodel, take the frame to be $\mathbb{N}$ with its usual order, $M_n = \{0,\dots , n\}$, and interpret $A$ in $M_n$ as $M_n\setminus\{n\}$. Then $M,0\not\Vdash\lnot\lnot\forall x(A(x)\lor \lnot A(x))$, since for any world $n$, the truth value of $A(n)$ "flips" when moving from $n$ to $n+1$.

Answer 2

No, it is not. If it were, then using the internal language of a topos, the interpretation of the formula $\lnot\lnot \forall p : \Omega, p \lor \lnot p$ would be $\mathrm{true}$ on any topos.

However, consider the topos of sheaves of sets on $\mathbb{R}$. In this topos, for each $x \in \mathbb{R}$, we have a global section of $\Omega$ corresponding to the open subset $\mathbb{R} \setminus \{ x \} \subseteq \mathbb{R}$. For this section $p$, we get $\lnot p = \emptyset$, so $p \lor \lnot p = \mathbb{R} \setminus \{ x \}$. Taking the intersection over all $x$, we see that $\forall p : \Omega, p \lor \lnot p$ must evaluate to $\emptyset$, and so $\lnot\lnot \forall p : \Omega, p \vee \lnot p$ also evaluates to $\emptyset$ instead of to $\mathrm{true} = \mathbb{R}$.

(Actually, in this argument, there is nothing all that special about the topological space $\mathbb{R}$ that we used. Pretty much the same argument would work on any $T_1$ topological space with no isolated points.)