= Solution
The language of <Gödel-Löb logic> has <propositional variables>, $\bot$, implication, and the unary operator $\Box$; the other <logical connectives> are abbreviations. Its axioms are all classical <tautologies>, the distribution scheme $\Box(A\to B)\to(\Box A\to\Box B)$, and the Löb scheme $\Box(\Box A\to A)\to\Box A$. Its rules are <modus ponens rule>, <necessitation rule> of theorems, and uniform substitution.
For a single boxed equation $p\leftrightarrow\Box C(p)$, set $F=\Box C(\top)$. The identity supplied in the source gives directly $GL\vdash F\leftrightarrow\Box C(F)$. If $p$ does not occur, take $F=\Box C$ instead.
Proceed by induction for a system of $m$ equations, allowing other <propositional variables> as parameters. Treat $p_1,\ldots,p_{m-1}$ as parameters in the last equation and put
$$
D(p_1,\ldots,p_{m-1})=\Box C_m(p_1,\ldots,p_{m-1},\top).
$$
The one-variable result proves $D\leftrightarrow\Box C_m(p_1,\ldots,p_{m-1},D)$. Substitute this $D$ for $p_m$ in the first $m-1$ equations. They are still boxed equations, so induction supplies solutions $F_1,\ldots,F_{m-1}$. Define $F_m=D(F_1,\ldots,F_{m-1})$.
By construction, the first $m-1$ equations hold after this substitution; substituting into the theorem for $D$ proves the last. Hence
$$
\boxed{GL\vdash F_i\leftrightarrow\Box C_i(F_1,\ldots,F_m)\quad(1\leq i\leq m).}
$$
The elimination introduces no new parameter letters and removes every unknown letter. This gives a constructive <simultaneous boxed fixed-point elimination in GL>.
Back to article page
