Ordinals in constructive mathematics ? (references)

Question

I'm looking for references presenting a constructive treatment of the theory of ordinals. By constructive I mean valid in the internal logic of a topos (so no axiom of choice and no law of excluded middle).

I can easily guess that there are several non-equivalent approaches to this question: for example it makes sense to define ordinal as being well ordered sets as such do exist internally in toposes (For example the Higgs object) but this would mean that the natural number object when it exist is not an ordinal.

For this reasons I will clarify a bit what kind of properties I want on ordinals:

• The natural number object should be an ordinal.

• I want to be able to do proof by induction over ordinals and induction over the natural number object should be a special case of ordinal indcution.

• In the topos of sheaf over a topological space $X$ ordinals should be described the following way: For every (classical) ordinal $\alpha$, one can define the sheaf $F_{\alpha}$ over $X$ of (local) continuous functions from $X$ to $\alpha$ (I guess with the order topology on $\alpha$, although I'm open to suggestion on that point). If $\alpha' > \alpha$ there is a canonical inclusion $F_\alpha \hookrightarrow F_{\alpha'}$ and one can define $\operatorname{Ord}_X$ as the (large) sheaf obtain as the union of all the $F_\alpha$. Ordinals over $X$ should corresponds to sections of this large sheaf $\operatorname{Ord}_X$.

• One should be able to pullback ordinal along geometric morphisms (although it might not be exactly a pullback of sheaf), and if $f$ is a bounded geometric morphism there should be an operation of pushforward of ordinals, right adjoint to the pullback for the order relation.

• Maybe ordinal of the effective topos are related to recursive ordinal ? (this is suggested by the look of the NNO of the effective topos, but this last one is just a guess)

I'm relatively convince that such a notion exists, and the third point can be used to answer any question that one might have about the properties ordinals should have (at least for the "geometric" properties): For example, it should not be expected that ordinals are totaly ordered, but any two ordinals should have a supremum (because the function $\max(a,b)$ is continuous in the order topology but $\{a \leqslant b \}$ is not open in $\alpha \times \alpha$).

What I was wondering is if this kind of constructive theory of ordinals has been already developed and appears in the literature or not ?

Edit : It seems that the more restrictive notion of Ordinals among those that has been proposed in answer and comment is Paul Taylor notion of Plump ordinals (with an equivalent inductive-indutive definition in type theory given here ) but this definition seems already too weak for what I had in mind : one has the following Plump ordinals $0 = \emptyset$, $1 = \{ \emptyset \}$, $2 = \Omega$, $3 = \{$Initial segement of $\Omega \}$, $n = \{ $ Initial segment of $ n -1 \}$. And as any element of an ordinal is again ordinal there is already way too many of them to be describe by a geometric theory as I mentioned in my third point (the elements of $3$ are already non geometric). SO there must be a more restrictive notion but it seems that no one has considered it yet...

Answer 1

Perhaps the literature on W-types is what you are looking for? This is well-developed categorically and gives a good theory of inductive types.

If you are looking explicitly for ordinals, there's a recent discussion about ordinals in HoTT. @paul-taylor has worked on this. Since he is a regular here, I'll just provide the references. JSL paper and the section in his book.

Answer 2

If you want proof by induction, then you do want to use well-ordered sets, but you need the correct definition of ‘well-ordered’. Of course we can't require that any non-empty subset have a minimal element; then Excluded Middle follows. But requiring any inhabited subset to have a minimal element is still too strong. Requiring a total order is also too strong (although at least the natural numbers have that). Instead, we define a well order on a set $ X $ to be a binary relation $ \prec $ that is transitive, extensional, and well-founded (and define ‘well-founded’ to mean that induction works, not anything about minimal elements).

You know what transitivity means: if $ x \prec y \prec z $, then $ x \prec z $. It will follow from well-foundedness that the relation is irreflexive, so we have a (strict) partial order (sometimes called a quasi-order).

Extensionality is complicated to define in general, but since $ \prec $ is well-founded, it's enough to require weak extensionality: if for each $ t $ in $ X $, $ t \prec x $ iff $ t \prec y $, then $ x = y $.

(From this, using well-foundedness below, you can prove strong extensionality: if for every $ \prec $-bisimulation $ \sim $ on $ X $, if $ x \sim y $, then $ x = y $. Here, a $ \prec $-bisimulation is a relation $ \sim $ such that: if $ x \sim y $, then for each $ s $ in $ X $, if $ s \prec x $, then for some $ t $ in $ X $, $ t \prec y $ and $ s \sim t $; and if $ x \sim y $, then for each $ t $ in $ X $, if $ t \prec y $, then for some $ s $ in $ X $, $ s \prec x $ and $ s \sim t $.)

Finally, well-foundedness means that for each subset $ S $ of $ X $, if $ S $ is $ \prec $-inductive, then $ S = X $. Here, $ S $ is $ \prec $-inductive if, for each $ x $ in $ X $, if (for each $ t $ in $ X $, if $ t \prec x $, then $ x \in S $), then $ x \in S $. So if $ S $ is the only inductive subset of $ X $, then you prove properties of $ X $ by induction on $ \prec $.

It's handy to say that $ t $ is a predecessor of $ x $ if $ t \prec x $. Then the definitions are easier to state in words:

• transitivity: a predecessor of a predecessor is a predecessor;
• weak extensionality: if two elements of $ X $ have the same predecessors, then they are equal;
• (bisimulation: if two elements are related, then each predecessor of either is related (in the same direction) to some predecessor of the other;)
• inductive subset: if every predecessor of $ x $ belongs, then so does $ x $ itself.

This stuff is on the nLab, which may not count as a reference since I mostly put it there. I got the ideas from Paul Taylor, and there are references to his work in the other answer, so that's probably what you want to look at. But note that the plump ordinals are only some of the ordinals by this definition; much less ‘plump’ sets like $ \{ 0 , 1 , 2 \} $ and $ \mathbb N $ are also ordinals (just not plump ones).

Answer 3

The first response to any question about "the" ordinals is what you want to do with them. Regrettably, that is most often to find the fixed point of some construction within some already-known object, even though Kazimierz Kuratowski explained eloquently, but unfortunately not persuasively, that this can usually be done using closure operators.

In situations, common in algebraic subjects, where not all (binary) joins are available, you need Dito Pataraia's 1997 (constructive) fixed point theorem, or rather my adaptation of it that I have discussed on MO. There was a classical argument, called the Bourbaki--Witt theorem but actually due to Ernst Zermelo in 1908, which should have been a fundamental part of the curriculum long ago.

If you are trying to construct something by transfinite iteration of functors that goes beyond the logic of a an elementary topos or Zermelo set theory then set theorists will say that you need the axiom-scheme of replacement. However, I made a proposal using fibred category theory in the final pages of my book that I intend to write up properly in the near future.

Proof theorists use ordinals and their arithmetic in a more combinatorial way. I don't currently understand that, but hope that my research programme will throw some light on it.

However, Simon Henry is an accomplished categorist and will want a genuinely categorical answer.

The motivation, as I see it, for re-formulating the structures of set theory categorically is that they provide partial models of the non-existent free algebra for the covariant powerset functor. It would be useful to generalise this to other functors and other ways of presenting mathematical structures such as type theories.

Experienced categorists know that a superior understanding of a topic is not obtained by wrapping an existing symbolic argument in a few diagrams. That means that Homotopy Type Theory is not going to throw any more light on the subject than set theory does.

Starting from the beginning, Gerhard Osius represented any binary relation $(X,\prec)$ as a coalgebra $\alpha:X\to{\mathcal P} X$ for the powerset functor, with $$ \alpha(x) \;=\; \{y|y\prec x\} \quad\mbox{or}\quad y\prec x\iff y\in\alpha(x). $$ Then $(\prec)$ is extensional iff $\alpha$ is mono and we can also define well-foundedness and recursion for coalgebras.

In my book, I generalised this to functors that preserve inverse images and relaxed this to just preserving monos in my recent Well Founded Coalgebras and Recursion.

This is where we can start making serious use of categorical tools, in particular replacing "monos" with a factorisation system.

That paper examined what was required of the category and factorisation system to do this. Ordinals as Coalgebras is a worked example in which we replace the powerset with the poset ${\mathcal D}(X)$ of lower subsets and three different factorisation systems are considered. I wrote the Introduction of this paper this week and posted a version that is not exactly finished but more-or-less all there on my website.

The best behaved notion of ordinal, from a categorist's point of view, is the plump one. The categorical definition is that the coalgebra $\alpha$ is well founded and embeds $X$ as a lower subset of ${\mathcal D}(X)$. This means that every lower subset of $\alpha(x)\subset X$ with respect to the poset order is $\alpha(y)$ for some $y\leq x\in X$. This is much simpler than the recursive symbolic definition that I gave in Intuitionistic Sets and Ordinals in JSL in 1996.

Yes, it is true that the plump ordinals are very plump, as I demonstrate in the final section of the recent paper.

However, that was not the point of the exercise. The reason for using category theory is that the techniques are transferable to other very different situations.

So, I invite Simon and others to think of some other categories, endofunctors and factorisation systems and reproduce my results in those.

As for Homotopy Type Theory, its purpose is also to generalise the equality relation, by analogy with geometric paths. If the object that you're studying is provably a "set" (in the HoTT sense), so its notion of equality is the naive one, then you're not exploiting this powerful intuition and just messing around with symbols. So I recommend to the HoTT people that they wait to see what comes out of my categorical approach, and then devise some radically new notion of homotopy-ordinal.

All of my own work mentioned above is on my website: http://www.paultaylor.eu/ordinals/