Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2008 / A / 3 / d

Let $j=i+n$ with $n\ge 1$. Positive introspection supplies the theorem $F_k\to F_{k+1}$ for every $k\ge 1$, since $F_k$ itself has the form $P_S(┌F_{k-1}┐)$.

Induction on $n$ consequently givesAt $n=1$ this is the identity implication. To pass from $n$ to $n+1$, compose the induction hypothesis with the positive-introspection implication at $k=i+n$, which is at least one. Composing the result with the assumed $F_j\to F_i$ givesi.e. $S⊢P_S(┌F_i┐)\to F_i$. Löb's rule now yieldsThe index restriction on positive introspection has been respected even when $i=0$: the chain begins at $F_{i+1}$, which already is a provability assertion.