Constructive Ordinal Exponentiation
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu

TL;DR
This paper investigates the limitations of constructive ordinal exponentiation, proposing two near-constructive definitions that preserve key algebraic properties and are mechanized in Agda within homotopy type theory.
Contribution
It demonstrates the impossibility of general constructive ordinal exponentiation and introduces two alternative definitions with proven algebraic properties.
Findings
Two definitions are equivalent when applicable
Algebraic laws and cancellation properties hold for the definitions
The constructions preserve decidability of the exponential
Abstract
Cantor's ordinal numbers, a powerful extension of the natural numbers, are a cornerstone of set theory. They can be used to reason about the termination of processes, prove the consistency of logical systems, and justify some of the core principles of modern programming language theory such as recursion. In classical mathematics, ordinal arithmetic is well-studied; constructively, where ordinals are taken to be transitive, extensional, and wellfounded orders on sets, addition and multiplication are well-known. We present a negative result showing that general constructive ordinal exponentiation is impossible, but we suggest two definitions that come close. The first definition is abstract and solely motivated by the expected equations; this works as long as the base of the exponential is positive. The second definition is based on decreasing lists and can be seen as a constructive…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHomotopy and Cohomology in Algebraic Topology · Advanced Topology and Set Theory · Mathematical and Theoretical Analysis
