# Teoria dos conjuntos de Tarski-Grothendieck

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:
    $\forall x\exists y[x\in y\wedge \forall z\in y({\mathcal {P}}(z)\subseteq y\wedge {\mathcal {P}}(z)\in y)\wedge \forall z\in {\mathcal {P}}(y)(\neg z\approx y\to z\in y)]$
onde "${\mathcal {P}}(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)\neq (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)))