How can we tell if a proof by contradiction is necessary?

Question

I saw this post, whose answer states that within certain systems of logic, there are statements that can only be proven by contradiction. If we only consider classical logic, is it still true that there are things that can only be proven by contradiction?

Answer 1

No. Since $(\text{not }A) \implies B$ is equivalent to $(\text{not } B) \implies A$, any proof of the following form:

1. Suppose (not A)
2. Then B
3. But (not B)
4. Therefore A.

can be rewritten as

1. (not B)
2. (not B) implies A
3. Therefore A.

Answer 2

There are certain cases which are easier to proof by contradiction, rather than applying straightforward logic.

For example, if we need to show that √2 is irrational, we simply prove that by contradiction, because it's easier than other methods.

By general, we cannot tell instantly that weather we need to use contradictive method, but see if it is shorter than others or lengthy.

Answer 3

Any assertion $P$ is logically equivalent to $\neg P\Rightarrow{\rm false}$. So its just proving an equivalent statement. As said, some proofs are easier using contradition.

Answer 4

If you consider formal proof systems, then the answer is yes: in some (many?) formal proof systems you cannot do without proof by contradiction for some proofs.

You can prove that you need the proof by contradiction by proving that without it, the proof system is not complete. And to prove that, you have to use non-classical semantics where, for example, statements can take on values other than just true or false. This can all be made hard mathematically, though often the proof can be tedious.

More informally and intuitively, though, take any of the many proof systems that have a pair of Introduction and Elimination rules for each connective (see the Wikipedia page on Natural Deduction for an example). Typically, the $\neg Intro$ is the formalization of the proof by contradiction (that is: if some assumption $P$ leads to a contradiction, then we can derive $\neg P$, i.e. introduce a $\neg$). Now, if we remove $\neg Intro$ from the system, then it is intuitively true that we can no longer derive something like $\neg \neg P$ from $P$. Again, that is no hard proof, but you can certainly 'tell' that something is missing.