Sistema de teoría matemática de conjuntos.
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áticas 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 , proporcionando 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 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.
![{\displaystyle A}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle \{A\}}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
- Dados dos conjuntos cualesquiera, existen sus pares ordenados y desordenados.
- Dado cualquier conjunto de conjuntos, su unión existe.
TG incluye los siguientes axiomas, que son convencionales porque también forman parte de ZFC :
- Axioma de conjuntos: las variables cuantificadas abarcan únicamente 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 membresía son imposibles.
- Esquema de axioma de sustitución : 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.
![{\displaystyle F}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle A}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle F}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle F(x)}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle x}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle A}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
Es el axioma de Tarski lo que distingue a TG de otras teorías axiomáticas de conjuntos. El axioma de Tarski también implica los axiomas de infinito , elección , [1] [2] y conjunto de potencias . [3] [4] También implica la existencia de cardinales inaccesibles , gracias a los cuales 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:
![{\displaystyle x}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle y}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
- sí mismo;![{\displaystyle x}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
- cada elemento de cada miembro de ;![{\displaystyle y}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
- cada subconjunto de cada miembro de ;![{\displaystyle y}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
- el conjunto de poderes de cada miembro de ;![{\displaystyle y}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
- cada subconjunto de de cardinalidad menor que el de .![{\displaystyle y}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle y}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
Más formalmente:
![{\displaystyle \forall x\exists y[x\in y\land \forall z\in y(z\subseteq y\land {\mathcal {P}}(z)\subseteq y\land {\mathcal {P} }(z)\in y)\land \forall z\in {\mathcal {P}}(y)(\neg (z\approx y)\to z\in y)]}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
donde " " denota la clase de potencia de x y " " denota equinumerosidad . Lo que establece el axioma de Tarski (en lengua vernácula) es que para cada conjunto existe un universo de Grothendieck al que pertenece.![{\displaystyle {\mathcal {P}}(x)}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle \aprox}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle x}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
Esto se parece mucho a un “conjunto universal” porque – no sólo tiene como miembros el conjunto de poderes de , y todos los subconjuntos de , sino que también tiene el conjunto de poderes de ese conjunto de poderes, etc. – sus miembros están cerrados bajo las operaciones de tomar el conjunto de poderes o tomar el conjunto de poderes. un subconjunto. Es como un “conjunto universal”, excepto que, por supuesto, no es miembro de sí mismo ni es un conjunto de todos los conjuntos. Ése es el universo Grothendieck garantizado al que pertenece. Y entonces cualquiera de ellos es en sí mismo miembro de un “conjunto casi universal” aún mayor, y así sucesivamente. Es uno de los fuertes axiomas de cardinalidad que garantiza muchos más conjuntos de los que normalmente se supone que existen.![{\displaystyle y}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle x}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle x}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle x}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle y}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
Implementación en el sistema Mizar
El lenguaje Mizar, que subyace a la implementación de TG y proporciona su sintaxis lógica, se escribe y se supone que los tipos no están vacíos. Por lo tanto, se considera 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 igualdad, el predicado de membresía y las siguientes definiciones estándar:
- Singleton : un conjunto con un miembro;
- Par desordenado : conjunto con dos miembros distintos. ;
![{\displaystyle \{a,b\}=\{b,a\}}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
- Par ordenado : El conjunto ;
![{\displaystyle \{\{a,b\},\{a\}\}=(a,b)\neq (b,a)}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
- 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 .
![{\displaystyle Y}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
![{\displaystyle Y}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
Implementación en Metamath
El sistema Metamath admite lógicas arbitrarias de orden superior, pero normalmente se usa con las definiciones de axiomas "set.mm". El axioma del crecimiento del hacha 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)
- ^ "WELLORD2: Teorema de Zermelo y axioma de elección. La correspondencia de relaciones de buen orden y números ordinales".
- ^ Robert Solovay, Re: AC y cardenales fuertemente inaccesibles.
- ^ Crecimiento de metamathpw.
- ^ Tarski (1939)
Referencias
- 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 de conjuntos axiomática . Van Nostrand. Reimpresión de 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) . Fundamentos Mathematicae . 32 : 176–183. doi :10.4064/fm-32-1-176-783.
enlaces externos
- 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"