Solution

ID: past-exam-of-the-model-theory-and-godel-s-incompleteness-theorems-course-of-the-university-of-oxford/2008/a/3/d/solution

Let with . Positive introspection supplies the theorem for every , since itself has the form .
Induction on consequently gives
At this is the identity implication. To pass from to , compose the induction hypothesis with the positive-introspection implication at , which is at least one. Composing the result with the assumed gives
i.e. . Löb's rule now yields
The index restriction on positive introspection has been respected even when : the chain begins at , which already is a provability assertion.

New to topics? Read the docs here!