= Solution
Induct on a derivation in <Gödel-Löb logic>. Propositional axiom instances translate to theorems of <Peano arithmetic>. The image of $\bot$ 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$ is
$$
\operatorname{PA}\vdash B(BA\to A)\to BA,
$$
the <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 $\operatorname{PA}\vdash\mathcal I_i(A)$, then
$$
\operatorname{PA}\vdash Pr(\ulcorner\mathcal I_i(A)\urcorner)=\mathcal I_i(\Box A).
$$
Here 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>:
$$
\boxed{\mathrm{GL}\vdash A\quad\Longrightarrow\quad\operatorname{PA}\vdash\mathcal I_i(A).}
$$
Back to article page
