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.

  • 2
    $\begingroup$ 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. $\endgroup$ – spaceisdarkgreen Jul 21 '18 at 1:26

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

  • $\begingroup$ 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. $\endgroup$ – Henning Makholm Jul 21 '18 at 10:46
  • $\begingroup$ @HenningMakholm Bah, quite right; edited! $\endgroup$ – Noah Schweber Jul 21 '18 at 16:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.