= Solution
Put $Y=\Box X\to X$. The Löb axiom gives $\Box Y\to\Box X$. Consequently $Y$ implies $\Box Y\to X$: if $\Box Y$ holds, first obtain $\Box X$ and then apply $Y$.
For the other direction, $X\to Y$ is a propositional theorem. Necessitation and distribution give $\Box X\to\Box Y$. Hence $\Box Y\to X$ implies $\Box X\to X$, which is $Y$. We have proved the unboxed theorem
$$
GL\vdash Y\leftrightarrow(\Box Y\to X).
$$
Necessitation yields
$$
\boxed{GL\vdash\Box\bigl(Y\leftrightarrow(\Box Y\to X)\bigr).}
$$
This is the explicit fixed point for the modalized operator $Z\mapsto(\Box Z\to X)$.
Back to article page
