8
$\begingroup$

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!

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

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

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Okay! I see the point now. Thank you so much, Z. A. K! Your answer is pretty clear! $\endgroup$ – ferdinand Feb 23 at 11:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.