4.1 Iteració

Aquesta és una regla molt senzilla:

$$\begin{fitch*} \par n & A \\ \par \hline \par & A & IT n \par \end{fitch*}$$

Sí, ho sé, escrit així queda bastant estrany, però és per a què serveixi com a definició. Això de dalt vol dir que si en la línia número $n$ tenim escrit $A$ (sigui l'expressió que sigui) llavors podem tornar a escriure $A$ a la línia actual, i per justificar-ho hem d'escriure a la dreta $IT\ n$.

Que per a què serveix això? Doncs de moment, per res, però tindrà la seva utilitat quan comencem a fer allò de les hipòtesis. Com que una hipòtesi és tancada, totes les regles hauran de treballar amb fórmules que es trobin dins de la hipòtesi. Si una fórmula està just a fora, la podem ficar dins amb això de la iteració.

Alguns creuen que no és necessari gastar una línia així, però queda molt més clar quan s'usa. El que no s'accepta és usar-la només per ``apropar'' una fórmula que queda vàries línies per damunt: no fa falta tornar a escriure una línia si ja la tenim a dalt en la derivació actual.