Recientemente, he estado leyendo sobre la teoría de conjuntos de Tarski-Grothendieck y me ha impresionado su breve axiomatización, la inclusión de cardinales inaccesibles y la capacidad de respaldar la teoría de categorías sin las clases adecuadas. http://mizar.org/JFM/pdf/tarski.pdf .
Sin embargo, me confunde un poco su primer axioma, que establece que todo es un conjunto. Luego formula la extensionalidad al decir que dos conjuntos son iguales si tienen los mismos miembros, y el axioma de Tarski al decir que todo conjunto es miembro de un universo de Grothendieck. Esto me parece innecesariamente complejo. Usando la definición de un conjunto como una "clase que es miembro de una clase", ¿no serían las declaraciones ∀ a ∀ b ( a = b ⇔ ∀ c ( c ∈ a ⇔ c ∈ b )) y ∀ a ∃ U ( a ∈ U ), donde Ues un universo de Grothendieck, demuestre que si un objeto no tiene miembros, sería el conjunto vacío, y que cualquier otra cosa, por supuesto, sería un conjunto, ya que tendría miembros y sería miembro de un universo de Grothendieck.
¿Estoy malinterpretando algo o hay alguna otra razón para usar el axioma de conjuntos?
Lo estás leyendo "mal". Solo aclaran el contexto, que todas las variables indican conjuntos, y no algunos objetos atómicos como si quisiera pensar en los números reales como "números" en lugar de conjuntos.
Tenga en cuenta que este es un documento breve relacionado con el sistema Mizar, que es un asistente de prueba. Dado que los asistentes de prueba están destinados a ser utilizados por matemáticos que pueden no suscribirse a la noción de que "todo es un conjunto", es una buena idea recordarles este hecho cuando sea relevante.
Desde una perspectiva fundamental teórica establecida, sí, nada es nuevo en esta actualización. ¿Para otras personas? Bueno, ese podría no ser el caso.
El artículo al que te refieres es el segundo de los dos artículos axiomáticos de la Biblioteca Matemática de Mizar . Como se describe en ese sitio:
Todos los demás textos se someten a la verificación de Mizar para ser consecuencias correctas de esos axiomas. El sistema Mizar ayuda al autor de un nuevo texto a preparar la terminología y los resultados disponibles, verifica las afirmaciones del texto y extrae hechos y definiciones para incluirlos en la biblioteca.
Entonces, el artículo al que se refirió ( TARSKI ) (tenga en cuenta que la versión que leyó fue un resumen escrito por humanos + una versión en látex del artículo escrito por humanos para el sistema Mizar, este último puede ser entendido por la máquina) fue escrito explícitamente como base para un estricto sistema de verificación computacional. Como tal, no puedes simplemente ser
Usar la definición de un conjunto como una "clase que es miembro de una clase"
porque eso no es sobre lo que está construido. Los axiomas, así como Mizar en general, están cubiertos en " Mizar in a Nutshell " por Adam Grabowski et al.
El otro de los dos artículos axiomáticos está literalmente OCULTO . Los conceptos lógicos importantes (p. ej.
&,
or,
not(para predicados) o non(para atributos),
implies,
iff,
for,
ex) están conectados directamente al software y la gramática del lenguaje Mizar, pero los modos explícitos (qué tipo de otra cosa puede ser algo, como un o un ) objecto setpredicados explícitos (decir que uno o varios algo(s) están en alguna relación con otro o no, como
x = y,
x <> yy
x in X) que básicamente la base para poder hablar de axiomas no se ha declarado implícitamente en el software, sino explícitamente en HIDDEN. simplemente son Y en base a eso, se podrían definir los axiomas en TARSKI desde el punto de vista de la programación. O como se pone en "Mizar en pocas palabras":
[OCULTO] documenta una parte de la axiomática de Mizar: muestra cómo se introducen las primitivas de la teoría de conjuntos en la biblioteca matemática de Mizar.
"Mizar in a Nutshell" repasa cada uno de los breves artículos axiomáticos. Afirma
[TARSKI] define los fundamentos axiomáticos de la teoría de conjuntos de Tarski-Grothendieck: axioma de extensionalidad [TARSKI:2] [...]
y continúa con el resto del artículo, afirmando implícitamente que TARSKI:1 ("todo es un conjunto") no es directamente parte de los axiomas TG, sino simplemente parte de la axiomática de Mizar. De hecho, uno podría haber dejado los objetos fuera de toda la axiomatización y, a veces, me pregunto si eso no hubiera sido mejor, o simplemente introducir "objeto" como una notación diferente de conjunto, pero al final, básicamente equivale a lo mismo. cosa, pero mejora mucho la legibilidad, dependiendo de que un autor quiera enfatizar si cierta "cosa" es una objecto más bien una set(que, por ejemplo, puede estar emptyo estar en el lado derecho de una in).
Si te interesa, el conjunto vacío se deriva de estos axiomas aquí .
Primero, debe consultar https://en.wikipedia.org/wiki/Tarski%E2%80%93Grothendieck_set_theory para ver los axiomas en TG. Están escritos en lenguaje estándar/lógico. Puede ver que no hay un axioma establecido. En segundo lugar, la referencia que citó comienza con el axioma 2 y una nota al pie dice que el axioma 1 (el axioma conjunto que le molesta) ha sido eliminado. Debes haberlo leído en otro periódico/más antiguo. Esta es una traducción en lenguaje legible por máquina de los axiomas que se encuentran en Wikipedia. Obviamente, si todo lo que puede cuantificar se llama "conjunto", entonces ya no tiene sentido escribir/verificar esto (el predicado conjunto (x) siempre es verdadero).
hanul jeon
malicia vidrina
DanielWainfleet
Tomás Antón