The omega-rule interpretation of transfinite provability logic

In this paper we will formalize such iterations of ω-rules in second-order arithmetic and show how it is a special case of what we call uniform provability predicates. Uniform provability predicates are similar to Ignatiev's strong provability predicates except that they can be iterated transfinitely. Finally, we show that GLPΛ is sound and complete for any uniform provability predicate.