[quietbritishjim]

Oops, perhaps I meant proof by contradiction is equivalent to contrapositive (rather than equivalent to law of excluded middle). If you write out a classic high school proof by contradiction formally, then you find yourself basically writing out the contrapositive.

Let's say you know A and ~B=>~A, then you can deduce B. Proof by contradiction: assume otherwise, i.e. ~B, then by ~B=>~A you have ~A, but that contradicts A.

So if you have ~B=>~A then you have A=>B.

[ceh123]

Okay yup, turns out this is correct and it's slightly upsetting to me honestly haha. Just for someone else if they're interested where contrapositive and contradiction both use law of excluded middle (the ==* step requires it):

Contrapositive:

A-> B == A or ~B == ~B or A ==* ~B or ~(~A) == ~B -> ~A

Contradiction:

~(~A and B) == ~~A or ~B ==* A or ~B == A -> B

[housecarpenter]

You might be interested to know that in intuitionistic logic, you still have a one-sided contrapositive law, i.e. (A > B) > (~B > ~A):

  [1] A > B(assumption)
  [2] ~B (assumption)
  [3] A (assumption)
  [4] B (modus ponens on 1 and 3)
  [5] ~A (proof of negation on 3, 4 and 2)

It's only the converse that no longer holds. In general familiar equivalences from classical logic are still valid in intuitionistic logic but only in one direction.