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?