I'm trying to show the above. We define interpretations as follows:
For any provability predicate $Pr(v_1)$, and $i$ any mapping from $\{ \bot, p_1, ..., p_n, ...\}$ (where $p_i$ are the sentence letters of GL) to sentences in the language of PA, we define an interpretation $\xi_i$ of GL in PA (Peano Aritmetic) wrt $i$ and $Pr(v_1)$ as:
$\xi_i (\bot) = i(\bot)$
$\xi_i (p_n) = i(p_n)$
$\xi_i ((X \supset Y)) = \xi_i (X)\supset \xi_i (Y)$
$\xi_i (\Box X) = Pr(\ulcorner \overline{\xi_i(X)}\urcorner)$
I think I'm struggling with understanding how PA and GL are related. I'm assuming for the proof I need to do a deduction in PA, but how do I 'convert' what we're given from GL?
Thanks!
GL is basically PA but with all the details "abstracted away", apart from propositional logic and the provability predicate. You can think of the sentence letters $p_i$ as standing for formulas in PA, but it doesn't really matter which ones. What this "Soundness" result tells us is that a proof in GL provides a template for proofs in PA, where we get the proof in PA by choosing a proof predicate to replace $\square$ and PA sentences to replace the $p_i$s.
Here's how the proof works: since we're given a proof in $\mathrm{GL}$, we'll proceed by induction on the length of that proof. What this means in practice is that we'll have to show that the axioms and rules of inference for $\mathrm{GL}$ still hold in PA, after interpreting them using $\xi_i$.
I'll give an example here. One of the axioms for GL is distribution: for any GL sentences $X$ and $Y$: $$\mathrm{GL} \vdash ( \square (X \supset Y) \supset (\square X \supset \square Y))$$ What we need to prove is: $$\mathrm{PA} \vdash \xi_i \big(\square (X \supset Y) \supset (\square X \supset \square Y)\big)$$ Using the rules for interpretations, this is the same as: $$\mathrm{PA} \vdash \big( Pr (\overline{ \ulcorner \xi_i(X) \supset \xi_i(Y) \urcorner}) \supset ( Pr (\overline{\ulcorner \xi_i(X) \urcorner} )\supset Pr(\overline{\ulcorner \xi_i(Y) \urcorner}) \big) $$ This is just an instance of $P_2$ in the definition of a proof predicate, so this holds.
All that remains is to do a similar proof for the remaining two axioms and the two rules of inference.