Glivenko's theorem in predicate logic

Question

Is it possible to extend Glivenko's theorem, which states:

If $\Gamma$ is a set of propositional formulas and $\phi$ is a propositional formula, then $\Gamma$ proves $\phi$ using classical logic if and only if $\Gamma$ proves $\neg \neg \phi$ using intuitionistic logic.

to predicate logic as well?

Answer 1

There is a generalisation to first order logic, the Gödel-Trenzen translation. To a formula $\phi$ in first order language it associates another formula $\phi^N$ as follows:

• If $\phi$ is atomic we let $\phi^N = \neg\neg\phi$,
• If $\phi = \psi \land \chi$, $\phi^N = \psi^N \land \chi^N$
• If $\phi = \psi \lor \chi$, $\phi^N = \neg\neg (\psi^N \lor \chi^N)$
• If $\phi = \psi \to \chi$, $\phi^N = \psi^N \to \chi^N$
• If $\phi = \neg \psi$, $\phi^N = \neg \psi^N$
• If $\phi = \forall x\, \psi$, $\phi^N = \forall x \, \psi^N$,
• If $\phi = \exists x\, \psi$, $\phi^N = \neg\neg \exists x\, \psi^N$

For a set $T\subseteq {\sf Form}$ of formulas, we let $T^N = \{\phi^N \mid \phi \in T\}$, then the following holds analogously to the propositional case:

Fundamental soundness theorem. If $T \subseteq {\sf Form}$ and $\phi \in {\sf Form}$, then $T$ proves $\phi$ in classical logic if and only if $T^N$ proves $\phi^N$ in intuitinonistic logic.