The omega-rule interpretation of transfinite provability logic (Q1694812)

For any linear order $\Lambda$, the polymodal provability logic $\mathsf{GLP}_\Lambda$ (generalizing the logic $\mathsf{GLP}_\omega$ introduced by Japaridze) has modal operators $[\xi]$ for each $\xi\in\Lambda$, representing a chain of provability operators of increasing strength. Japaridze's logic has various arithmetical interpretations in the literature: for example, for subsystems of first-order arithmetic, $[n]\phi$ may be interpreted as $n$-times iterated $\omega$-provability, or provability relative to the set of true $\Pi_n$ sentences. The latter was exploited by \textit{L. D. Beklemishev} [Ann. Pure Appl. Logic 128, No. 1--3, 103--123 (2004; Zbl 1048.03045)] to give a modal logic proof of the ordinal analysis of PA in terms of $\varepsilon_0$. \par This paper investigates the interpretation of $\mathsf{GLP}_\Lambda$ for a recursive well-order $\Lambda$ in systems of a second-order arithmetic $T$, where $[\xi]\phi$ denotes provability from $T$ using the $\omega$-rule with nesting depth at most $\xi$. It is shown that $\mathsf{GLP}_\Lambda$ is sound and complete under this interpretation for theories $T\supseteq\mathrm{ACA}_0$ meeting certain conditions, and more generally, that the same holds for any so-called $\Lambda$-uniform proof predicate for $T$. In particular, the authors include a self-contained, relatively simple Solovay-style arithmetical completeness proof for $\mathsf{GLP}_\Lambda$. The paper is intended as a groundwork for a possible future ordinal analysis of subsystems of second-order arithmetic in the spirit of Beklemishev's method.