# 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

## 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