¿Qué hace que la teoría de conjuntos de Tarski Grothendieck no esté vacía?

Estoy peleando con la teoría de conjuntos de Grothendieck desde hace algún tiempo. Este es el marco para el sistema de verificación de pruebas automatizado de Mizar y, por lo tanto, aquí también hay una versión formalizada de los axiomas , y aquí en el enlace "Contenido" que se proporciona en formato pdf.

Lo que quiero entender es cómo la teoría contiene conjuntos y luego dónde residen qué tipos de conjuntos.

La primera pregunta quedaría respondida si establecemos por qué la teoría contiene el conjunto vacío. leo los titulares

¿La existencia del conjunto vacío es un axioma de ZFC o no?

y

¿Cómo obtengo la existencia de un set en ZFC siguiendo a Jech?

Sin embargo, se ocupan de una teoría de conjuntos bastante diferente.

Ahora bien, si se estableciera el conjunto vacío, entonces supongo que la teoría garantiza la existencia de un universo de Grothendieck con muchas cosas buenas. De acuerdo, existe la afirmación en la página de Wikipedia de que el axioma de Tarski implica el axioma del infinito y la existencia de cualquier conjunto significaría que ganamos. Sin embargo, no puedo ver cómo esa formulación del axioma de Tarski

 reserve x,y,z,u,N,M,X,Y,Z for set;
 ...
 ex M st N in M &
 (for X,Y holds X in M & Y c= X implies Y in M) &
 (for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z) &
 (for X holds X c= M implies X,M are_equipotent or X in M);

nos permite generar incluso un axioma si el todo-quantor pasa por un dominio vacío.

Otro camino: si buscamos la primera aparición del conjunto vacío en la biblioteca matemática de Mizar, la encontraremos aquí justo después de que se establezca el esquema del axioma de separación. Al hacer clic en "prueba", nos permite ver cómo se usa el esquema para mostrar la existencia. Sucede que al final del siguiente artículo

http://en.wikipedia.org/wiki/Axiom_of_empty_set

se refieren exactamente a un procedimiento para obtener un conjunto del axioma de separación, sin embargo, leí esto y todavía no aclara las cosas. Y no hace falta decir que no existe el axioma "existe un conjunto tal..." en la biblioteca de Mizar.

Por último, puedo señalar que la definición o especificación del conjunto vacío

 definition
 func {} -> set means
 :: XBOOLE_0:def 1
 not ex x being set st x in it;

se hace introduciendo algo que denotan "funtor", pero no es un funtor en el sentido teórico de la categoría, creo que es un término constructor ya que también usan esto para definir el par en la página del axioma

  definition let y; func { y } means
  :: TARSKI:def 1
  x in it iff x = y;
  let z; func { y, z } means

Ni siquiera estoy seguro de si este es un axioma que garantiza la existencia del "funtor" o si es simplemente una construcción de notación.

Una nota más: leí este hilo SE y en la respuesta el cartel dice "A menudo se necesita verificar que alguna definición no dependa del universo en el que se lleva a cabo". Me pregunto, si estoy interesado en conjuntos para hacer topología y teoría de propabilidad, ¿esta desventaja nombrada será realmente una?

Respuestas (1)

Por lo general, se supone que las teorías axiomáticas de conjuntos utilizan la lógica clásica de primer orden como sustrato, y la lógica clásica de primer orden, tal como suele formalizarse implícitamente , requiere que el dominio del discurso no sea vacío.

Más técnicamente, si φ es cualquier fórmula lógica en el lenguaje que estamos considerando, entonces la lógica de primer orden prueba ∃ X ( φ ∨ ¬ φ ) utilizando axiomas y reglas puramente lógicos , sin necesidad de axiomas teóricos de conjuntos para ello. Por lo tanto, la existencia de algún conjunto no necesita convertirse en un axioma de la teoría; puede asumirse como una condición límite porque la teoría es una criatura de la lógica de primer orden.

Es posible formular una variante de la lógica de primer orden que no prueba cosas que son falsas en el dominio vacío del discurso, pero el costo de esto son reglas más complejas para razonar sobre cuantificadores, y lo único que nos compra es permitir un caso de esquina bastante poco interesante como modelo, que generalmente no se considera que valga la pena el precio.

