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?

  • $\begingroup$ 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$"." $\endgroup$ – Noah Schweber Jun 1 '16 at 22:25
  • $\begingroup$ 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. $\endgroup$ – Carl Mummert Jun 1 '16 at 23:18
  • $\begingroup$ @CarlMummert Why is that? And then can we at least give large classes of examples? $\endgroup$ – fhyve Jun 2 '16 at 3:35
  • 1
    $\begingroup$ @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. $\endgroup$ – Carl Mummert Jun 2 '16 at 11:59
  • $\begingroup$ 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. $\endgroup$ – J Marcos Jun 2 '16 at 17:44

Remember that the set of theorems of intuitionistic logic is a proper subset of the set of theorems of classical logic. So, if you want to translate every classical theorem to an intuitionistic version you will fail in general.

  • $\begingroup$ This doesn't actually address the question - I think you misunderstand what a "translation" means in this context. Keep in mind that there are translations, such as the double-negation translation mentioned. $\endgroup$ – Noah Schweber Jun 3 '16 at 23:33
  • $\begingroup$ 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). $\endgroup$ – fhyve Jun 5 '16 at 17:58

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.