The many faces of omega-logic

TL;DR

This paper explores multiple formalizations of omega-logic within second-order arithmetic, analyzing their provability relations and reflection principles, and characterizes certain reverse mathematics systems using a new fixed-point formalization.

Contribution

It introduces a novel fixed-point formalization of omega-logic and establishes new equivalences and characterizations within reverse mathematics.

Findings

Characterization of $ ext{Pi}^1_1$-${ m CA}_0$ via fixed-point omega-logic

Analysis of provability relations among formalizations in reverse mathematics

Survey of reflection principles related to omega-logic

Abstract

We consider several formalizations in the language of second-order arithmetic of "The formula $\phi$ is a theorem of $\omega$-logic", including some which have been studied in the literature and a new variant defined via a least fixed point. We analyze the provability of relations between these different formalizations in standard theories of reverse mathematics. With this, we study the strength of various reflection principles arising from these notions of provability, surveying known results and establishing some new equivalences, including a characterization of $\Pi^1_1$-${\sf CA}_0$ in terms of our fixed-point formalization of $\omega$-logic.