# Would a proof predicate change if a stronger system used despite sharing language?

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.

• Yes it does change. Verifying a proof involves checking if certain statements are axioms or not. Thus if the axioms change, the verification procedure the proof predicate encodes changes, so the proof predicate changes. – spaceisdarkgreen Jul 21 '18 at 1:26

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
• Nitpick: $\left<\varphi\right>$ could also be a proof of $\varphi$ if $\varphi$ is an instance of a logical axiom in the proof system you're using. – Henning Makholm Jul 21 '18 at 10:46