= Solution
Take $Y(p)=p\to q$ and put $\top=(\bot\to\bot)$, $H=Y(\top)$ and $F_0=Y(\Box H)=\Box H\to q$. The first supplied substitution identity reads
$$
\mathrm{GL}\vdash\Box H\leftrightarrow\Box Y(\Box H)=\Box F_0.
$$
Use the supplied replacement of equivalents in the context $D(p)=p\to q$. It gives
$$
\mathrm{GL}\vdash F_0\leftrightarrow(\Box F_0\to q).
$$
But $H=(\top\to q)$ is equivalent to $q$. Replacement under a box gives $\Box H\leftrightarrow\Box q$, so $F_0$ is equivalent to
$$
\boxed{F=(\Box q\to q).}
$$
Replacing equivalents once more transfers the fixed-point equation to $F$, proving $\mathrm{GL}\vdash F\leftrightarrow(\Box F\to q)$.
A direct check of this <GL fixed point for a provability implication> is useful: the Löb axiom gives $\Box F\to\Box q$, and necessitating the <tautology> $q\to F$ gives $\Box q\to\Box F$ by $\mathrm K$. Thus $\Box F\leftrightarrow\Box q$, and replacing the antecedent in $\Box F\to q$ recovers $F$.
Back to article page
