= Solution
Let $j=i+n$ with $n\ge1$. <Positive introspection> supplies the theorem $F_k\to F_{k+1}$ for every $k\ge1$, since $F_k$ itself has the form $P_S(\ulcorner F_{k-1}\urcorner)$.
<Induction> on $n$ consequently gives
$$
S\vdash F_{i+1}\to F_{i+n}.
$$
At $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$ gives
$$
S\vdash F_{i+1}\to F_i,
$$
i.e. $S\vdash P_S(\ulcorner F_i\urcorner)\to F_i$. Löb's rule now yields
$$
\boxed{S\vdash F_i.}
$$
The 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.
Back to article page
