Does strong provability imply syntactical provability?

Question

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 formula, 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$".

Add the following axioms:

Axioms: if $A$ is an axiom 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)$$

Now, define the notion of strong provability as:

$S$ is strongly provable in $\sf PA$ if and only if there is a Gödel code of its proof in $\sf PA$ that is strictly smaller than any Gödel code of a proof of its negation in $\sf PA$

Formally:

$ S \text { is strongly provable in } {\sf PA} \iff \\ \exists x: \operatorname {Proof}_{\sf PA} (x, \ulcorner S \urcorner ) \land \\ \forall y (\operatorname {Proof}_{\sf PA} (y, \operatorname {neg}(\ulcorner S \urcorner)) \to x < y ) $

To explain the terminology: those are the same as the Gödel-Rosser terminology (see here). Notice here that the whole of the above sentence is written in the pure language of $\sf PA$, in particular it doesn't use the symbol "$\vdash$" whatsoever.

Question:

Assuming $\sf PA$ is consistent, is the following a theorem scheme of this theory?

• if $S$ is a sentence in the language of $\sf PA$, then: $$ (S \text{ is strongly provable in } {\sf PA}) \to (\vdash S)$$

I personally think it is not, since there are non-standard models of $\sf PA$. But, I'm not sure of whether the existence of such models would affect the truth of the above implication in this theory?

Answer 1

Let me assume that you also include the axioms $\vdash A$ whenever $A$ is a logical axiom, for some fixed standard proof system using modus ponens as the only inference rule. And let me also assume that we have induction in the language including $\vdash$.

It now follows easily by induction on proofs in that system that whenever $S$ is provable in PA, then your theory proves $\vdash S$.

Indeed, since the induction on proofs can be undertaken internally to the theory, we get that your theory proves the universal claim $$\forall S, \text{ if }S\text{ is provable in PA, then }\vdash S.$$

And since strong provability implies provability, the answer is yes, every instance of your implication is provable in your theory. (But I find strong provability to be a red herring here.)

If you don't include the logical axioms in your theory, then it will break this argument, but furthermore it would be questionable whether your theory in that case was expressing a useful concept about provability.

Answer 2

The negation of the Rosser sentence, that is $\neg \rho$, states that "the Rosser sentence $\rho$ is strongly provable in $\sf PA$". Now $\rho$ is not a theorem of $\sf PA$, neither is a theorem of this theory! (otherwise it will make this theory inconsistent for the same reasons it'll render $\sf PA$ inconsistent should it be a theorem of $\sf PA$)

So we can add $\neg \rho$ to the list of axioms of this theory, to get a consistent theory, call it $K$.

Now since $\neg \rho$ doesn't have the symbol $\vdash$ occurring in it, then all $(\vdash \phi)$ theorems of $K$ are those of the original theory, and precisely each $\phi$ must be a theorem of $\sf PA$.

Now $(\vdash \rho)$ is not a theorem of $K$, since $\rho$ is not a theorem of $\sf PA$. But $\neg \rho$ is a theorem of $K$, thus the implication is refuted in $K$ for the instance where $S$ is $\rho$.

Now, all models of $K$ are models of this theory, so this proves that the questioned implication scheme is NOT a theorem scheme of this theory, since it's not satisfied by all models of it.