Counterexample to Glivenko's theorem in predicate logic

Question

I read everywhere that Glivenko's double negation translation does not generalise to predicate logic. In other words, this means that for some predicate formula $\phi$ we have $\vdash\phi$ classically while $\not\vdash\lnot\lnot\phi$ intuitionistically. Most literature I find skips this point and continues showing that the Gödel-Gentzen translation does work in intuitionistic predicate logic.

Could anyone give an example of such a $\phi$ that is classically valid while $\lnot\lnot\phi$ is not provable intuitionistically?

Answer 1

See Dirk van Dalen, Logic and Structure, Springer (5th ed - 2013), page 161.

Gödel's transaltion has (for the non-trivial cases) :

$\varphi^G := \lnot \lnot \varphi$, for $\varphi$ atomic

$(\varphi \lor \psi)^G := \lnot (\lnot \varphi^G \land \lnot \psi^G)$

$(\exists x \ \varphi(x))^G := \lnot \forall x \lnot \ \varphi^G(x)$.

The relation between classical derivability $(\vdash_C$) and intuitionistic derivability ($\vdash_I$) is:

$\Gamma \vdash_c \varphi \ $ iff $ \ \Gamma^G \vdash_I \varphi^G$.

We have to note the special role of $∨$ and $∃$ in intuitionistic logic. This is underlined by the following result.

A formula $\varphi$ is called negative if atoms occur only negated, and it does not contain $\lor$ or $\exists$. In this case we have:

$\vdash_C \varphi$ iff $\vdash_I \varphi$, for negative $\varphi$.

For propositional logic we have a "stronger" result:

Glivenko’s Theorem: $\vdash_C \varphi$ iff $\vdash_I ¬¬ \varphi$.

An example of "double negation" formula that is not derivable in intuitionistic logic is:

$\lnot \lnot \forall x \ (A(x) \lor \lnot A(x))$.

See Jan von Plato, Elements of Logical Reasoning, Cambridge UP (2013), page 142, for the proof on its unprovability in intuitionistic predicate calculus.