La teoría de conjuntos de Tarski-Grothendieck ( TG , llamada así por los matemáticos Alfred Tarski y Alexander Grothendieck ) es una teoría de conjuntos axiomática . Es una extensión no conservadora de la teoría de conjuntos de Zermelo-Fraenkel (ZFC) y se distingue de otras teorías de conjuntos axiomáticos por la inclusión del axioma de Tarski , que establece que para cada conjunto hay un universo de Grothendieck al que pertenece (ver más abajo). El axioma de Tarski implica la existencia de cardenales inaccesibles , lo que proporciona una ontología más rica que la de las teorías de conjuntos convencionales como ZFC. Por ejemplo, agregar este axioma apoyateoría de categorías .
El sistema Mizar y Metamath utilizan la teoría de conjuntos de Tarski-Grothendieck para la verificación formal de las pruebas .
Axiomas
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 , definiciones y notación de Mizar para describirlo. Los objetos y procesos básicos de Mizar son completamente formales ; se describen informalmente a continuación. Primero, supongamos que:
- Dado cualquier conjunto , el singleton existe.
- Dados dos conjuntos cualesquiera, existen sus pares ordenados y desordenados.
- Dado cualquier conjunto de conjuntos, existe su unión.
TG incluye los siguientes axiomas, que son convencionales porque también forman parte de ZFC :
- Establecer axioma: las variables cuantificadas se extienden sobre conjuntos solamente; 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 : deje que el dominio de la clase funcione ser el set . Entonces el rango de (los valores de para todos los miembros de ) también es un conjunto.
Es el axioma de Tarski lo 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 de poderes . [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 teorías de conjuntos convencionales como ZFC .
- Axioma de Tarski (adaptado de Tarski 1939 [5] ). Para cada set, existe un conjunto cuyos miembros incluyen:
- sí mismo;
- cada subconjunto de cada miembro de ;
- el conjunto de poder de cada miembro de ;
- cada subconjunto de de cardinalidad menor que la de.
Más formalmente:
dónde ""Denota la clase de potencia de xy "”Denota equinumerosidad . Lo que dice el axioma de Tarski (en la lengua vernácula) es que para cada conjuntohay un universo Grothendieck al que pertenece.
Que se parece mucho a un "conjunto universal" para - no solo tiene como miembros el poder de , y todos los subconjuntos de , también tiene el conjunto de poderes de ese conjunto de poderes y así sucesivamente: sus miembros están cerrados bajo las operaciones de tomar conjunto de poderes 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 de Grothendieck garantizado al que pertenece. Y luego cualquiera de esoses en sí mismo un miembro de un "conjunto casi universal" aún mayor y así sucesivamente. Es uno de los axiomas de cardinalidad fuerte que garantiza muchos más conjuntos de los que normalmente se supone que existen.
Implementación en el sistema Mizar
El lenguaje Mizar, subyacente a la implementación de TG y proporcionando su sintaxis lógica, se escribe y se supone que los tipos no están vacíos. Por tanto, la teoría se considera implícitamente no vacía . Los axiomas de existencia, por ejemplo, la existencia del par desordenado, también se implementa indirectamente mediante la definición de constructores de términos.
El sistema incluye 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.;
- Par ordenado : El conjunto;
- Subconjunto : un conjunto cuyos miembros son miembros de otro conjunto dado;
- La unión de un conjunto de conjuntos: El conjunto de todos los miembros de cualquier miembro de .
Implementación en Metamath
El sistema Metamath admite lógicas arbitrarias de orden superior, pero normalmente se utiliza con las definiciones de axiomas "set.mm". El axioma axi-groth agrega 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)))
Ver también
Notas
- ↑ Tarski (1938)
- ^ http://mmlquery.mizar.org/mml/current/wellord2.html#T26
- ^ Robert Solovay, Re: AC y cardenales fuertemente inaccesibles .
- ^ Metamath grothpw .
- ↑ Tarski (1939)
Referencias
- Andreas Blass , IM Dimitriou y Benedikt Löwe (2007) " Cardenales inaccesibles sin el axioma de la elección ", Fundamenta Mathematicae 194: 179-89.
- Bourbaki, Nicolas (1972). "Univers" . En Michael Artin ; Alexandre 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 (Lecture Notes in Mathematics 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 de conjuntos axiomáticos . Van Nostrand. Reimpresión de Dover, 1972.
- Tarski, Alfred (1938). "Über unerreichbare Kardinalzahlen" (PDF) . Fundamenta Mathematicae . 30 : 68–89.
- Tarski, Alfred (1939). "En los subconjuntos bien ordenados de cualquier conjunto" (PDF) . Fundamenta Mathematicae . 32 : 176-183.
enlaces externos
- Trybulec, Andrzej, 1989, " Teoría de conjuntos de Tarski-Grothendieck ", Revista de matemáticas formalizadas .
- Metamath : " Página de inicio del Explorador de pruebas " . Desplácese hacia abajo hasta "El axioma de Grothendieck".
- PlanetMath : " Axioma de Tarski "