This is a follow-up question from Proof predicate in PA and stronger system
Suppose that two theories $T_1$ and $T_2$ share the same language - thus only axioms differ such that $T_2$ is a stronger theory relative to $T_1$.
Do/can $T_1$ and $T_2$ share the same proof predicate $Proof(x,y)$ where $x$ is Godel encoding of proof of Godel decoding of $y$? If not, why would it be? From my understanding, $Proof$ predicate is really about decoding $x$ and $y$, demonstrating that $x$ follows the right rule of inference or deduction and arriving at Godel decoding of $y$. And adding axioms does not necessarily change rule of inference or deduction. Thus, it seems that proof predicate does not have to change.
You've argued that the non-"initial" steps in a proof don't depend on the ambient theory, but we also have to consider the "initial" steps: steps in a proof where a statement is asserted without previous justification within the proof itself. This is exactly where the ambient theory comes in.
Amongst the properties that (the thing coded by) $x$ must have, in order to be a proof of (the thing coded by) $y$ in a theory $T$, is that it can only use "axioms" which are actually axioms of $T$. (This is actually an inference rule: in a proof from $T$, we can at any point assert any of the axioms of $T$.) In particular, the sequence $\langle\varphi\rangle$ is a proof of $\varphi$ from $T$ iff $\varphi\in T$ (EDIT: or $\varphi$ is a logical axiom). So any two different sets of axioms have different proof predicates. For example, "$\langle \forall x(S(x)\not=0)\rangle$" is a valid proof of $\forall x(S(x)\not=0)$ from the axioms of Peano arithmetic, but not from, say, the theory $\{\forall x(S(x)=x)\}$.
Of course, if $T$ is a theory and $\varphi$ is a theorem of $T$, then for some $\psi_1,...,\psi_n\in T$ we have $\emptyset\vdash (\psi_1\wedge...\wedge\psi_n)\implies\varphi$, so in a sense all proof predicates reduce to the proof predicate for the empty theory. But that's not what you asked