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

Take the outermost boxed subformulas of $X(p)$ containing the distinguished letter. Because $X$ is modalized in $p$, every occurrence of $p$ lies inside one of these boxes. The supplied decomposition therefore has the formwhere $H$ has no occurrence of $p$. Other letters and subformulas not involving $p$ may be retained as parameters in $H$ and the $C_i$.

Introduce temporary letters $q_1,\dots ,q_m$ and solve the boxed systemby part (b), obtaining $Q_i$ without the temporary letters or $p$. Put $F=H(Q_1,\dots ,Q_m)$. Each solved equation gives $GL⊢Q_i\leftrightarrow \square C_i(F)$. The supplied replacement-of-equivalents principle then givesOnly letters already present in $X$, apart from the removed $p$, occur in the constructed $F$. If $p$ is absent from $X$ to begin with, take $F=X$. This is the modalized fixed-point theorem for GL, proved by finite elimination rather than a semantic completeness argument.