Polymorphic Ordinal Notations

Abstract

We give an alternative presentation of the ordinal notation at the strength of ${\hat{I}}_1^1-C{A}_0$ which allows the "uncountable" notation $\hat{I}\text{c◯}$ 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 ${\hat{I}}_2^1-C{A}_0$.