= Solution
<Set> $Y=\square X\to X$. The Löb axiom at $X$ is $\square Y\to\square X$. Therefore $Y$ and $\square Y$ together imply $X$, proving
$$
GL\vdash Y\to(\square Y\to X).
$$
For the converse, the tautology $X\to Y$ gives $\square X\to\square Y$ by necessitation and distribution. Consequently $\square Y\to X$ together with $\square X$ gives $X$, so
$$
GL\vdash(\square Y\to X)\to(\square X\to X),
$$
whose consequent is $Y$. Combining both directions gives an unboxed equivalence as a theorem of GL. Necessitation then yields exactly
$$
\boxed{GL\vdash\square\bigl(Y\leftrightarrow(\square Y\to X)\bigr).}
$$
Back to article page
