= Solution
One can take
$$
\boxed{F_1=\neg\Box\bot,\qquad F_2=\bot.}
$$
For the first formula, the Löb axiom with conclusion $\bot$ gives $\Box(\Box\bot\to\bot)\to\Box\bot$, that is, $\Box F_1\to\Box\bot$. Conversely, the <tautology> $\bot\to F_1$, <necessitation rule>, and distribution give $\Box\bot\to\Box F_1$. Thus $GL\vdash\Box F_1\leftrightarrow\Box\bot$. Negating both sides gives $GL\vdash\neg\Box F_1\leftrightarrow F_1$.
For the second formula, $\neg F_2=\top$ is a theorem, so $GL\vdash\Box\neg F_2$. Hence $\neg\Box F_2\wedge\neg\Box\neg F_2$ is false in the logic and is equivalent to $\bot=F_2$. A fixed point is a formula satisfying the equivalence; it need not itself express a nontrivial undecidable assertion.
Back to article page
