Abstract

We consider several formalizations in the language of second-order arithmetic of "The formula ϕϕ is a theorem of ωω-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 Π11Π^1_1-CA0{\sf CA}_0 in terms of our fixed-point formalization of ωω-logic.

Explore this paper’s authors, topics and related work.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Reviews 0

Write a reviewWrite

No reviews yet.

Discussion 0

Add a commentWrite

No comments yet.