# Is there a reverse double-negation translation?

There are many double-negation translations $$f$$, each with the property that $$\vdash\varphi$$ classically iff $$\vdash f(\varphi)$$ intuitionistically. Is there a translation the other way? Specifically, I mean, is there a function $$f$$ on formulae such that $$\vdash\varphi$$ intuitionistically iff $$\vdash f(\varphi)$$ classically?

For the purposes of this question, let us consider only propositional (intuitionistic and classical) logic, even though the double-negation translations mentioned above generalize to first-order logic.

Even in just the propositional case, given the difference in complexity between the two logics' semantics, one would expect any such $$f$$ would increase the size/complexity of its argument, perhaps even a lot. But making the translation as efficient as possible is a secondary (bonus?) question that comes after the question of whether such a translation exists at all.

• I suspect the answer is "no", but I don't have a proof or a reference. The idea is that clasiscal logic is intuitionistic logic plus a ~bonus axiom~ (LEM). So to simulate classical logic intuitionistically, all we need to do is find a subset of formulas validating that bonus axiom, and the double-negated ones fit the bill (there's more to say here, obviously, but comments are short). Conversely, once you have access to the bonus axiom, it's comparatively hard to restrict its use. Jun 29 at 20:24
• That said, if you're willing to expand your classical language slightly to allow a new symbol $\square$, then we can interpret intuitionistic logic classically by embedding it into a modal logic, for instance, S4. If you like, I can write up an answer to this effect, but I'm not sure if it actually answers your question (which is why I'm leaving a comment instead) Jun 29 at 20:25
• For the first-order logic case, you could translate $\varphi$ to "the axioms of a Heyting algebra imply that for every assignment of values to the free variables of $\varphi$, the formula for $\varphi$ evaluates to $\top$". Jun 29 at 21:51

Based on an analysis of computational complexity, we should not expect any such $$f$$ to be computable in polynomial time.
It is well-known that the problem of determining whether $$\vdash \phi$$ classically is a co-NP complete problem, since its complement is trivially equivalent to the famous satisfiability problem, the first problem ever proved to be NP-complete.
It is less known, but still established in the literature, that the task of determining whether $$\vdash \phi$$ constructively is PSPACE-complete.
If we had a polynomial-time reduction $$f$$ from the intuitionist problem to the classical problem, this would prove that $$PSPACE = co-NP = NP$$. However, it is not presently known whether $$PSPACE = NP$$, nor is it even known whether $$NP = co-NP$$.
Of course, if we wanted to be silly, we could define $$f(\phi) = \top$$ if $$\phi$$ is an intuitionist tautology and $$\bot$$ otherwise. This would satisfy your criterion. But this function does not reveal much insight, and, as mentioned, computing $$f(\phi)$$ is a $$PSPACE$$-complete problem which we should not expect to be solvable in polynomial time.
• Even though, as you say, this is not a full answer, it is still very helpful--thank you! My interest in the question was to detect whether $\vdash\varphi$ intuitionistically by applying a SAT solver (some of which are remarkably fast) to check if $\vdash f(\varphi)$ classically. Your comments suggest that $f(\varphi)$ will be very large, so this might not be a useful strategy--depending on how the output of $f$ comports with the optimizations of the SAT solver. Jun 30 at 13:15