Can every true theorem that has a proof be proven by contradiction?

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?

• Let $P$ be a proof of the theorem. Assume the theorem is false. However we can exhibit $P$, which contradicts the assumption. – Stahl Jan 3 '17 at 4:11
• I think @Stahl is correct – MPW Jan 3 '17 at 4:22
• @Masacroso note that I did not post it as an answer, but rather as a comment ;) I'm neither a logician nor particularly interested in the subtleties of logic, and I assume someone can and will give a better explanation than I can. However, I have a hunch that one can formalize what I've said. – Stahl Jan 3 '17 at 4:26
• I think @Stahl is correct. Many so-called proofs by contradiction amount to assuming the result is false, proceeding to prove the result, then saying that the proven result then contradicts the hypothesis that it is false. It's a classic overkill used by many students when they could just prove the result directly. – MPW Jan 3 '17 at 4:28
• Ah, sorry, I missread the question as the opposite direction. Anyway it is not clear to me if this is possible or not, I mean that we can construct a proof by contradiction derived from any other proof, but then the status of this proof to be "by contradiction" is not very clear (because the statement is already proved before to "prove it but this derived proof"). – Masacroso Jan 3 '17 at 4:57

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$$.

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.

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.

• Your intuition makes sense, but raises the challenge of how to precisely define what a "proof by contradiction" actually is then. – Eric Wofsey Jan 3 '17 at 23:10
• The conclusion that gives you your result in a straightforward proof becomes the conclusion that gives you a contradiction in the new proof. In other words, we can rephrase any proof as a proof by contradiction. – Morgan Rodgers Jan 3 '17 at 23:13
• I'm not reading the other answers as suggesting to insert a reference to another proof, but rather to repeat the arguments. – Morgan Rodgers Jan 4 '17 at 2:28
• I meant that it is of a specific syntactic form; it begins with a subproof of a contradiction under an assumption of the form $\neg A$, and then deduces $\neg \neg A$ and then applies DNE to get $A$. So when I said "form" in my answer I do not refer to the notion of "method" that most non-logicians have in mind. Is what I say clearer now? – user21820 Jan 4 '17 at 5:15
• The specific details of the syntactic form will depend on the specific formal system chosen, so you can consider the proof sketch in my answer akin to pseudo-code. If you use the rules in my linked post, then "form of a proof by contradiction" in my answer corresponds to a formal proof whose last 3 lines are of the form: $$¬A→⊥. \quad [→intro] \\ ¬¬A. \quad \quad \quad [¬intro] \\ A. \quad \quad \quad \quad [¬¬elim]$$. By the way, your answer is related to mathoverflow.net/questions/3776/…. – user21820 Jan 4 '17 at 5:38