5.5 Reduction to the absurd. $P\Rightarrow Q,\ \neg Q\vdash\neg P$

This is a very useful technique. Validity of $P\Rightarrow Q,\ \neg Q\vdash\neg P$ is proved with:

$$\begin{fitch} \par P \Rightarrow Q \\ \par \neg Q \\ \par \... ...neg Q & IT 2 \\ \par \neg P & I$\neg$\ 3,4,5 \par \end{fitch}$$

What has to be achieved here is $\neg P$, which is the negation of something, so the rule which will help is the negation introduction, also known as reduction to the absurd.

The way to act will be to suppose the contrary of $\neg P$ (which is $P$) and find a contradiction (any). Supposing $P$ will lead us to $Q$ (by implication elimination), and, as we also have $\neg Q$, we can apply the rule. This $\neg Q$ should be inserted in the current subdemonstration with the iteration rule, so that it is together with the $Q$ and inside the subdemonstration. Everything which is inside the subdemonstration is consequence of $P$, so it is important to see that both $Q$ and $\neg Q$ also are.

For the negation introduction, the way to justify this rule is putting the line number of where does the (wrong) supposition start, and the numbers of the two lines where we saw the contradiction. The conclusion of this rule is the contrary of what we just supposed, in this case $\neg P$, so we can finish the derivation here.

This reasoning is actually made without much thinking. In words it would be something like: ``of course that$\neg P$, since if it were $P$ then $Q$, and you say that $\neg Q$, so it can't be that $P$''.