I have a question about Gödel-Gentzen negative translation. According to the Wikipedia article for negative translations, "a sentence $$\phi$$ may not imply its negative translation $$\phi^{\rm N}$$". I am not sure if I understand correctly this sentence. Does it mean that if $$\phi$$ is true in intuitionistic logic, $$\phi^{\rm N}$$ is not necessarily intuitionistically true? If that's the case, could anyone give me an illustrating example?

Thanks!

• The wikipedia page suggests that Troesltra/van Dalen (following Leivant) discuss this - but I don't have access to that book right now. Feb 22 '20 at 21:51
• @NoahSchweber Hi Noah, I have access to that book and actually, I checked that mentioned section, but they didn't explicitly mention that. Feb 22 '20 at 22:01

Does it mean that if $$\varphi$$ is true in intuitionistic logic, $$\varphi^N$$ is not necessarily intuitionistically true?

First, let's get the meaning of "a sentence $$\varphi$$ may not imply its negative translation $$\varphi^N$$" straight.

The raison d'être of the double-negation translation is to realize the proof system for classical logic LK inside the proof system LJ for intuitionistic logic. In that capacity, the double-negation translation is not just a translation of formulas, but a translation of proofs. If there is a derivation with conclusion $$\vdash \varphi$$ in classical logic, then there is a derivation with conclusion $$\vdash \varphi^N$$ in intuitionistic logic, and vice versa. In fact, more is true: a classical derivation of $$\Gamma \vdash \varphi$$ can be translated into an intuitionistic derivation of $$\Gamma^N \vdash \varphi^N$$. Since intuitionistic proofs double as classical proofs, this means that whenever $$\vdash \varphi$$ is provable in intuitionistic logic, then so is $$\vdash \varphi^N$$. So if $$\varphi$$ "is intuitionistically true" (is a tautology of intuitionistic logic), then $$\varphi^N$$ "is intuitionistically true" (is a tautology of intuitionistic logic) as well.

The assertion "a sentence $$\varphi$$ may not imply its negative translation $$\varphi^N$$" has a very different meaning. It means that there might not be an intuitionistic derivation of $$\vdash \varphi \rightarrow \varphi^N$$ (by the previous result this can happen only if $$\varphi$$ is not a tautology).

[...] could anyone give me an illustrating example?

Let's choose a sentence $$\varphi$$ that is not a tautology, say $$(\forall x. P) \rightarrow Q$$ for predicate variables $$P$$ and $$Q$$ (where $$x$$ occurs in $$P$$). According to the Gödel–Gentzen translation given on the Wikipedia page, the translation $$\varphi^N$$ is defined as $$((\forall x. P) \rightarrow Q)^N \equiv (\forall x. P)^N \rightarrow Q^N \equiv (\forall x. P^N) \rightarrow Q^N \equiv (\forall x. \neg\neg P) \rightarrow \neg\neg Q.$$

Clearly $$\vdash ((\forall x.P) \rightarrow Q) \rightarrow (\forall x. \neg\neg P) \rightarrow \neg\neg Q$$ is not derivable in intuitionistic logic. In fact, if you let $$Q_1$$ denote $$\forall y. y = 0 \vee y \neq 0$$ and $$P_1$$ denote $$x = 0 \vee x \neq 0$$, then the real line of Smooth Infinitesmial Analysis satisfies $$\forall x. \neg\neg P_1$$, $$(\forall x. P_1) \rightarrow Q_1$$ and $$\neg Q_1$$.

• Okay! I see the point now. Thank you so much, Z. A. K! Your answer is pretty clear! Feb 23 '20 at 11:46