The omega-rule interpretation of transfinite provability logic

TL;DR

This paper develops a formal interpretation of transfinite provability logics using the omega rule, establishing soundness and completeness, and explores reducing the base theory for broader applicability.

Contribution

It introduces a novel omega-rule-based interpretation for transfinite provability logic and formalizes it within second order number theory.

Findings

Soundness and completeness of the interpretation are proven.

The interpretation can be formalized in second order number theory.

The base theory can be lowered below RCA_0 for broader applicability.

Abstract

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.