4.1 Iteracio

Tiu estas tre simpla regulo:

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

Nu, tiel verkite estas iom konfuza, sed ĉi tio estas ĝia formala difino, do estas la plej utila maniero skribi la regulon. Supra formulaĵo signifas ke se en linio numero $n$ estas verkata $A$ (ia ajn esprimo) tiam oni povas reskribi $A$ en la nuna linio, klarigante tiun aldonon per la noto $IT\ n$ verkita dekstre.

Do kial oni volus tion? Ĝis la momento, por nenion, tamen, tio havos sian utilecon poste, kiam oni komencos uzi hipotezojn. Ĉar hipotezo estas ferma (malebligas eniron aŭ eliron de formuloj), ĉiuj reguloj devos uzi formulojn el ĉe la hipotezo. Se nia ŝatita formulo estas tuj ekstere de tiu hipotezo, oni povas enmeti ĝin uzante la iteracion.

Iuj kredas ke ne estas necese elspezi linion tiel, sed ĝia uzado multe klarigas la skemojn. Sed io malpermesita estas uzi ĝin nur por ``alproksimigi'' formulon kiu estas kelkajn liniojn supre: estas malnecese reskribi linion kiu jam estas skribita supre en la nuna derivo.