This may be a duplicate question but I am curious as to the answer regarding the statement "some theorems can only be proved by contradiction".
In Can every proof by contradiction also be shown without contradiction the highly voted answer claims that
It is known that there are statements that are provable in intuitionistic logic but not in minimal logic, and there are statements that are provable in classical logic that are not provable in intuitionistic logic.
Further in Theorems that we can only prove by contradiction the answer claims that
There are in fact numerous theorems that cannot be proved without arguing by contradiction. A nice example is the extreme value theorem (EVT). One cannot prove this theorem without an argument by contradiction, whose main ingredient is the Law of Excluded Middle (LEM). There are alternatives to classical logic where the LEM is not part of the package. Such logics are generally known as intuitionistic logics. It turns out that the extreme value theorem is actually false in one such setting. From this it follows that the EVT cannot be proved without LEM.
My problem is that as far as I am aware classical logic can be embedded in intuitionistic logic via double-negation translation. See Double-negation translation
What does this mean? Does it simply mean that the consistency strength is the same, or does it mean that all classical theorems can be proved in a classically equivalent form without contradiction? In fact is there a difference between those two statements?