I'm trying to solve the following question set by my professor:
Show that if $S$ is a definable set of sentences, and $Pr_S$ is an associated proof predicate, and $X$ and $Y$ are any formulae, then $PAE ⊢ (Pr_S(\#(X → Y)) → (Pr_S(\#(X)) → Pr_S(\#(Y))))$
When I say that $Pr_S$ is a proof predicate, we mean that $Pr_S(n)$ holds if and only if $n$ is the Gödel number of a formula provable from $S$; PAE is Peano Arithmetic with Exponentiation; and e.g. $\#(X)$ is the Gödel number of $X$.
I've just started a course on Gödel's incompleteness theorems and working with Gödel numbers etc is still very new!
My question, essentially, is whether I can answer this question by applying the deduction theorem for first order logic twice - to say that the result holds if and only if:
$$PAE, Pr_S(\#(X → Y)), Pr_S(\#(X)) ⊢ Pr_S(\#(Y))$$
and then solve by saying if there's a proof of X → Y and a proof of X, then there must be a proof of Y by concatenating those proof and applying modus ponens. This seems like it might be too simple, and I'm not 100% convinced that this constitutes a proof that Y is provable from S i.e. that $Pr_S(\#(Y))$ holds.
If I'm missing something, and there's a proper way to do this, I'd really appreciate it if someone could point me in the right direction (or, if it turns out that this is sufficient, some confirmation would be appreciated). Thanks in advance!