Strengthening of Shoenfield's result on the recursive omega-rule

Question

It is trivial to show that Peano artithmetic ($\mathsf{PA}$) supplemented with the $\omega$-rule is complete. Joseph Shoenfield (`On a Restricted $\omega$-Rule', Bull. Acad. Polon. Sci. 7 (1959): 405–7) showed that this is true even if we replace the $\omega$-rule with the recursive $\omega$-rule; i.e., we admit

$$\frac{\phi(\bar{0}), \phi(\bar{1}),\ldots}{\forall x \ \phi(x)}$$

only if there exists a recursive function enumerating the proofs of $\phi(\bar{0}), \phi(\bar{1}),\ldots$.

Is it known whether this result can be strengthened? E.g., is $\mathsf{PA}$ $+$ the primitive recursive $\omega$-rule complete? $\mathsf{PA}$ $+$ the Kalmár-elementary $\omega$-rule?

Answer 1

In short the answer is yes.

Let us consider Schütte-style proof of completeness of $\omega$-logic. This proof works as follows. For any sequent $\Gamma$ we define it's canonical (cut-free) pre-proof (i.e. possibly ill-founded proof tree that locally obeys the rules of $\omega$-logic). The general idea here is to define pre-proof, whose conclusion is $\Gamma$, so that each possible rule is applied at some point. Next we show that if there is an infinite path in the cannonical pre-proof of $\Gamma$ there is an infinite path, then $\Gamma$ is false. Henceforth a sequent $\Gamma$ is true in $\mathbb{N}$ iff the canonical pre-proof of $\Gamma$ is well-founded.

The usual construction of the canonical pre-proof is in fact Kalmar elementary. Moreover, it should be even polynomial.