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)