Semi-recursive ω-rule I thought of the following semi-recursive ω-rule for a sequence of first-order theories $PA_k$ that extend $PA_0 = PA$:

Semi-recursive ω-rule: For each $1$-parameter arithmetical sentence $Q$, if (using the usual encoding) $PA_k \vdash \forall n ( PA_k \vdash Q(n) )$, then we add $∀n ( Q(n) )$ as an axiom of $PA_{k+1}$.

$PA_k$ clearly has a semi-recursive axiom set for each natural $k$, so it has a theorem generator and will still be arithmetically-incomplete by the generalized incompleteness theorems. Anyway if PA is sound then $PA_k$ would also be sound. My questions are:

(1) What is the strength of each $PA_k$ for natural $k$?
(2) What happens if I go further by defining $PA_ω = \bigcup_{k \in ω} PA_k$ and carry on iterating all the way up the computable ordinals?
(3) What if we start with ACA instead? In general, what happens to the strength of the system on applying this semi-recursive ω-rule?


Assuming $PA$ is sound, I cannot even think of a single sentence that $PA_1$ proves that $PA$ does not. So I am actually guessing that this rule is completely useless. Can anyone prove that $PA_1 = PA$ and $ACA_1 = ACA$? If not, does the hierarchy reach a fixed point?
 A: Below, all theories are "appropriate" - that is, they are recursively axiomatizable, consistent, and contain PA. Of course this last bit is overkill, but what the hey.
I can't give a full answer, but let me address your question as to whether $PA=PA_1$. The answer is no, and indeed the "semirecursive $\omega$-rule operator" has no nontrivial fixed points.
The key is the following fact: that PA is internally $\Sigma_1$-complete, that is, that PA proves "PA proves every true $\Sigma_1$ fact." See e.g. here. And of course this is hereditary upwards - all the theories we consider will share this property too. (Actually, we really only need $\Delta_0$-completeness, but meh.)
Internal $\Sigma_1$-completeness lets us make the following neat argument. Given an appropriate theory $S$, let $Q_S(x)$ be the formula "$x$ is not (the Godel number of) a proof of a contradiction in $S$." Then I claim that we have $$S\vdash\forall x(S\vdash Q_S(x)).$$ Consequently the "next step up" from $S$ according to your semi-recursive $\omega$-rule is at least (and indeed will wind up being much more than) $S+Con(S)$, since "$\forall x(Q_S(x))$" is just "$Con(S)$."
To see this, we reason inside $S$ as follows:

"Fix $n$; we need to show that $S$ proves '$n$ is not (the Godel number of) an $S$-proof of a contradiction.' There are two possibilities. Maybe $n$ is the Godel number of a proof of a contradiction in $S$, in which case $S$ is inconsistent and so we have $S\vdash Q_S(n)$ trivially. Otherwise, $n$ is not the Godel number of a proof of a contradiction in $S$, in which case we have $S\vdash Q_S(n)$ since 'not-being-a-proof-of' is $\Sigma_1$ (indeed, $\Delta_0$) and $S$ is $\Sigma_1$-complete. Either way, it must be the case that $S\vdash Q_S(n)$, regardless of $n$ - if only for stupid reasons!"

The fact that $S$ knows itself to be $\Sigma_1$-complete is what lets the "otherwise" case work.
