= 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 theorem
$$
X\to(\square C\to C).
$$
Indeed, $X$ together with $\square C$ supplies both conjuncts of $C$. Necessitate this theorem and apply distribution to obtain
$$
\square X\to\square(\square C\to C).
$$
The 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 proves
$$
\boxed{GL\vdash\square X\to\square\square X.}
$$
No positive-introspection instance was used in deriving it. The argument shows why that scheme can be dropped when the Löb scheme is added.
Back to article page
