Teoría de conjuntos de Tarski-Grothendieck

La teoría de conjuntos de Tarski-Grothendieck ( TG , llamada así por los matemáticos Alfred Tarski y Alexander Grothendieck ) es una teoría axiomática de conjuntos . Es una extensión no conservativa de la teoría de conjuntos de Zermelo-Fraenkel (ZFC) y se distingue de otras teorías axiomáticas de conjuntos por la inclusión del axioma de Tarski , que establece que para cada conjunto existe un universo de Grothendieck al que pertenece (ver más abajo). El axioma de Tarski implica la existencia de cardinales inaccesibles , lo que proporciona una ontología más rica que ZFC. Por ejemplo, agregar este axioma respalda la teoría de categorías .

El sistema Mizar y Metamath utilizan la teoría de conjuntos de Tarski-Grothendieck para la verificación formal de pruebas .

La teoría de conjuntos de Tarski-Grothendieck comienza con la teoría de conjuntos convencional de Zermelo-Fraenkel y luego agrega el “axioma de Tarski”. Usaremos los axiomas , las definiciones y la notación de Mizar para describirla. Los objetos y procesos básicos de Mizar son completamente formales ; se describen de manera informal a continuación. Primero, supongamos que:

• Dado cualquier conjunto , el singleton existe.${\estilo de visualización A}$${\estilo de visualización \{A\}}$
• Dados dos conjuntos cualesquiera, existen sus pares ordenados y no ordenados.
• Dado cualquier conjunto de conjuntos, existe su unión.

TG incluye los siguientes axiomas, que son convencionales porque también son parte de ZFC :

• Axioma de conjuntos: Las variables cuantificadas abarcan solo conjuntos; todo es un conjunto (la misma ontología que ZFC ).
• Axioma de extensionalidad : Dos conjuntos son idénticos si tienen los mismos miembros.
• Axioma de regularidad : Ningún conjunto es miembro de sí mismo y las cadenas circulares de pertenencia son imposibles.
• Esquema axiomático de reemplazo : Sea el dominio de la función de clase el conjunto . Entonces el rango de (los valores de para todos los miembros de ) también es un conjunto.${\estilo de visualización F}$${\estilo de visualización A}$${\estilo de visualización F}$${\estilo de visualización F(x)}$${\estilo de visualización x}$${\estilo de visualización A}$

Es el axioma de Tarski el que distingue a TG de otras teorías de conjuntos axiomáticos. El axioma de Tarski también implica los axiomas de infinito , elección , ^{[1] [2]} y conjunto potencia . ^{[3] [4]} También implica la existencia de cardinales inaccesibles , gracias a lo cual la ontología de TG es mucho más rica que la de las teorías de conjuntos convencionales como ZFC .

• Axioma de Tarski (adaptado de Tarski 1939 ^[5] ). Para cada conjunto , existe un conjunto cuyos miembros incluyen:${\estilo de visualización x}$${\estilo de visualización y}$
  • ${\estilo de visualización x}$sí mismo;
  • Cada elemento de cada miembro de ;${\estilo de visualización y}$
  • Cada subconjunto de cada miembro de ;${\estilo de visualización y}$
  • El conjunto de potencias de cada miembro de ;${\estilo de visualización y}$
  • Cada subconjunto de de cardinalidad menor que la de .${\estilo de visualización y}$${\estilo de visualización y}$

Más formalmente:

${\displaystyle \para todo x\existe y[x\en y\land \para todo z\en y(z\subseteq y\land {\mathcal {P}}(z)\subseteq y\land {\mathcal {P}}(z)\en y)\land \para todo z\en {\mathcal {P}}(y)(\neg (z\approx y)\to z\en y)]}$

donde “ ” denota la clase de potencia de x y “ ” denota equinumerosidad . Lo que el axioma de Tarski establece (en la jerga) es que para cada conjunto existe un universo de Grothendieck al que pertenece.${\displaystyle {\mathcal {P}}(x)}$${\displaystyle \aprox }$${\estilo de visualización x}$

