= Solution
Use the supplied uniqueness theorem for the modalized <logical formula> $A(p)=\Box 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=\Box X\to X$. Uniformly substitute $Y$ for the fresh letter $q$ in the uniqueness theorem. Since $q$ occurs nowhere in $X$, this gives
$$
GL\vdash\bigl(\Box(p\leftrightarrow(\Box p\to X))\wedge
\Box(Y\leftrightarrow(\Box Y\to X))\bigr)\to\Box(p\leftrightarrow Y).
$$
Part (c) proves the second conjunct outright. Propositional reasoning removes that already-proved conjunct and yields
$$
\boxed{GL\vdash\Box(p\leftrightarrow(\Box p\to X))\to
\Box(p\leftrightarrow(\Box X\to X)).}
$$
The freshness conditions make the substitution legal and ensure it changes only the placeholder intended for the second fixed point.
Back to article page
