stringtranslate.com

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 .

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 , 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:

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

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 .

Más formalmente:

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.

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 normalmente se supone que existen.

Implementación en el sistema Mizar

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:

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 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)))

Véase también

Notas

  1. ^ Tarski (1938)
  2. ^ "WELLORD2: Teorema de Zermelo y axioma de elección. La correspondencia entre relaciones de buen orden y números ordinales".
  3. ^ Robert Solovay, Re: AC y cardenales fuertemente inaccesibles.
  4. ^ Metamath crecimiento.
  5. ^ Tarski (1939)

Referencias

Enlaces externos