Esto se parece mucho a un “conjunto universal” porque no solo tiene como miembros el conjunto potencia de , y todos los subconjuntos de , sino que también tiene el conjunto potencia de ese conjunto potencia, y así sucesivamente; sus miembros están cerrados bajo las operaciones de tomar el conjunto potencia o tomar un subconjunto. Es como un “conjunto universal”, excepto que, por supuesto, no es un miembro de sí mismo y no es un conjunto de todos los conjuntos. Ese es el universo garantizado de Grothendieck al que pertenece. Y entonces, cualquier conjunto de este tipo es en sí mismo un miembro de un “conjunto casi universal” aún más grande, y así sucesivamente. Es uno de los axiomas de cardinalidad fuerte que garantizan muchos más conjuntos de los que uno normalmente supone que existen.${\estilo de visualización y}$${\estilo de visualización x}$${\estilo de visualización x}$${\estilo de visualización x}$${\estilo de visualización y}$

El lenguaje Mizar, que sustenta la implementación de TG y proporciona su sintaxis lógica, está tipificado y se supone que los tipos no están vacíos. Por lo tanto, se supone implícitamente que la teoría no está vacía . Los axiomas de existencia, por ejemplo, la existencia del par desordenado, también se implementan indirectamente mediante la definición de constructores de términos.

El sistema incluye la igualdad, el predicado de pertenencia y las siguientes definiciones estándar:

• Singleton : Un conjunto con un miembro;
• Par desordenado : Un conjunto con dos miembros distintos. ;${\displaystyle \{a,b\}=\{b,a\}}$
• Par ordenado : El conjunto ;${\displaystyle \{\{a,b\},\{a\}\}=(a,b)\neq (b,a)}$
• Subconjunto : Un conjunto cuyos miembros son todos miembros de otro conjunto dado;
• La unión de un conjunto de conjuntos : El conjunto de todos los miembros de cualquier miembro de .${\estilo de visualización Y}$${\estilo de visualización Y}$

El sistema Metamath admite lógicas arbitrarias de orden superior, pero normalmente se utiliza con las definiciones de axiomas "set.mm". El axioma ax-groth añade el axioma de Tarski, que en Metamath se define de la siguiente manera:

⊢ ∃y(x ∈ y ∧ ∀z ∈ y (∀w(w ⊆ z → w ∈ y) ∧ ∃w ∈ y ∀v(v ⊆ z → v ∈ w)) ∧ ∀z(z ⊆ y → (z ≈ y ∨ z ∈ y)))

• Axioma de limitación de tamaño

• Andreas Blass , IM Dimitriou y Benedikt Löwe (2007) "Cardenales inaccesibles sin el axioma de elección", Fundamenta Mathematicae 194: 179-89.
• Bourbaki, Nicolás (1972). "Universo". En Michael Artín ; Alejandro Grothendieck ; Jean-Louis Verdier (eds.). Séminaire de Géométrie Algébrique du Bois Marie – 1963-64 – Théorie des topos et cohomologie étale des schémas – (SGA 4) – vol. 1 (Apuntes de clase de matemáticas 269 ) (en francés). Berlina; Nueva York: Springer-Verlag . págs. 185-217. Archivado desde el original el 26 de agosto de 2003.
• Patrick Suppes (1960) Teoría axiomática de conjuntos . Van Nostrand. Reimpresión en Dover, 1972.
• Tarski, Alfred (1938). "Über unerreichbare Kardinalzahlen" (PDF) . Fundamentos Mathematicae . 30 : 68–89. doi :10.4064/fm-30-1-68-89.
• Tarski, Alfred (1939). "Sobre los subconjuntos bien ordenados de cualquier conjunto" (PDF) . Fundamenta Mathematicae . 32 : 176–183. doi :10.4064/fm-32-1-176-783.

• Trybulec, Andrzej, 1989, "Teoría de conjuntos de Tarski-Grothendieck", Revista de matemáticas formalizadas .
• Metamath : "Página de inicio de Proof Explorer". Desplácese hacia abajo hasta "Axioma de Grothendieck".
• PlanetMath : "El axioma de Tarski"