Csdrhrt

After reading and being inspired by, Can every proof by contradiction also be shown without contradiction? and after some thought, I still don't have an answer to this.

Does every theorem with a true proof have a proof by contradiction?

In classical logic, the answer is yes. Take any theorem $T$ and any proof $P$ for $T$. Now write the following proof:

If $neg T$:

  [Write $P$ here.]

  Thus $T$.

  Thus a contradiction.

Therefore $neg neg T$, by negation introduction.

Thus $T$, by double negation elimination.

One may object that this proof is essentially the same as $P$, and is just wrapped up. That is true, but it is a perfectly legitimate proof of $T$, even if it is longer than $P$, and it is indeed of the form of a proof by contradiction. A natural question that arises is whether the shortest proof of $T$ is a proof by contradiction. That is a much harder question to answer in general, but there are some easy examples, at least for any reasonable natural deduction system.

For instance, the shortest proof of "$A to A$" for any given statement $A$ is definitely not a proof by contradiction but rather just:

If $A$:

  $A$.

Therefore $A to A$, by implication introduction.

On the other hand, the shortest proof of "$neg ( A land neg A )$" for any given statement $A$ is definitely a proof by contradiction:

If $A land neg A$:

  $A$, by conjunction elimination.

  $neg A$, by conjunction elimination.

  Thus a contradiction.

Therefore $neg( A land neg A )$.

The first part of this post shows that the shortest proof by contradiction is at most a few lines longer than the shortest proof, but nothing much else interesting can be said about the shortest proof unless...

Well what if we do not allow the use of double negation elimination? If you have only the other usual rules (the first-order logic rules here but excluding ¬¬elim and including ex falso), then the resulting logic is intuitionistic logic, which is strictly weaker than classical logic, and cannot even prove the law of excluded middle, namely "$A lor neg A$" for any statement $A$. So if you instead ask the more interesting question of whether every true theorem can be proven in intuitionistic logic, then the answer is no.

Note that intuitionistic logic plus the rule "$neg A to bot vdash A$" gives back classical logic, and one could say that this rule embodies the 'true principle' of proof by contradiction, in which case one can say that some true theorems require the use of a proof by contradiction somewhere.

If you can prove a statement $A$ directly, you can prove it by contradiction. Just assume $lnot A$, perform your proof of $A$, note the contradiction, and derive $A$.

I find the common thought here unsettling, even if seemingly widely held. Perhaps others share my view, perhaps not (and note, it is just an intuitive view, one which--as explained to me in the comments--isn't in line with the notion of proof!)

The proof in these purported proofs by contradiction must necessarily rely on the content of the direct proof. Yes, we have ourselves a contradiction, but in a proof by contradiction what convinces us (i.e., what we count as the proof) is not merely that we have a contradiction, but that we have derived a contradiction in a particular manner--from particular assumption(s)--which leads us to conclude something about these assumptions....that they must not be true.

Here, all we do is prove a statement directly from the premises of the argument, and make a note that our conclusion contradicts the conclusion's_negation--leading us to believe that the negation of the conclusion's_negation (i.e., our conclusion) must be true. We then say to ourselves "aha! Indeed this is the case...since we have already (directly) proven our conclusion to be true!"

It is not simply that our conclusion need not be derived via contradiction (and that it can be done directly and then "wrapped up" in a so called proof by contradiction), but rather that our conclusion has not been derived in this manner.

A contradiction arising in a proof does not necessarily warrant that the method of proof being employed is what we call "proof by contradiction." It is the derivation of this contradiction which warrants the name "proof by contradiction." It is how the contradiction arises. And here, our contradiction doesn't really arise so much as the situation is one in which we are pointing out that a directly derived conclusion is contradictory to its negation.