This posting is related to the answer to this question.
Lets extend the language of $\sf PA$ with a monadic symbol "$\vdash$", add to the formula formation rules, the rule:
- if $(\phi)$ is a sentence in the language of $\sf PA$, then $(\vdash \phi)$ is a formula.
Now add all of the usual axioms of $\sf PA$ with induction restricted to the language of $\sf PA$, i.e. doesn't use the symbol "$\vdash$".
To be noted is that $\vdash$ can occur in the logical axioms, so we for example have $\neg (\neg(\vdash A)) \iff (\vdash A)$, for any sentence $A$ in the language of $\sf PA$
Add the following axioms:
Axioms: if $A$ is an axiom [logical or extra-logical] of $\sf PA$, then: $$ \vdash A$$
Modus Ponens: Let $A;B$ be sentences in the language of $\sf PA$, then: $$ (\vdash A) \land (\vdash (A \to B)) \to (\vdash B)$$
Truth: if $A$ is a sentence in the language of $\sf PA$, then: $$ (\vdash A) \to A $$
/
Call this theory $\sf PA+ \vdash + T$, while $\sf PA +\vdash$ denotes the theory without the last axiom.
Here, this theory won't have any of its models satisfying "$ (\vdash A) $ for every sentence $A$". The addition of the last axiom would bar that.
What I've noticed is that if we add the sentence $\neg \rho$ (i.e. the negation of the Rosser sentence) as an axiom, then $\sf PA+ \vdash + T + \neg \rho$ would actually prove: $$(\neg \rho) \not\to (\vdash \rho)$$
And so, all models of $\sf PA+ \vdash + T+ \neg \rho$ would falsify the implication schema present in the prior posting for the instance of $\rho$. While with $\sf PA+ \vdash + \neg \rho $ it only says that $\neg \rho$ is provable and $(\vdash \rho)$ is not proved, so it fails to prove the instance of that implication for $\rho$, rather than manage to reject it. However, still $\sf PA+ \vdash + \neg \rho$ answered the question, because if $(\vdash \rho)$ is not provable, then adding $\neg (\vdash \rho)$ as an axiom is consistent, and in that theory the implication would be falsified, so it is one step short of this theory.
Seeing that, my question is:
Does $\sf PA+ \vdash + T$ have higher consistency strength than $\sf PA+ \vdash$?
Best Answer
No, both of these theories are equiconsistent with PA.
The reason is that given any model of PA, we may expand it to a model in the language with $\vdash$ by interpreting $\vdash\psi$ as true in the model exactly when PA proves $\psi$. That is, we interpret $\vdash\psi$ inside the model as being the same as provability in the metatheory. This fulfills all your axioms, including the truth axiom, since every theorem of PA is true in this model. And so every model of PA expands to a model of PA + $\vdash$ + T.
The argument shows that your theories are both conservative over PA for assertions in the language of arithmetic, which is a very strong way of being equiconsistent.
Because your theory does not have induction in the language with your symbol $\vdash$, what it does is simply copy the metatheoretic proofs over into the model. Every model of PA+$\vdash$ is simply a model of PA equipped with metatheoretic provability of some (possibly inconsistent) extension of PA. Every model of PA + $\vdash$ + T is a model $M$ of PA together with metatheoretic provability of some extension of PA that is true in $M$.