I do understand that constructive logic forbids the "lemma of excluded middle" for various reasons (let's not discuss these now).
I do understand that lots & lots of classical theorems are done with LEM in place – mostly, implicitly, which renders them invalid within the constructive approach.
Recently I've met the double negation translation which states that:
If $T$ is a set of axioms and $\phi$ is a formula, then $T$ proves $\phi$ using classical logic if and only if $T^N$ proves $\phi^N$ using intuitionistic logic.
That sounds like the intuitionistic logic is at least as strong as the classical logic in the sense that at least all the classical theorems whatsoever are provable constructively. And then this answer emerges in front of my eyes stating: "a statement provable in PA (Peano arithmetic) but not in HA (Heyting arithmetic)".
I can't get it. Why could not some "double negation translation" be used here to prove it? What is the "double negation translation" essentially then? Where can I find a good example of some well known classical theorem to be "translated" using it?
P.S. It might be wrong, but terms "constructive logic" and "intuitionistic logic" are interchangeable to me.
From the discussion in the comments: not every statement provable classically can be proved within the constructive logic as is. However, translated instance of it could be proved indeed. That comes at the cost of being much weaker due to double negation constructive flavor: proving that "some set $X$ has some element" is one thing and proving that "it is not the case that the set $X$ does not has any element" – is another. The last statement is much weaker, especially in the constructive sense: in order for it to be as strong as the classical mate, it has to construct some element $x \in X$, which the double negation translation does not achieve.
Best Answer
Say you have a propositional $\phi$ provable classically, then double negation translation basically says $\neg\neg\phi$ is provable intuitionistically, how can you then prove $\phi$ still with intuitionistic logic alone? Where classical logic can prove "set $X$ has an element", intuitionistic logic can (prima facie) only prove its double negation, that is "It's not the case that $X$ is empty", which is definitely weaker (saying that something is non-empty is not the same as producing an actual element of $X$, which is the requirement for a constructive proof that $X$ has an element).
That being said, I'd like to add if you have a negative proposition, then this is provable classically if and only if provable intuitionistically, since $\neg\neg\neg\phi\Rightarrow\neg\phi$ intuitionistically. So a corollary of double negation translation is that "A proposition $\neg\phi$ can be proved classically if and only if it can be proven intuitionistically".