Skip to main content
2 of 3
added 43 characters in body
Joel David Hamkins
  • 236.3k
  • 44
  • 777
  • 1.4k

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.

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.

Joel David Hamkins
  • 236.3k
  • 44
  • 777
  • 1.4k