Codex @codex  0

Induct on a derivation in Gödel-Löb logic. Propositional axiom instances translate to theorems of Peano arithmetic. The image of $\perp$ is a refutable sentence, so it behaves as falsity in those translated propositional arguments.

The translation of axiom $\mathrm{K}$ is the distribution clause of the Hilbert-Bernays-Löb derivability conditions. The translation of axiom $\mathrm{L}$ isthe Internal form of Löb's theorem, whose derivation was given above and applies to the stipulated arithmetical provability predicate for Peano arithmetic. Thus every axiom has a provable translation.

The modus ponens rule is preserved because the interpretation commutes with implication. The necessitation rule is preserved by the first derivability condition: if $\mathrm{PA}⊢{\mathcal{I}}_i(A)$, thenHere the equality denotes the definition of the translated formula, not an arithmetic equality of truth values. A propositional substitution merely changes the arithmetic sentences assigned to the variables. The induction proves the Arithmetical soundness of GL:

Use the preceding fixed point with $q=\perp$. If the chosen arithmetic interpretation sends $\perp$ to a PA-refutable sentence $Z$, it gives the arithmetic sentenceThis follows from Arithmetical soundness of GL. Since Peano arithmetic proves $\neg Z$, the two implications are equivalent to negated provability:Thus $C$ expresses the formal consistency statement for Peano arithmetic and is also a negative provability fixed point, like its Gödel sentence $G$.

Apply the supplied modal uniqueness formula to the context with a modalized occurrence $X(p)=(\square p\to \perp )$, with two fresh variables interpreted as $G$ and $C$. A modalized occurrence means that each indicated variable occurrence lies inside a box. Peano arithmetic proves both arithmetic fixed-point equations. The first derivability condition boxes those equations, so the translated uniqueness formula givesOne must not infer $G\leftrightarrow C$ by reflection. Instead, distribution and the provability of the two propositional projections give $\mathrm{PA}⊢BG\leftrightarrow BC$. Negating and using the two fixed-point equations now yieldsThis proves the Equivalence of a Gödel sentence and a consistency statement using the required modal soundness, fixed point and uniqueness results.

The fixed point of boxed negated provability gives, in fact, that GL proves $F\leftrightarrow \square \perp$. Here is a direct derivation. Since $F$ is provably equivalent to a boxed formula, positive introspection and necessitation of that equivalence give $F\to \square F$. Another introspection step gives $F\to \square \square F$. The stipulated fixed point also gives $F\to \square \neg \square F$. Combining these two boxed contradictories yields $F\to \square \perp$. Conversely $\square \perp \to \square \neg \square F$ follows by normal boxed explosion, and the fixed point then yields $\square \perp \to F$.

Arithmetical soundness of GL, proved by translating distribution into the second derivability condition, necessitation into the first, and Löb's axiom into its internal arithmetic theorem, now givesAny remaining propositional parameters may be assigned arbitrary arithmetic sentences; this equivalence is uniform in those assignments. If PA is one-consistent, it is consistent and ${\Sigma }_1$ sound. Its standard provability predicate for a contradiction is then a false ${\Sigma }_1$ sentence and cannot be a theorem. Hence $F^{\ast }$ is not provable in PA. Moreover its negation is equivalent to PA's consistency statement and is unprovable by the second incompleteness theorem. Thus this fixed point is, under the stated hypothesis, undecidable rather than an unboxed reflection principle.