 Nelson’s Theorem establishes the unprovability in \(\mathbf{IQC}\) of some theorems of classical predicate logic. If, to each \(n\)-place predicate letter \(P(\ldots ),\) a formula \(f(P)\) of \(L(\mathbf{HA})\) with \(n\) free variables is assigned, and if the formula \(f(A)\) of \(L(\mathbf{HA})\) comes from the formula \(A\) of \(L\) by replacing each prime formula \(P(x_1, \ldots, x_n)\) by \(f(P)(x_1 ,\ldots ,x_n),\) then \(f(A)\) is called an arithmetical substitution instance of \(A.\) As an example, if a formula of \(L(\mathbf{HA})\) expressing “\(y\) is the code of a sentence and \(x\) codes a proof in \(\mathbf{HA}\) of the sentence with code \(y\)” is assigned to \(P(x,y),\) then (assuming \(\mathbf{HA}\) is consistent) the resulting arithmetical substitution instance of \(\forall y (\exists x P(x, y) \vee \neg \exists x P(x, y))\) is unrealizable and hence unprovable in \(\mathbf{HA},\) and so is its double negation. It follows that \(\neg \neg \forall y (\exists x P(x, y) \vee \neg \exists x P(x, y))\) is not provable in \(\mathbf{IQC}.\)