= Arithmetical soundness of GL
{c}
{title2=$\mathrm{GL}\vdash A\Longrightarrow\operatorname{PA}\vdash A^*$}
Map propositional letters to arithmetic sentences, map falsity to a refutable sentence, commute with implication and interpret $\Box$ 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.
Back to article page
