Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

What is a useful definition of an ordinal in Grothendieck toposes. Useful in this context means that I would like to construct fixed points of monotone maps on complete lattices using iteration from $\bot$. Can this be done? I know one can prove that there exists the least fixed point by constructing it as the intersection of all the pre-fixed points.

To define the chains I presumably need some form of well-founded induction principle, but the definitions of ordinals that are classically equivalent turn out to not be equivalent intuitionistically, and I can't find a proper reference explaining the relationship among them.

Any references explaining these issues are also very welcome.

share|improve this question

2 Answers 2

In the homotopy type theory book, the following definition is used:

  • Given a binary relation $<$ on a set $A$, the set of accessible elements of $A$ is the smallest subset $X \subseteq A$ with the following property: if $a$ is an element of $A$ and for all $b < a$ we have $b \in X$, then $a \in X$ as well.
  • A binary relation on a set $A$ is well-founded if every element of $A$ is accessible.
  • An ordinal is a set with an extensional well-founded transitive binary relation.

This can be interpreted in any elementary topos in a straightforward way, but I do not know how useful ordinals are in the intuitionistic context.

share|improve this answer

In intuitionistic logic there are several different ways to define the notion of ordinal, depending on what property you want, and in general these notions are not equivalent. For a good description of these different definitions and their relations you can check out Paul Taylors Intuitionistic Sets and Ordinals

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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