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

Put $Y=\square X\to X$. The Löb axiom gives $\square Y\to \square X$. Consequently $Y$ implies $\square Y\to X$: if $\square Y$ holds, first obtain $\square X$ and then apply $Y$.

For the other direction, $X\to Y$ is a propositional theorem. Necessitation and distribution give $\square X\to \square Y$. Hence $\square Y\to X$ implies $\square X\to X$, which is $Y$. We have proved the unboxed theoremNecessitation yieldsThis is the explicit fixed point for the modalized operator $Z\mapsto (\square Z\to X)$.