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.