12
$\begingroup$

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 is 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 $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 $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 restricitve 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...

$\endgroup$
  • 2
    $\begingroup$ Did you look at the section on ordinals in Homotopy type theory? $\endgroup$ – Zhen Lin Jun 1 '15 at 15:29
  • $\begingroup$ I havn't, and I should have. It might be the answer I was looking for, but I need to think a little about it. $\endgroup$ – Simon Henry Jun 1 '15 at 15:37
  • 2
    $\begingroup$ There's a chapter on ordinals in Aczel and Rathjen's book draft on constructive set theory (section 9.4 in this version), but that's maybe not quite what you want. $\endgroup$ – aws Jun 1 '15 at 19:43
  • $\begingroup$ I reckon people in algebraic set theory have looked at this, but can't immediately find something, other than that projecteuclid.org/euclid.bsl/1231081369 mentions it can be done. $\endgroup$ – Chris Heunen Jun 1 '15 at 20:24
  • $\begingroup$ What theorem would you want to prove with ordinals that is not stated with ordinals? Maybe something about infinite abelian groups? It will probably be non-constructive. For good constructive theorems, one reasonable strategy on ordinals is to avoid them. $\endgroup$ – Matt F. Jun 11 '15 at 0:39
4
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Interesting. Paul Taylor's "Plump ordinals" seems to be exactly the ones I'm looking for, but I still need to think more about it. $\endgroup$ – Simon Henry Jun 2 '15 at 9:56
  • $\begingroup$ After more thought, Plump ordinals are not the ones, see the edit of the question. $\endgroup$ – Simon Henry Jun 10 '15 at 14:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.