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.