Ciertamente, no tendría sentido hacer que la lógica misma sea más compleja solo para necesitar agregar un axioma explícito a nuestra teoría de conjuntos cuyo efecto es negar lo que acabamos de hacer.

Sin embargo, a menudo se siente que esto es un punto bastante sutil, por lo que para evitar confusiones, algunas introducciones pueden optar por incluir "algo existe" como un axioma explícito de todos modos; después de todo, esto no duele a menos que le demos un valor especial a tener un conjunto mínimo de axiomas, que generalmente no se puede lograr cuando hay esquemas de axiomas de todos modos.

Además, en teorías de conjuntos como ZF donde ya existe, por otras razones, uno o más axiomas con un ∃ como el cuantificador más externo, entonces se puede considerar que vale la pena señalar que esto nos permitiría demostrar que existe un conjunto, incluso si elegimos trabajar en un fondo lógico que no hace esto por sí mismo.

Si este "conjunto lógico" está ahí pero no puedo especificarlo por completo, ¿cómo puedo trabajar correctamente con él? Este conjunto no es el conjunto vacío, ¿verdad? Además, si veo este conjunto como el que genera el primer universo de Grothendieck a través del axioma de Tarski, ¿significa esto que tengo cosas extrañas en mi universo?
@NickKidman: Por lo general, una vez que sabes que algún conjunto A existe, podría fabricar el conjunto vacío a partir de él mediante un axioma de separación: { X ∈ A ∣ ( X ∈ X ) ∧ ( X ∉ X ) } existe y está vacío. Sin embargo, el artículo de Wikipedia al que se vincula no parece incluir un axioma de separación. Es posible que el artículo asuma una variación de Reemplazo que subsume la Separación, al permitir el uso de funcionales parciales .
La lista de axiomas en el artículo de Wikipedia me parece particularmente vaga, no hay forma de saber a partir de esa exposición qué pueden probar los axiomas.
Bueno, digo en mi mensaje inicial que la biblioteca incluye el esquema del axioma de separación. También publiqué el enlace a los axiomas del probador, creo que incluyen reemplazo. como "esquema Fraenkel".
@Nick: Sí, scheme Fraenkelincluye la Separación; producirá el conjunto vacío si P[x,y]se elige que sea una contradicción.
@HenningMakholm: No entiendo cómo puedo escribir la existencia usando el axioma de separación sin tener ningún conjunto a mano antes. Existe la subcadena " ∈ X "con cuantificado X en él, pero no tengo X para empezar. No tengo nada de qué separar algo. (Creo que ni siquiera sé a priori que el conjunto vacío es un subconjunto de cualquier conjunto, podría no importar de todos modos). También acabo de leer esta publicación de mathoverflow y también discuten sobre el conjunto vacío.
@NickKidman: Por supuesto, debe tener algo a mano antes de poder usar la separación. El punto de mi comentario fue que después de que la lógica de primer orden prueba que algo existe (y que algo debe ser implícito un conjunto porque todo lo que dice la teoría son conjuntos), puedes usar la Separación para llegar desde allí al conjunto vacío.
Vale, sí, lo tengo formalmente aquí en su wiki . El lenguaje subyacente de Mizar se escribe e implícitamente exigen que sus tipos no estén vacíos. Además, el "axioma de emparejamiento" y los otros dos posteriores en los artículos no son los axiomas reales, sino las consecuencias con las que comienzan a trabajar y es por eso que los establecen como definiciones.
Solo una adición con respecto a establecer la teoría de las teorías de primer orden para permitir universos de discurso vacíos: esta extensión se vuelve interesante, y de hecho crucial, tan pronto como nos interesamos en modelos que no están hechos de conjuntos, sino modelos en diferentes categorías. Por ejemplo, en la mayoría de los topos, la afirmación "todo conjunto está vacío o habitado" no es verdadera. Por lo tanto, al restringirnos a las definiciones clásicas, excluimos mucho más que el modelo vacío. También excluimos todos aquellos que no están vacíos, pero no están habitados. Clásicamente, esto no puede suceder, pero en la mayoría de los casos, sucede.
¿Qué hace que la teoría de conjuntos de Tarski Grothendieck no esté vacía?
RespuestasAquíPolítica de privacidad1y, 0v