Polymorphic Ordinal Notations
Henry Towsner · arXiv (Cornell University) · 2025
We give an alternative presentation of the ordinal notation at the strength of $Π^1_1-CA_0$ which allows the "uncountable" notation $Ω$ to be interpreted "polymorphically" - that is, we allow the notation to be interpreted as different cardinals depending on their context. This gives us a way to represent functions on ordinals within our ordinal notation system. We then use this idea to present an ordinal notation system for a system a bit weaker than parameter-free $Π^1_2-CA_0$.