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

Let $C=\square X\wedge X$. The normal distribution axiom and necessitation of $C\to X$ give $\square C\to \square X$. Combining this with propositional reasoning yields the theoremIndeed, $X$ together with $\square C$ supplies both conjuncts of $C$. Necessitate this theorem and apply distribution to obtainThe new Löb axiom at $C$ now gives $\square X\to \square C$. Finally, necessitation and distribution applied to the tautology $C\to \square X$ give $\square C\to \square \square X$. Composition provesNo positive-introspection instance was used in deriving it. The argument shows why that scheme can be dropped when the Löb scheme is added.