Consistencia relativa de ETCS sobre la teoría de un bien-señaló topos con NSIN

Question

EDIT: estoy chocando esto, porque todavía soy curioso, y porque tengo un pariente resultado de consistencia sobre la teoría de un bien-señaló topos con NSIN, y me pregunto cuánto equipaje puedo guardar por no asumir CA en el modelo base (que no voy a usar AC en las pruebas).

Gödel bien conocido de la prueba de la implicación $Con(ZF) \Rightarrow Con(ZFC)$ utiliza la construcción del interior de la modelo $L$ en $ZF$ para obtener un modelo de $ZFC$ (y, de hecho, mucho más). Sin embargo, este tipo de construcción no es (inmediatamente) disponible en una categoría de la teoría de la aproximación a la teoría de conjuntos. En particular, dado un bien-señaló topos con NSIN, que es la teoría de ETCS menos el axioma de elección, me pregunto si hay alguna manera para construir un modelo de ETCS. En la cara de ella, no parece probable, ya que los objetos de los topos son bastante amorfo.

La única cosa que puedo pensar (es cierto que no he intentado muy duro) está pasando a un modelo de ZF a través de la pura conjuntos, la construcción de $L$, y luego tomar la categoría de conjuntos de $L$. Pero esto es algo insatisfactorio, ya que deja la comodidad de la esfera de las categorías y se dirige al material de la teoría de conjuntos. Así:

Hay una categoría de la teoría de la construcción de un modelo de ETCS de un bien-señaló topos con NSIN?

Answer 1

Confieso que no soy del todo claro cuál es la Pregunta requiere, mientras que muchos de los Comentarios que están más allá de mí, pero aquí es una construcción de la que usted puede no ser consciente, y que pueden arrojar algo de luz sobre los problemas.

Se basa en mi papel Intuitionistic Conjuntos y los números Ordinales, en el Diario de la Lógica Simbólica 61 (1996) 705-744, especialmente la Sección 3. Esto, a su vez construida sobre Categórico de la Teoría de conjuntos: una caracterización de la Categoría de Conjuntos por Gerhard Osius en el Diario de Pura y Aplicada Álgebra 4 (1974) 79-119.

Estamos trabajando en algunos primaria topos, cuyos objetos, voy a llamar a los transportistas con el fin de evitar la palabra conjunto.

Un modelo de un fragmento de la teoría de conjuntos es dado por un transportista $X$ equipada con una relación binaria $\epsilon$ que es conveniente considerar como un mapa de $\epsilon:X\to P X$ para el powerset. Es decir, es un coalgebra para la covariante powerset functor.

Decimos que $(X,\epsilon)$ es extensional si el mapa $\epsilon:X\to P X$ es mono (1-1).

La definición de cuando el coalgebra está bien fundada implica un retroceso diagrama y es dada en el papel.

A continuación, un conjunto es una extensional bien fundada coalgebra.

La aplicación de la covariante powerset functor a un conjunto da otra.

Entre dos conjuntos hay un coalgebra homomorphism, y es mono. Esto captura la inclusión en el conjunto de la teoría de la sensación.

La categoría de los conjuntos, por lo tanto es un preorden. Es un gran categoría en el mismo sentido que el familiar de categorías tales como la de los grupos en un topos son grandes.

Podemos ensayar las definiciones estándar de emparejamiento, funciones, etc a partir de la teoría de conjuntos utilizando conjuntos y demostrar que este preorder proporciona un modelo de los axiomas de Zermelo.

Números naturales (infinito) y el axioma de elección se heredan de topos si se dispone de ellos.

Como el axioma esquema de reemplazo, entendiendo ésta desde una perspectiva categórica fue uno de mis principales objetivos en este trabajo. Los comentarios en mi JSL papel son bastante ingenuo y debe ser descontada en favor de las personas en el final de mi libro, sin Embargo, tengo interés en otras cosas y nunca consideré a una conclusión satisfactoria.