Abstract: This talk is on my first-year project on developing a theory of ordinal decidability within HoTT, utilizing the structure of Brouwer ordinals to establish an infinite hierarchy of decidability notions. The framework is shown to be a coherent generalization of standard notions, as the initial levels of the hierarchy correspond to internal decidability and semidecidability. The larger limit ordinals are then used to provide a classification for propositions of greater logical complexity. We also investigate the closure properties of these new decidability classes under logical connectives, and the effect of countable choice on this hierarchy. This work has been formalized in Cubical Agda and is joint work with Nicolai Kraus, Tom de Jong, and Fredrik Nordvall Forsberg.

[slide]