4.1 Iteración

Esta es una regla muy sencilla:

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

Vale, escrito así queda muy raro, pero es para que sirva como definición. Lo que hay aquí arriba quiere decir que si en la línea número $n$ tenemos escrito $A$ (sea la expresión que sea) entonces podemos volver a escribir $A$ en la línea actual, y para justificarlo tenemos que escribir a la derecha $IT\ n$.

¿Que para qué sirve esto? Pues de momento para nada, pero tendrá su utilidad cuando empecemos a hacer lo de las hipótesis. Como una hipótesis es cerrada, todas las reglas tendrán que trabajar con fórmulas que hay dentro de la hipótesis. Si una fórmula que queremos está justo fuera de esta hipótesis, la podemos meter dentro con lo de la iteración.

Algunos creen que no es necesario gastar una línea así, pero queda mucho más claro cuando se usa. Lo que no se acepta es usarla sólo para ``acercar'' una fórmula que queda muchas líneas por arriba: no hace falta volver a escribir una línea si ya la tenemos arriba en la derivación actual.