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 , o conjunto unitário 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 o conjunto . Então a imagem de (os valores de para qualquer pertencente 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[1]).
- Para todo conjunto , existe um conjunto cujos membros incluem: - O conjunto ; - todo subconjunto de cada membro de ; - o conjunto das partes de cada membro de ; - cada subconjunto de com cardinalidade menor que .
Mais formalmente:
onde "" denota a classe de x ,"" denota a equipotência.O que o axioma de Tarski diz(no vernáculo), é que para cada conjunto 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.;
- Par ordernado: O conjunto ;
- Subconjunto: O conjunto cujos elementos também são elementos de outros conjuntos;
- União de uma família de conjuntos : O conjunto de todos os elementos de qualquer elemento de .
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
Referências
- ↑ Tarski(1939)
Bibliografia
- Andreas Blass, I.M. Dimitriou, and Benedikt Löwe (2007) "Inaccessible Cardinals without the Axiom of Choice," Fundamenta Mathematicae 194: 179-89.
- Bourbaki, Nicolas (1972). «Univers». In: Michael Artin, Alexandre 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 (Lecture notes in mathematics 269) (em French). Berlin; New York: Springer-Verlag. pp. 185–217 !CS1 manut: Nomes múltiplos: lista de editores (link) !CS1 manut: Língua não reconhecida (link)
- Patrick Suppes (1960) Axiomatic Set Theory. Van Nostrand. Dover reprint, 1972.
- Tarski, Alfred (1938). «Über unerreichbare Kardinalzahlen» (PDF). Fundamenta Mathematicae. 30: 68–89
- Tarski, Alfred (1939). «On the well-ordered subsets of any set» (PDF). Fundamenta Mathematicae. 32: 176–183