= Solution
<GL> has all classical propositional <tautologies>, the normal <normal modal distribution axiom>[distribution] <axiom> $\Box(A\to B)\to(\Box A\to\Box B)$ and the Löb <axiom> $\Box(\Box A\to A)\to\Box A$, closed under uniform substitution, modus ponens and <necessitation rule>[necessitation] of theorems. We use its derived positive-introspection theorem $\Box A\to\Box\Box A$, normal boxed reasoning, and the boxed replacement principle supplied in the question.
For completeness, <positive introspection> follows from these <axioms>. Put $C=A\land\Box A$. <Hilbert-Bernays-Löb derivability conditions>[Distribution] gives $\Box C\to\Box A$, so <classical propositional logic>[propositional logic] proves $A\to(\Box C\to C)$. Necessitate and distribute to get $\Box A\to\Box(\Box C\to C)$; Löb's <axiom> gives $\Box A\to\Box C$, and boxing $C\to\Box A$ finishes $\Box A\to\Box\Box A$.
For a <GL fixed point by truth substitution>, <set> $\top=(\bot\to\bot)$, $U=\Box Y(\top)$ and $V=\Box Y(U)$. From the <tautology> $U\to(\top\leftrightarrow U)$, boxed reasoning gives $\Box U\to\Box(\top\leftrightarrow U)$. The supplied replacement principle and <normal modal distribution axiom>[distribution] then give
$$
\mathrm{GL}\vdash\Box U\to(U\leftrightarrow V).
$$
Since $U$ is itself boxed, <positive introspection> gives $U\to\Box U$, and hence $U\to V$.
For the reverse direction, the displayed implication entails the theorem $V\to(\Box U\to U)$. Necessitate it and distribute to obtain $\Box V\to\Box(\Box U\to U)$. Since $V$ is boxed, $V\to\Box V$ holds. The Löb <axiom> therefore yields $V\to\Box U$, and the same displayed implication then yields $V\to U$. Consequently
$$
\boxed{\mathrm{GL}\vdash U\leftrightarrow\Box Y(U),\qquad U=\Box Y(\top).}
$$
All occurrences of the unknown letter have been removed from $U$ by substitution of truth; any other parameter letters remain available. The proof does not assume the invalid <full local reflection in a one-sentence extension is inconsistent>[reflection] principle $\Box U\to U$ as an unconditional <axiom>.
Back to article page
