  In this paper we consider transfinite provability logics where for each
ordinal in some recursive well-order we have a corresponding modal provability
operator. The modality [xi] will be interpreted as "provable in ACA_0 together
with at most xi nested applications of the omega rule". We show how to
formalize this in in second order number theory. Next we prove both soundness
and completeness under this interpretation. We conclude by showing how one can
lower the base theory ACA_0 to theories below RCA_0.
