Definición de ordinales en tópicos de Grothendieck

Question

¿Cuál es una definición útil de un ordinal en toposes de Grothendieck? Útil en este contexto significa que me gustaría construir puntos fijos de aplicaciones monótonas en retículos completos usando iteración desde $\bot$. ¿Se puede hacer esto? Sé que se puede demostrar que existe el punto fijo más pequeño construyéndolo como la intersección de todos los pre-puntos fijos.

Para definir las cadenas presumiblemente necesito algún tipo de principio de inducción bien fundado, pero las definiciones de ordinales que son clásicamente equivalentes resultan no ser equivalentes intuicionísticamente, y no puedo encontrar una referencia adecuada que explique la relación entre ellas.

Cualquier referencia que explique estos problemas también es muy bienvenida.

Answer 1

En el libro de teoría de tipos de homotopía, se utiliza la siguiente definición:

• Dada una relación binaria $<$ en un conjunto $A$, el conjunto de elementos accesibles de $A$ es el subconjunto más pequeño $X \subseteq A$ con la siguiente propiedad: si $a$ es un elemento de $A$ y para todo $b < a$ tenemos $b \in X$, entonces $a \in X$ también.
• Una relación binaria en un conjunto $A$ es bien fundada si cada elemento de $A$ es accesible.
• Un ordinal es un conjunto con una relación binaria transitiva bien fundada extensional.

Esto puede interpretarse de manera directa en cualquier topos elemental, pero no sé qué útiles son los ordinales en el contexto intuicionista.

Answer 2

En la lógica intuicionista hay varias formas distintas de definir la noción de ordinal, dependiendo de la propiedad que se desee, y en general estas nociones no son equivalentes. Para obtener una buena descripción de estas distintas definiciones y sus relaciones, puedes consultar el documento de Paul Taylor Conjuntos e Ordinales Intuicionistas