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 1939Tarski(1939)).
- 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
Bibliografia
Andreas Blass, I.M. Dimitriou, and Benedikt Löwe (2007) "Inaccessible Cardinals without the Axiom of Choice," Fundamenta Mathematicae 194: 179-89.
Patrick Suppes (1960) Axiomatic Set Theory. Van Nostrand. Dover reprint, 1972.
Categoria:Teoria dos conjuntos Categoria:Sistemas conceituais