# All translations of classical logic into intuitionistic logic

What are all possible ways of translating classical logic into intuitionistic logic? That is, if $S$ is the collection of sentences of first order logic, what are all the functions $f : S \to S$ such that $\Gamma \vdash_c \phi$ if and only if $f(\Gamma) \vdash_i f(\phi)$? I know that there is a couple of variants of double negation translation. So, two questions: is there a classification of all possible translations? Are they all logically equivalent to double negation translation?

• You probably want to also demand that $f(\varphi)$ has the same nonlogical symbols as $\varphi$, to avoid silliness like "$f(\varphi)$ applies the double negation translation, but then swaps the unary relation symbols "$U$" and "$V$"." – Noah Schweber Jun 1 '16 at 22:25
• Even telling whether a given function is a translation will be difficult, for several reasons. I doubt there will be a very nice, general classification. – Carl Mummert Jun 1 '16 at 23:18
• @CarlMummert Why is that? And then can we at least give large classes of examples? – fhyve Jun 2 '16 at 3:35
• @fhyve: if $f_0$ is any translation and $\phi$ is any formula, consider $f(\phi) := f_0(\phi)\land \psi$. This is a translation if and only if $\vdash_i \psi$. Now consider $g(\phi)$ defined so that $g(\phi) := f(\phi)$ if there is no proof of $\lnot\text{Con}(ZFC)$ with fewer than $|\phi|$ symbols, and $g(\phi) := (0=1)$ otherwise. Then $g$ is a translation if and only if $\text{Con}(ZFC)$. All the functions I have defined here are primitive recursive. So, unless we find some narrower type of translation that is easier to handle, it will be very hard to characterize translations. – Carl Mummert Jun 2 '16 at 11:59
• To show how much the answer to this question really depends on the exact definition of the class of things that count as 'translations', it is worth recalling that there is a result by Wójcicki according to which the consequence relation of classical logic cannot be faithfully embedded (or 'conservatively translated') by any connective-by-connective (or 'homophonic') translation into that of intuitionistic logic. Here is a paper that can be checked for a stronger version of this result. – J Marcos Jun 2 '16 at 17:44

• While $\phi$ being a classical theorem doesn't imply $\phi$ being an intuitionistic theorem, that doesn't preclude the possibility that there is a way of transforming every classical $\phi$ to some $f(\phi)$ such that if $\phi$ is a classical theorem, then $f(\phi)$ is an intuitionistic theorem. In fact, there are many such $f$, such as the usual double negation translation, which is roughly $f(\phi) = \neg \neg \phi$ (you still need to define how it interacts with operators). – fhyve Jun 5 '16 at 17:58