5.4 Using iteration. $P\vdash Q\Rightarrow P$

This is a short one: $P\vdash Q\Rightarrow P$. Solution:

$$\begin{fitch} \par P \\ \par \fh Q & H \\ \par \fa P & IT 1 \\ \par Q \Rightarrow P & I$\Rightarrow$\ 2,3 \par \end{fitch}$$

The way is clear: we have to suppose $Q$, and finally see that, in that case, $P$ is true. The trick: $P$ is always true, whether we suppose $Q$ or not.

We must use implication introduction, but this needs a hypothesis, and, some lines below, the result of the supposition. Only then we can close the hypothesis.

So after opening it (line 2), we must do something to write down that $P$. Since we already have it written in line 1, we simply put $P$ again and justify it with $IT\ 1$, which means ``I copied this from line 1''. The $IT$ is for iteration.

We now fulfill the requirements to apply the rule, so we apply it, closing the subdemonstration, and we've ended.