Teoria dos conjuntos de Tarski-Grothendieck

Predefinição:Mais notas A teoria dos conjuntos de Tarski-Grothendieck (TG, assim denominada em referência aos matemáticos Alfred Tarski e Alexander Grothendieck) é uma teoria dos conjuntos axiomática. Também é uma extensão não conservativa da teoria dos conjuntos de Zermelo-Fraenkel (ZFC) e pode ser distinguida de outras teorias dos conjuntos axiomáticas por causa da inclusão do axioma de Tarski, que diz que para cada conjunto existe um universo de Grothendieck a qual pertence. O axioma de Tarski implica na existência de cardinais inacessíveis, fornecendo uma ontologia mais rica do que outras teorias como a ZFC. Por exemplo, adicionar esse axioma dá suporte a teoria das categorias.

O sistema Mizar e Metamath usam a teoria dos conjuntos de Tarski-Grothendieck para verificação formal de provas.

Axiomas

A teoria dos conjuntos de Tarski-Grothendieck começa com a convencional teoria dos conjuntos de Zermelo-Fraenkel e depois adiciona o axioma de Tarski. Usaremos os axiomas, definições e notação de Mizar para descrevê-los. O processos e objetos básicos de Mizar são completamente formais, e são descrevidos informalmente abaixo. Primeiro, assumiremos que:

Dado um conjunto qualquer $A$, o conjunto unitário $\{A\}$ existe. Dados dois conjuntos quaisquer, seus pares ordenados e desordenados existem. Para quaisquer famílias de conjuntos, suas uniões existem.

TG utiliza os axiomas a seguir, que são convencionais, por fazerem parte da ZFC:

• Axioma dos conjuntos: Variáveis quantificadas variam apenas sobre conjuntos; tudo é um conjunto (a mesma ontologia da ZFC).
• Axioma da extensionalidade: Dois conjuntos são idênticos se tiverem os mesmos componentes.
• Axioma da regularidade: Nenhum conjunto é membro de si mesmo, e correntes circulares de filiação são impossíveis.
• Esquema axiomático da substituição: Seja o domínio da função $F$ o conjunto $A$. Então a imagem de $F$(os valores de $F(x)$ para qualquer $x$ pertencente a $A$) também é um conjunto.

É o axioma de Tarski que diferencia a TG das outras teorias dos conjuntos. Ele também implica os axiomas do infinito, escolha e o axioma da potência. Também implica a existência de cardinais inacessíveis, graças aos quais a ontologia da TG é muito mais rica do que a de outras teorias dos conjuntos, como a ZFC.

Axioma de Tarski (adaptado de Tarski 1939).

- Para todo conjunto $x$, existe um conjunto $y$ cujos membros incluem: - O conjunto $x$; - todo subconjunto de cada membro de $y$; - o conjunto das partes de cada membro de $y$; - cada subconjunto de $y$ com cardinalidade menor que $y$.

Mais formalmente:

$\mathrm{\forall }x\mathrm{\exists }y[x\in y\wedge \mathrm{\forall }z\in y(𝒫(z)\subseteq y\wedge 𝒫(z)\in y)\wedge \mathrm{\forall }z\in 𝒫(y)(\mathrm{\neg }z\approx y\to z\in y)]$

onde "$𝒫(x)$" denota a classe de x ,"$\approx$" denota a equipotência.O que o axioma de Tarski diz(no vernáculo), é que para cada conjunto $x$ existe um universo de Grothendieck para o qual ele pertence.

Implementação no sistema Mizar

A linguagem Mizar, usada na implementação da TG, e fornecendo sua sintaxe lógica é tipada e assume-se que os tipos não são vazios. Então, a teoria é implicita e não-vazia. Os axiomas de existência, por exemplo, a existência do par desordenado é implementado indiretamente pela definição dos construtores de termos. O sistema inclui a igualdade, predicados e as seguintes definições padrão:

• Conjunto unitário: Um conjunto com um elemento;
• Par desordenado: Um conjunto com dois elementos distintos.$\{a,b\}=\{b,a\}$;
• Par ordernado: O conjunto $\{\{a,b\},\{a\}\}=(a,b)\ne (b,a)$;
• Subconjunto: O conjunto cujos elementos também são elementos de outros conjuntos;
• União de uma família de conjuntos $Y$: O conjunto de todos os elementos de qualquer elemento de $Y$.

Implementação em Metamath

O sistema Metamath permite lógica de alta ordem arbitrárias, mas é tipicamente usado com as definições “set.mm” de axiomas. O axioma ax-groth adiciona o axioma de Tarski, que é definido da seguinte maneira em Metamath:

⊢ ∃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 também

• Sistema Mizar
• Metamath
• Universo de Grothendieck
• Axioma da limitação do tamanho

Bibliografia

• Andreas Blass, I.M. Dimitriou, and Benedikt Löwe (2007) "Inaccessible Cardinals without the Axiom of Choice," Fundamenta Mathematicae 194: 179-89.
• Predefinição:Citar conferência
• Patrick Suppes (1960) Axiomatic Set Theory. Van Nostrand. Dover reprint, 1972.
• Predefinição:Citar periódico
• Predefinição:Citar periódico