5.4 Usant la iteració. $P\vdash Q\Rightarrow P$

Aquest és molt curt: $P\vdash Q\Rightarrow P$. Solució:

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

El camí és directe: hem de suposar $Q$, i acabar veient que, en aquest cas, és cert $P$. El truc: $P$ és sempre cert, tant si suposem $Q$ com si no.

Haurem d'usar la introducció de la implicació, però això requereix tenir una hipòtesi, i, línies més avall, el resultat d'haver suposat això. És llavors quan podem tancar la hipòtesi.

Després d'obrir-la (línia 2), haurem de fer alguna cosa per deixar escrit que $P$. Com ja ho tenim escrit a la línia 1, simplement posem la $P$ altre cop i ho justifiquem amb $IT\ 1$, que vol dir ``això ho he copiat de la línia 1''. El $IT$ és per iteració.

Ja complim els requisits per aplicar la regla, així que l'apliquem, sortim de la subdemostració, i hem acabat.