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

Use the supplied uniqueness theorem for the modalized logical formula $A(p)=\square p\to X$. Its occurrence of $p$ is boxed, and the source assumes $p$ does not occur in $X$. Choose another first-order sentence letter $q$ absent from $X$ and from $p$. Besides the uniqueness theorem and propositional reasoning, use that GL is closed under uniform substitution in modal logic.

Let $Y=\square X\to X$. Uniformly substitute $Y$ for the fresh letter $q$ in the uniqueness theorem. Since $q$ occurs nowhere in $X$, this givesPart (c) proves the second conjunct outright. Propositional reasoning removes that already-proved conjunct and yieldsThe freshness conditions make the substitution legal and ensure it changes only the placeholder intended for the second fixed point.