Well-Ordering Principles in Proof Theory and Reverse Mathematics

Michael Rathjen ()
Additional contact information
Michael Rathjen: University of Leeds, Department of Pure Mathematics

Chapter Chapter 4 in Axiomatic Thinking II, 2022, pp 89-127 from Springer

Abstract: Abstract Several theorems about the equivalence of familiar theories of reverse mathematics with certain well-ordering principles have been proved by recursion-theoretic and combinatorial methods (Friedman, Marcone, Montalbán et al.) and with far-reaching results by proof-theoretic technology (Afshari, Freund, Girard, Rathjen, Thomson, Valencia Vizcaíno, Weiermann et al.), employing deduction search trees and cut elimination theorems in infinitary logics with ordinal bounds in the latter case. At type level 1, the well-ordering principles are of the form $$ \text { (*) } ``\text {if}\,X \text { is well-ordered then } \, f(X) \, \text { is well-ordered''} $$ (*) ` ` if X is well-ordered then f ( X ) is well-ordered'' where f is a standard proof-theoretic function from ordinals to ordinals (such f’s are always dilators). One aim of the paper is to present a general methodology underlying these results that enables one to construct omega-models of particular theories from $$(*)$$ ( ∗ ) and even $$\beta $$ β -models from the type 2 version of $$(*)$$ ( ∗ ) . As $$(*)$$ ( ∗ ) is of complexity $$\Pi ^1_2$$ Π 2 1 such a principle cannot characterize stronger comprehensions at the level of $$\Pi ^1_1$$ Π 1 1 -comprehension. This requires a higher order version of $$(*)$$ ( ∗ ) that employs ideas from ordinal representation systems with collapsing functions used in impredicative proof theory. The simplest one is the Bachmann construction. Relativizing the latter construction to any dilator f and asserting that this always yields a well-ordering turns out to be equivalent to $$\Pi ^1_1$$ Π 1 1 -comprehension. This result has been conjectured and a proof strategy adumbrated roughly 10 years ago, but a detailed proof has only been worked out in recent years.

Keywords: Infinite proof theory; Reverse mathematics; Ordinal analysis; Ordinal representation systems; Cut elimination; Dilators; $$\omega $$ ω -models; $$\beta $$ β -models (search for similar items in EconPapers)
Date: 2022
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-3-030-77799-9_4

Ordering information: This item can be ordered from
http://www.springer.com/9783030777999

DOI: 10.1007/978-3-030-77799-9_4

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().