Induct on a derivation in Gödel-Löb logic. Propositional axiom instances translate to theorems of Peano arithmetic. The image of

⊥

is a refutable sentence, so it behaves as falsity in those translated propositional arguments.

The translation of axiom

K

is the distribution clause of the Hilbert-Bernays-Löb derivability conditions. The translation of axiom

L

PA ⊢ B (B A \to A) \to B A,

(1)

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

PA ⊢ I_{i} (A)

, then

PA ⊢ P r (┌ I_{i} (A) ┐) = I_{i} (□ A) .

(2)

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: