Arithmetical soundness of GL ($\mathrm{GL}⊢A⟹\mathrm{PA}⊢A^{\ast }$)

Map propositional letters to arithmetic sentences, map falsity to a refutable sentence, commute with implication and interpret $\square$ by an arithmetical provability predicate. Propositional axioms remain theorems. The K axiom uses the second of the derivability conditions, and the Löb axiom uses the Internal form of Löb's theorem. Modus ponens rule is preserved directly, and the necessitation rule uses the first derivability condition. Induction on a GL proof therefore proves the displayed soundness implication for Peano arithmetic with the stipulated provability predicate.