Constructive Taboos for Ordinals
University of Strathclyde
Abstract: Ordinals are crucial for many constructions and proofs, such as the transfinite construction of free algebras. If we had a constructive theory of ordinals, we could hope to simply compute colimits and other infinite objects, rather than having to carefully construct them by hand. However in a constructive setting, different classical equivalent formulations of ordinals have widely different properties. I will survey a few different notions of ordinals in the context of homotopy type theory, and consider what is possible to do constructively with them. For ordinals defined "set-theoretically", most decidability properties will turn out to be equivalent to the law of excluded middle, whereas for a notion based on Kleene's O, most properties are equivalent to Bishop's Limited Principle of Omniscience instead -- a weaker principle, but still constructively challenging. This is joint work with Nicolai Kraus and Chuangjie Xu.