Part 3: Proofs with Contradictions

Introduction

Last chapter, we saw how to prove that something is a tautology, and we learnt how to do natural deduction with the \( \Rightarrow \) and \( \land \) operators. We still have a few other operators to learn though, and it turns out we need to reason about contradictions (statements that are always false, as opposed to a tautology which is always true).

The True and False Symbols

The \( \textit{true} \) symbol denotes a proposition that is, well, always true. Proving that it holds is very simple, because you don't have to do anything! On the other hand, the \( \textit{false} \) symbol denotes a proposition that cannot possibly be true, which is to say, a contradiction. Their truth tables are very straightforward, because there are no variables involved:

 \( \textit{true} \)
 1

 \( \textit{false} \)
 0

How can we ever prove \( \textit{false} \) if it cannot possibly be true? Well, we can never prove it just by itself (without making additional assumptions). However, we can use it in a proof by contradiction, where you assume something that might not be true, and then prove that this would lead to \( \textit{false} \). In the real world, this could look like the following (somewhat questionable) argument:

"If ice cream was healthy, everyone would be eating it all the time, so it must not be healthy."

Here we first assume for the sake of argument that it is healthy. Then we use that assumption to derive a contradiction; namely, everyone would be eating it all the time, which contradicts with the (questionable) premise that people rarely eat it. From this, we conclude that the opposite of the assumption must have been true, so it is not healthy.

The \( \textit{true} \) and \( \textit{false} \) symbols have introduction and elimination rules that are relatively straightforward. The introduction rule for \( \textit{true} \) is trivial because it does not have any conditions:

{ by introduction rule for \( \textit{true} \) }
\( \textit{true} \)

The elimination rule for \( \textit{false} \) says that, if you know that both something itself and its negation hold, then you can conclude \( \textit{false} \):

\( X \)
 
...
 
\( \lnot X \)
 
...
 
{ by introduction rule for \( \textit{false} \) }
\( \textit{false} \)

Finally there is the elimination rule for \( \textit{false} \), which says that once you've found a contradiction, you can conclude anything after that.

\( \textit{false} \)
 
...
 
{ by elimination rule for \( \textit{false} \) }
\( X \)

Rules for \( \lnot \)

To prove a negation \( \lnot X \), we use the reasoning principle from the ice cream example from before. We assume the positive form \( X \) and then derive a contradiction \( \textit{false} \). The rule looks as follows:

assume \( X \)
 
...
 
\( \textit{false} \)
 
{ by introduction rule for \( \lnot \) }
\( \lnot X \)

TODO