Constructive theory of ordinals

TL;DR

This paper develops a constructive theory of ordinals based solely on order relations, aligning with intuitionistic principles and avoiding classical disjunctions, while maintaining key properties of classical ordinals.

Contribution

It introduces a new constructive framework for ordinals using only order relations, extending Martin-Löf's ideas without relying on classical logic or computability assumptions.

Findings

Constructive ordinals satisfy key properties similar to classical ones.

The theory emphasizes the role of supremum operations in a constructive setting.

Classical logic addition recovers classical ordinals but reduces computability.

Abstract

In Chapter 3 of his Notes on constructive mathematics, Martin-L{\"o}f describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable ordinals. In fact, the Turing definition of computable functions is not needed from a constructive point of view. We give in this paper a constructive theory of ordinals that is similar to Martin-L{\"o}f's theory, but based only on the two relations "$x \leq y$" and "$x < y$", i.e., without considering sequents whose intuitive meaning is a classical disjunction. In our setting, the operation "supremum of ordinals" plays an important r\^ole through its interactions with the relations "$x \leq y$" and "$x < y$". This allows us to approach as much as we may the notion of linear order when the property "$\alpha \leq \beta$ or $\beta \leq \alpha$" is provable only within classical logic. Our aim is to give a formal definition corresponding to intuition, and to prove that our constructive ordinals satisfy constructively all desirable properties. Note that by adding classical logic, we would recover the ordinals of usual classical mathematics, at the cost of a loss of computability for most statements given in the usual form.