Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2010 / A / 3 / d / Solution

One can takeFor the first formula, the Löb axiom with conclusion $\perp$ gives $\square (\square \perp \to \perp )\to \square \perp$, that is, $\square F_1\to \square \perp$. Conversely, the tautology $\perp \to F_1$, necessitation rule, and distribution give $\square \perp \to \square F_1$. Thus $GL⊢\square F_1\leftrightarrow \square \perp$. Negating both sides gives $GL⊢\neg \square F_1\leftrightarrow F_1$.

For the second formula, $\neg F_2=\top$ is a theorem, so $GL⊢\square \neg F_2$. Hence $\neg \square F_2\wedge \neg \square \neg F_2$ is false in the logic and is equivalent to $\perp =F_2$. A fixed point is a formula satisfying the equivalence; it need not itself express a nontrivial undecidable assertion.