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

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

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 .

- sí mismo;

- cada elemento de cada miembro de ;

- cada subconjunto de cada miembro de ;

- el conjunto de poderes de cada miembro de ;

- cada subconjunto de de cardinalidad menor que el de .

Más formalmente:

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.

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.

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:

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

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

Referencias

enlaces externos