= Simultaneous boxed fixed-point elimination in GL
{title2=$F_i\leftrightarrow\Box C_i(F_1,\ldots,F_m)$}
In <Gödel-Löb logic>, the one-variable identity $\Box C(\top)\leftrightarrow\Box C(\Box C(\top))$ solves a boxed equation with a formula omitting its unknown letter. A finite simultaneous system can be solved by elimination. First solve its last equation with the other unknowns treated as parameters, substitute that formula into the preceding equations, and apply induction. Substituting the resulting solutions back into the last formula completes the system. This construction introduces no new parameter letters.
Back to article page
