= Solution
The <fixed point of boxed negated provability> gives, in fact, that <GL> proves $F\leftrightarrow\Box\bot$. Here is a direct derivation. Since $F$ is provably equivalent to a boxed formula, <positive introspection> and <necessitation rule>[necessitation] of that equivalence give $F\to\Box F$. Another introspection step gives $F\to\Box\Box F$. The stipulated <logical fixed point>[fixed point] also gives $F\to\Box\neg\Box F$. Combining these two boxed contradictories yields $F\to\Box\bot$. Conversely $\Box\bot\to\Box\neg\Box F$ follows by normal boxed explosion, and the <logical fixed point>[fixed point] then yields $\Box\bot\to F$.
<Arithmetical soundness of GL>, proved by translating <normal modal distribution axiom>[distribution] into the second derivability condition, <necessitation rule>[necessitation] into the first, and Löb's <axiom> into its internal arithmetic theorem, now gives
$$
\mathrm{PA}\vdash F^*\leftrightarrow\operatorname{Pr}_{\mathrm{PA}}(\ulcorner\bot\urcorner).
$$
Any remaining propositional parameters may be assigned arbitrary arithmetic sentences; this equivalence is uniform in those assignments. If PA is <one-consistency>[one-consistent], it is <consistent first-order theory>[consistent] and $\Sigma_1$ sound. Its standard <arithmetical provability predicate>[provability predicate] for a <contradiction> is then a false $\Sigma_1$ sentence and cannot be a theorem. Hence \b[$F^*$ is not provable in PA]. Moreover its <negation> is equivalent to PA's <consistent first-order theory>[consistency] statement and is unprovable by the <Gödel second incompleteness theorem>[second incompleteness theorem]. Thus this <logical fixed point>[fixed point] is, under the stated hypothesis, undecidable rather than an unboxed <full local reflection in a one-sentence extension is inconsistent>[reflection] principle.
Back to article page
