Negative translations not intuitionistically equivalent to the usual ones (Q361872)

With the purpose of verifying the folklore conjecture that all negative translations of classical predicate logic into intuitionistic predicate logic are intuitionistically equivalent, the notion of ``negative translation'' is defined as one applying to any translation \((-)^*\) of formulas that satisfies: if \(\Gamma\vdash A\) classically, then \(\Gamma^*\vdash A^*\) intuitionistically (soundness); and, \(\vdash (A^* \leftrightarrow A)\) classically (characterization). Then it is shown that there are (at least) two translations \((-)^{N_1}\) and \((-)^{N_2}\) that satisfy the above definition of negative translation, but are both not intuitionistically equivalent to Gentzen's negative translation \((-)^G\) (Theorem 8). The translation \((-)^{N_1}\) is defined by \[ A^{N_1} := A^G \vee F, \] for \(F\) a chosen formula such that \(\vdash \neg F\) classically, but \(\not\vdash \neg F\) intuitionistically. For the same kind of \(F\), \((-)^{N_2}\) is defined as \[ A^{N_2} := A^G [F/\bot], \] where \(A'[F/\bot]\) denotes the formula obtained by replacing all instances of \(\bot\) in \(A'\) by \(F\). The translation \((-)^{N_2}\) is actually the well-known Dragalin-Friedman translation applied after Gentzen's translation, as shown in Proposition 11. The method for establishing Theorem 8 is to choose as \(F\) one of the two classically (provable and) equivalent versions of Kuroda's conjecture (double negation shift -- DNS), \[ \neg(\neg\forall x P(x) \wedge \forall x \neg\neg P(x)), \] \[ \neg\neg(\forall x\neg\neg P(x) \to \neg\neg\forall x P(x)), \] with one prefixing ``\(\neg\)'' removed. The theorem then follows from the well-known fact that DNS is intuitionistically not provable. In conclusion we can infer that the defined notion of ``negative translation'' is too permissive if one wants to keep thinking of all negative translations as being intuitionistically equivalent. Besides the main result outlined above, the paper may also be of interest to researchers studying negative translations because of the elementary and detailed exposition.