= Fixed point of boxed negated provability
{title2=$F\leftrightarrow\Box\neg\Box F\quad\Longrightarrow\quad F\leftrightarrow\Box\bot$}
A formula provably equivalent to a boxed formula satisfies $F\to\Box F$ in <GL>. The displayed <logical fixed point>[fixed point] then gives both $\Box\Box F$ and $\Box\neg\Box F$ under $F$, hence $\Box\bot$. Boxed explosion proves the reverse implication. Under arithmetic realization this is a formal inconsistency statement; <Sigma-1 soundness> excludes its provability, while second incompleteness excludes provability of its <negation>.
Back to article page
