From wikipedia: On the contradiction-v-contrapositive question, in some sense there's no logical difference between proof by contradiction and proof by contrapositive. More precisely, if you add either inference method to intuitionistic logic you can derive the other. (Therefore neither rule is intuitionistically valid for proving existential statements). If you wanted to formalize what you could do with one that you can't do with the other, it would probably have to take some form of relevance logic as the base theory, and relevance logic is generally hard to work with or even make precise in generality.

However, there is indeed a big difference in practice. When proving A=>B by assuming A and not(B) and trying to derive a contradiction, the problem is that (assuming the theorem you're trying to prove is actually true) you're working in an impossible situation. So when you get to the "end", where you've proved C and not(C) from your assumptions, there's no little bell that rings in your head and says "hey, wait a minute, this is fishy, the situation shouldn't look like this" -- because, as it's an impossible situation, there's nothing it should look like. That means that, while the methodology is technically valid, it's very vulnerable to small, apparently inessential errors, which can allow you to derive both a statement and its negation by mistake.

On the other hand, when you start with not(B) and try to derive not(A), you have a lot more of a safety net, because presumably not(B) usually is possible (otherwise you'd usually try to prove B outright, rather than A=>B). So, if you have some experience in the area, you have a sense of what sort of thing is reasonable in the case that ÃÂB holds, and you can compare the assertions that show up in your proof with that intuition. --Trovatore 22:21, 5 July 2007 (UTC)