Universal Quantifier in Intuitionistic Logic

Question

I have a very basic question about $\forall$ in intuitionistic first-order logic (IQL). It is well-known that in intuitionistic propositional logic (IPL), (\ref{dnlem}) and (\ref{dndne}) are both valid. \begin{equation} \neg\neg(A\vee\neg A)\tag{LEM$_{\neg\neg}$}\label{dnlem} \end{equation} \begin{equation} \neg\neg(\neg\neg A\rightarrow A)\tag{DNE$_{\neg\neg}$}\label{dndne} \end{equation} My question is, are (\ref{dnlem}) and (\ref{dndne}) also valid for $\forall$? That is, shall we prove the following propositions? $$\neg\neg(\forall xA(x)\vee\neg\forall xA(x)),\quad\quad\quad\neg\neg(\neg\neg\forall xA(x)\rightarrow\forall xA(x))$$ Thanks!

Answer 1

To take the first case, the same intuitionistic proof of e.g. $\neg\neg(\phi \lor \neg\phi)$ goes through whether $\phi$ is a propositional wff or involves quantifiers.

In the obvious way, just using uncontentious rules for the connectives, we show that the supposition $\neg(\phi \lor \neg\phi)$ entails a contradiction, and hence can infer its negation $\neg\neg(\phi \lor \neg\phi)$. Nothing here depends on what is 'inside' the wff we substitute for $\phi$.

So in particular, we can derive $\neg\neg(\forall xA(x)\vee\neg\forall xA(x))$ just using the rules for $\neg$ and $\lor$.

Similarly, just the inituitionistically acceptable connective rules suffice to show $\neg\neg(\neg\neg\phi \to \phi)$, whether or not $\phi$ contains quantifiers.