About Gödel-Gentzen negative translation

Solution 1:

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$.