5.4 Uzante iteracion. $P\vdash Q\Rightarrow P$

Tiu ĉi estas tre mallonga: $P\vdash Q\Rightarrow P$. Jen solvo:

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

La vojo estas direkta: oni supozu $Q$, kaj vidu ke, tiuokaze, estas prava $P$. Jen sekreteto: $P$ ĉiam certas, ĉu supozinte $Q$ aŭ ĉu ne.

Oni devos uzi kunimplikaciigon, sed tio necesas hipotezon, kaj, kelkaj linioj sube, la rezulton supozi tion. Nur tiam oni povos fermi la subderivon.

Post ĝia malfermo (linio 2), oni faru ion por restigi skribe ke $P$. Ĉar ni jam havas ĝin verkita en linio 1, simple metu $P$ denove kaj klarigu per $IT\ 1$, kio signifas ``ĉi tion mi kopiis de linio 1''. La $IT$ estas pro iteracio.

Jam oni plenumas la kondiĉojn por apliki la derivregulon, do oni apliku ĝin, eliru el subderivo, kaj jam estas finita.