The omega rule is an infinitary rule of logic which says that from $\phi(0),\phi(1),\phi(2),...$ you can infer $\forall n\phi(n)$. My question is, what is the theory $T$ obtained by adding the omega rule to the system $ACA_0$? And what relation does $T$ bear to stronger subsystems of second-order arithmetic than $ACA_0$?
Clearly $T$ proves more truths in the language of first-order arithmetic than $Z_2$ (second-order arithmetic) or any of its subsystems, since it proves them all. But if $Th$ denotes all the truths in the language of first-order arithmetic, does $Z_2+Th$ prove all the consequences of $T$? And if so is the same true of $ATR_0+Th$ and the like?