= Modalized fixed-point theorem for GL
{title2=$GL\vdash F\leftrightarrow X(F)$}
If every occurrence of $p$ in $X(p)$ lies under a box, <Gödel-Löb logic> has a formula $F$ without $p$, using only the other letters of $X$, satisfying the displayed equivalence. Write $X(p)=H(\Box C_1(p),\ldots,\Box C_m(p))$ using the outermost boxes that contain $p$, so $H$ has no $p$. Solve $q_i\leftrightarrow\Box C_i(H(q_1,\ldots,q_m))$ by <simultaneous boxed fixed-point elimination in GL>. If the solutions are $Q_i$, then $F=H(Q_1,\ldots,Q_m)$ works by replacement of provably equivalent formulas.
Back to article page
