show/hide this revision's text 3 added 963 characters in body

The anwer is Yes.

Goodstein's theorem asserts that for every natural number $n$ the Goodstein sequence starting with $n$ eventually terminates. Thus, it can be stated in the form $\forall n\ \exists m\ \varphi(n,m)$, where $\varphi$ has only bounded quantifiers.

I claim that any true statement of this form is provable in PA+COR. To see this, note that for any particular fixed $n$ there is an $m$ such that $\varphi(n,m)$, since the statement was assumed to be true, and so for each $n$ the statement $\exists m\ \varphi(n,m)$ is provable in PA. Furthermore, the map $n\mapsto p_n$, where $p_n$ is th shortest PA proof of $\exists m\ \varphi(n,m)$ is a computable function. According to the article to which Kristal links, this is what is needed in order to deduce by COR that $\forall n\ \exists m\ \varphi(n,m)$, as desired.

As François mentioned in the comments, the way you have described your rule, it sounds more like the ordinary $\omega$-rule. The difference is whether the $\omega$-sequence of proofs of the instances is effective or not. According to the article in Kristal's answer, you find (on page 1) that the sequence of proofs must be given by a computable procedure. For the purpose of Goodstein's theorem, we were able to attain this. But it turns out not to matter, since the article mentions that Shoenfield proved that PA+$\omega$-rule is the same as PA+ recursively restricted $\omega$-rule. The article also mentions that a weakend form with primitive recursive proof enumerations is also complete (Nelsen), since one may use a padding trick to reduce to the computable case.

Edit. You have changed or updated the formal system to insist that the effective enumeration of proofs also be provably total (provable in P+COR). Although this seems like a more severe requirement, I claim it does not change anything, provided that you have the copy proof element mentioned in the context of Nelson's theorem in the article linked to by Kristal. In that article, it is claimed that insisting on primitive recursive enumerations of proofs is fully complete, equivalent to the full $\omega$-rule. The proof evidently uses a padding trick of some kind (and I have not looked at the details). I take this to mean that any statement provable in PA with the full $\omega$-rule is provable in PA+ primitive recursive COR. Since primitive recursive functions are provable total in PA, this would seem to satisfy your additional requirement. Thus, it seems still to be the case that Goodstein's theorem is provable in your version of PA+COR.
show/hide this revision's text 2 deleted 8 characters in body

The anwer is Yes.

Goodstein's theorem asserts that for every natural number $n$ the Goodstein sequence starting with $n$ eventually terminates. Thus, it can be stated in the form $\forall n\ \exists m\ \varphi(n,m)$, where $\varphi$ has only bounded quantifiers.

I claim that any true statement of this form is provable in PA+COR. To see this, note that for any particular fixed $n$ there is an $m$ such that $\varphi(n,m)$, since the statement was assumed to be true, and so for each $n$ the statement $\exists m\ \varphi(n,m)$ is provable in PA. Furthermore, the map $n\mapsto p_n$, where $p_n$ is th shortest PA proof of $\exists m\ \varphi(n,m)$ is a computable function. According to the article inked to in Kristal's answerwhich Kristal links, this is what is needed in order to deduce by COR that $\forall n\ \exists m\ \varphi(n,m)$, as desired.

As François mentioned in the comments, the way you have described your rule, it sounds more like the ordinary $\omega$-rule. The difference is whether the $\omega$-sequence of proofs of the instances is effective or not. If you follow According to the link article in Kristal's answer, you find (on page 1) that the sequence of proofs must be given by a computable procedure. But actually, for For the purpose of Goodstein's theorem, we were able to attain this. But it turns out that this difference does not to matter. In fact, since the article mentions that Shoenfield proved that PA+$\omega$-rule is the same as PA+ recursively restricted $\omega$-rule. The article also mentions that a weakend form with primitive recursive proof enumerations is also complete (Nelsen), since one may use a padding trick to reduce to the computable case.

show/hide this revision's text 1

The anwer is Yes.

Goodstein's theorem asserts that for every natural number $n$ the Goodstein sequence starting with $n$ eventually terminates. Thus, it can be stated in the form $\forall n\ \exists m\ \varphi(n,m)$, where $\varphi$ has only bounded quantifiers.

I claim that any true statement of this form is provable in PA+COR. To see this, note that for any particular fixed $n$ there is an $m$ such that $\varphi(n,m)$, since the statement was assumed to be true, and so for each $n$ the statement $\exists m\ \varphi(n,m)$ is provable in PA. Furthermore, the map $n\mapsto p_n$, where $p_n$ is th shortest proof of $\exists m\ \varphi(n,m)$ is a computable function. According to the article inked to in Kristal's answer, this is what is needed in order to deduce by COR that $\forall n\ \exists m\ \varphi(n,m)$, as desired.

As François mentioned in the comments, the way you have described your rule, it sounds more like the ordinary $\omega$-rule. The difference is whether the $\omega$-sequence of proofs of the instances is effective or not. If you follow the link in Kristal's answer, you find (on page 1) that the sequence of proofs must be given by a computable procedure. But actually, for the purpose of Goodstein's theorem, it turns out that this difference does not matter. In fact, the article mentions that Shoenfield proved that PA+$\omega$-rule is the same as PA+ recursively restricted $\omega$-rule. The article also mentions that a weakend form with primitive recursive proof enumerations is also complete (Nelsen), since one may use a padding trick to reduce to the computable case.