# Axiomas de Zermelo-Fraenkel

Na matemática, a teoria dos conjuntos de Zermelo-Fraenkel com o axioma da escolha, nomeada em homenagem aos matemáticos Ernst Zermelo e Abraham Fraenkel e comumente abreviada como ZFC, é um dos muitos sistemas axiomáticos que foram propostos no início do século XX para promover uma teoria dos conjuntos sem os paradoxos da teoria ingênua dos conjuntos, como o paradoxo de Russell. Especificamente, a ZFC não permite o axioma da compreensão. Atualmente, a ZFC é a forma padrão da teoria axiomática dos conjuntos, sendo o fundamento matemático mais comum. A ZFC deve formalizar uma única noção primitiva de um conjunto hereditário bem-fundado, para que cada indivíduo no domínio de discurso seja um conjunto. Desta forma, os axiomas da ZFC se referem apenas a conjuntos, e não urelementos (elementos de conjuntos que não são conjuntos) ou classes (coleções de objetos matemáticos definidos por uma propriedade em comum de seus membros). Os axiomas da ZFC previnem seus modelos de possuírem urelementos, e classes próprias só podem ser tratadas indiretamente. Formalmente, a ZFC é uma teoria de estruturas de lógica de primeira ordem. A assinatura possui igualdade e uma única relação binária primitiva, que é a pertinência, normalmente denotada por ∈. A fórmula a ∈ b significa que o conjunto a é membro do conjunto b (que também é lido como "a é elemento de b" ou "a está em b"). Existem várias formulações equivalentes dos axiomas da ZFC. A maioria de seus axiomas formulam a existência de conjuntos particulares definidos a partir de outros conjuntos. Por exemplo, o axioma do par diz que, dados dois conjuntos quaisquer a e b, existe um novo conjunto {a, b} contendo exatamente a e b. Outros axiomas descrevem propriedades da pertinência de conjuntos. Um dos objetivos dos axiomas da ZFC é que cada axioma deve ser verdade se interpretado como uma afirmação sobre a coleção de todos os conjuntos do universo de von Neumann (também conhecido como a hierarquia cumulativa). A metamatemática da ZFC foi estudada extensivamente. Resultados marcantes dessa área estabeleceram a independência da hipótese do contínuo da ZFC, e o axioma da escolha dos axiomas restantes da ZFC.

## História

Em 1908, Ernst Zermelo propôs a primeira teoria axiomática dos conjuntos, teoria dos conjuntos de Zermelo. Essa teoria axiomática não permitia a construção de números ordinais grandes. Enquanto a maioria da "matemática ordinária" pode ser desenvolvida sem usar esses ordinais grandes, eles são uma ferramenta essencial na maioria das investigações teóricas relacionadas a conjuntos. Além do mais, um dos axiomas de Zermelo invocou um conceito de propriedade "definida", cujo sentido operacional não era muito claro. Em 1922, Abraham Fraenkel e Thoralf Skolem propuseram, independentemente, a operacionalização de uma propriedade "definida" como uma que fosse formulada como uma teoria de primeira ordem cujas fórmulas atômicas fossem limitadas a pertinência e identidade de conjuntos. Eles também propuseram, independentemente, a troca do axioma da separação pelo axioma da substituição. Anexando a esse esquema, assim como o axioma da regularidade (proposto primeiramente por Dmitry Mirimanoff em 1917), à teoria dos conjuntos de Zermelo produz uma teoria chamada de ZF. Adicionar à ZF o axioma da escolha (AC) ou uma afirmação similar produz a ZFC.

## Os Axiomas
### Axioma da extensão

Dois conjuntos são iguais se eles têm os mesmos elementos.
    $\forall x\forall y(\forall z(z\in x\leftrightarrow z\in y)\rightarrow x=y)$
A recíproca é consequência da propriedade da substituição na igualdade. Deve-se notar que em ZFC não existem urelementos, ou seja, todo elemento de um conjunto é, também, um conjunto.

### Axioma da regularidade

Também chamado de Axioma da fundação, diz que todo conjunto não-vazio x contém algum elemento y tal que x e y são disjuntos.
    $\forall x[\exists y(y\in x)\rightarrow \exists y(y\in x\land \lnot \exists z(z\in y\land z\in x))]$
Nem todas versões da Teoria incluem esse axioma; esse axioma, porém, garante que não existem conjuntos do tipo $X=\{X\}$. E juntamente com o Axioma do Par garante que não existem conjuntos do tipo $Y=\{\varnothing ,Y\}$. Esse axioma também garante que a definição alternativa de par ordenado (a, b) = {a, {a,b}} seja satisfatória.

### Axioma da separação

Também chamado de Axioma da compreensão, ou ainda Axioma de Especificação), diz que se z é um conjunto e $\phi \!$ é qualquer propriedade que possa ser atribuída a elementos x de z, então existe um subconjunto y de z que contém os elementos x de z e que possuem essa propriedade. A restrição a z é necessária para evitar o paradoxo de Russell e suas variantes. Formalmente: qualquer formula $\phi \!$ na linguagem da ZFC com variáveis livres entre $x,z,w_{1},\ldots ,w_{n}\!$:
    $\forall z\forall w_{1}\ldots w_{n}\exists y\forall x(x\in y\iff (x\in z\land \phi ))$
Notar que esse não é um axioma, mas um esquema de axiomas: cada $\phi \!$ gera um novo axioma.

### Axioma do par

Se x e y são conjuntos (não necessariamente distintos) então existe um conjunto no qual x e y são elementos.
    $\forall x\forall y\exists z(x\in z\land y\in z)$

### Axioma da união

Para todo conjunto ${\mathcal {F}}$ existe um conjunto A tal que todo elemento que pertence a um elemento de ${\mathcal {F}}$ é um elemento de A.
    $\forall {\mathcal {F}}\,\exists A\,\forall Y\,\forall x(x\in Y\land Y\in {\mathcal {F}}\rightarrow x\in A)$

### Axioma da substituição

O objetivo é garantir que se algum esquema f, quando aplicado ao conjunto x, tem a cara de uma função, então existe um conjunto f(x). Formalmente: para toda fórmula $\phi \!$ na linguagem da ZFC com variáveis livres entre $x,y,A,w_{1},\ldots ,w_{n}\!$:
    $\forall A\,\forall w_{1},\ldots ,w_{n}[\forall x\in A\exists !y\phi \rightarrow \exists Y\forall x\in A\exists y\in Y\phi ].$
O símbolo $\exists !y$ significa que $y\!$ existe e é único. O próximo axioma usa a notação $S(x)=x\cup \{x\}\!$, chamado de sucessor de x. Os Axiomas 1 a 6 provam que $S(x)\!$ existe e é único para todo conjunto $x\!$. Outra consequência dos axiomas precedentes é que o conjunto vazio $\varnothing$ existe e é único.

### Axioma do infinito

Existe um conjunto x que tem o conjunto vazio como elemento, e que, para todo elemento y, ele contém seu sucessor S(y).
    $\exists x(\varnothing \in x\land \forall y\in x(S(y)\in x))$
Para o próximo axioma é conveniente definir $z\subseteq x$ como for $\forall q(q\in z\rightarrow q\in x)$.

### Axioma da potência

Para todo conjunto x existe um conjunto y que tem como elementos todo subconjunto de x.
    $\forall x\exists y\forall z(z\subseteq x\rightarrow z\in y)$
O próximo axioma é o mais polêmico de todos.

### Axioma da escolha

Para todo conjunto X existe uma relação binária R que torna X bem ordenado. Isso significa que R é uma relação de ordem em X e que todo subconjunto não-vazio de X tem um elemento que é mínimo nesta relação R.
    $\forall A\exists R(R\;{\mbox{well-orders}}\;A)$
Kunen também inclui um axioma redundante que diz que existe pelo menos um conjunto, o que pode ser provado a partir do axioma do infinito. O axioma do par também é redundante, e pode ser deduzido dos axiomas do infinito, separação e substituição. Existem formas alternativas dos primeiros oito axiomas. Por exemplo, o axioma do par (#4) costuma se apresentar na forma seguinte: para todos conjuntos x e y existe um conjunto z cujos elementos são x, y e mais nada: $\forall x\forall y\exists z(x\in z\land y\in z\land (\forall t\in z(t=x\lor t=y)))$. Analogamente, os axiomas da união, substituição e potência costumam ser escritos de forma que o conjunto por eles definido seja único. Essas variantes dos axiomas podem ser vistas em Jech. O Axioma da escolha pode ser substituído por formas equivalentes (em outras palavras, os primeiros 8 axiomas podem provar que essas formas do axioma da escolha são equivalentes). Dentre essas a mais conhecida, e que dá origem ao nome do axioma, é a que diz que todo conjunto formado por conjuntos não vazios tem uma função escolha. Na lista acima, dois axiomas são, na verdade, uma lista infinita de axiomas. Sabe-se que não existe uma forma de apresentar ZFC com um número finito de axiomas. Existe, porém, uma versão alternativa do axioma da substituição que implica o axioma da compreensão; isso permite escrever os axiomas da ZFC com apenas um esquema de axiomas.

## Motivação pela hierarquia cumulativa

Uma motivação a favor dos axiomas da ZFC é a hierarquia cumulativa de conjuntos introduzida por John von Neumann (Shoenfield 1977, sec. 2). Nesse ponto de vista, o universo da teoria dos conjuntos é construído em etapas, sendo uma etapa para cada número ordinal. Na etapa 0 não existem conjuntos. Em cada etapa seguinte, um conjunto é adicionado ao universo se todos os seus elementos foram adicionados em etapas anteriores. Logo, o conjunto vazio é adicionado na fase 1, e o conjunto contendo o conjunto vazio é adicionado na etapa 2; veja Hinman (2005, p. 467). A coleção de todos os conjuntos que são obtidos desta maneira, sobre todas as etapas, é conhecida como V. Os conjuntos em V podem ser organizados numa hierarquia atribuindo à cada conjunto a primeira etapa na qual esse conjunto foi adicionado à V.
É provável (demonstrável) que um conjunto está em V se e somente se o conjunto é puro e bem-fundado; e provável (demonstrável) que V satisfaz todos os axiomas da ZFC, se a classe de ordinais possui propriedades de reflexão apropriadas. Por exemplo, suponha que o conjunto x é adicionado na etapa α, o que significa que cada elemento de x foi adicionado em uma etapa anterior a α. Então cada subconjunto de x também é adicionado na etapa α, pois todos os elementos de qualquer subconjunto de x foram adicionados também antes da etapa α. Isso significa que qualquer subconjunto de x o qual o axioma da separação pode construir é adicionado na etapa α, e que o conjunto das partes de x será adicionado na próxima etapa após α. Para uma explicação completa de que V satisfaz a ZFC, veja Shoenfield (1977).
A descrição do universo de conjuntos estratificados na hierarquia cumulativa é característica da ZFC e teorias axiomáticas de conjuntos relacionadas, como a teoria dos conjuntos de Von Neumann-Bernays-Gödel (comumente chamada de NBG) e a teoria dos conjuntos de Morse-Kelley. A hierarquia cumulativa não é compatível com outras teorias de conjuntos como Novas Fundações.
É possível alterar a definição de V para que, em cada etapa, ao invés de adicionar todos os subconjuntos da união das etapas anteriores, subconjuntos só são adicionados se eles são definidos em um certo sentido. Isso resulta em uma hierarquia mais "estreita" que dá o universo construível L, que também satisfaz todos os axiomas da ZFC, incluindo o axioma da escolha. A questão se V = L é independente dos axiomas da ZFC. Apesar da estrutura de L ser mais regular e melhor comportada do que a de V, poucos matemáticos argumentam que V = L deva ser adicionado à ZFC como um axioma adicional.

## Metamatemática

Os esquemas axiomáticos de substituição e separação contém várias instâncias. Montague (1961) incluiu um resultado primeiramente provado em sua tese de doutorado, em 1957: se a ZFC é consistente, então é impossível axiomatizar a ZFC usando um número finito de axiomas. Por outro lado, a teoria dos conjuntos de Von Neumann-Bernays-Gödel (NBG) pode ser axiomatizada com um número finito de axiomas. A ontologia da NBG inclui classes próprias, assim como conjuntos; um conjunto é qualquer classe que possa ser membro de outra classe. A NBG e a ZFC são teorias de conjuntos equivalentes, num sentido que qualquer teorema que não menciona classes e é provável (demonstrável) em uma teoria, é provável (demonstrável) na outra.
O Teoremas da incompletude de Gödel diz que um sistema recursivamente axiomatizável que pode interpretar a aritmética de Robinson pode provar sua própria consistência apenas se for inconsistente. Além do mais, a aritmética de Robinson pode ser interpretada na teoria geral dos conjuntos, um pequeno fragmento da ZFC. Por isso a consistência da ZFC não pode ser provada na própria ZFC (a não ser que seja, de fato, inconsistente). Assim, dada que a ZFC é identificada com matemáticas ordinárias, a consistência da ZFC não pode ser demonstrada em matemáticas ordinárias. A consistência da ZFC não vem da existência de um cardinal inacessível fraco, que é improvável na ZFC se a ZFC é consistente. Ainda assim, é difícil que a ZFC abrigue uma contradição insuspeita; acredita-se que, se a ZFC fosse inconsistente, esse fato já teria sido revelado. Isto é certo — a ZFC é imune aos paradoxos clássicos da teoria ingênua dos conjuntos: paradoxo de Russel, o paradoxo de Burali-Forti e o paradoxo de Cantor.
Abian e LaMacchia (1978) estudaram uma subteoria da ZFC consistindo nos axiomas da extensão, união, potência, substituição e escolha. Usando modelos, eles provaram que essa subteoria era consistente, e provaram que cada um dos axiomas de extensão, substituição e potência eram independentes dos outros quatro axiomas dessa subteoria. Se essa subteoria é aumentada com o axioma da infinitude, cada um dos axiomas da união, escolha e infinitude são independentes dos outros cinco axiomas. Já que existem modelos não bem-fundados que satisfazem cada axioma da ZFC exceto o axioma da regularidade, esse axioma é independente de outros axiomas da ZFC.
Se consistente, a ZFC não pode provar a existência de cardinais inacessíveis que as teoria das categorias requerem. Grandes conjuntos dessa natureza são possíveis se a ZF é aumentada com o axioma de Tarski (Tarski, 1939). Assumindo que esse axioma transforma os axiomas de infinitude, potência e escolha em teoremas.

### Independência na ZFC

Muitas afirmações importantes são independentes da ZFC, supondo que ZF é consistente (veja afirmações matemáticas indecidíveis na ZFC). A independência é comumente provada por forçamento, pelo que é mostrado que cada modelo contável transitivo da ZFC (algumas vezes aumentado com os axiomas de grande cardinal) pode ser expandido para satisfazer a afirmação em questão. Uma expansão diferente é então mostrada para satisfazer a negação da afirmação. Uma prova de independência por forçamento automaticamente prova a independência de afirmações aritméticas, outras afirmações concretas, e axiomas de grande cardinal. Alguns modelos internos, como no universo construível. Apesar disso, algumas afirmações que são verdadeiras sobre conjuntos construíveis não são consistentes com axiomas hipotéticos de grande cardinal, como no caso do enunciado que afirma a existência de cardinais mensuráveis.
Forçamento prova que as seguintes afirmações são independentes da ZFC:
* Hipótese do continuum
* Princípio diamante
* Problema de Suslin
* Axioma de Martin (que não é um axioma de ZFC)
* Axioma de construtibilidade (V=L) (que também não é um axioma de ZFC).
Observações:
* A consistência de V=L é provável por modelos internos, mas não por forçamento: cada modelo da ZF pode ser aparado para se transformar um modelo ZFC+V=L.
* O Princípio Diamante implica a Hipótese do Continuum e a negação da Hipótese de Suslin.
* O Axioma de Martin somado com a negação da Hipótese do Continuum implica a Hipótese de Suslin.
* O universo construível satisfaz a Hipótese Generalizada do Continuum.
* A falha da Hipótese de Kurepa é equiconsistente com a existência de um cardinal inacessível.
Uma variação no método de forçamento também pode ser usada para demonstrar a consistência e improvabilidade do axioma da escolha, i.e., que o axioma da escolha é independente da ZF. A consistência da escolha pode ser (relativamente) fácil de se verificar provando que o modelo interno L satisfaz a escolha (Por conta disso, cada modelo de ZF contém um submodelo da ZFC, de forma que Con(ZF) implica Con(ZFC)). Já que forçamento preserva escolha, nós não podemos, diretamente, produzir um modelo contradizendo a escolha de um modelo satisfazendo a escolha. Apesar disso, nós podemos usar forçamento para criar um modelo que contém um submodelo apropriado, nomeadamente um satisfazendo a ZF mas não C.
Outro método de provar resultados de independência, um que nada tem a ver com forçamento, é baseado no segundo teorema da incompletude de Gödel. Essa técnica emprega a afirmação cuja independência está sendo examinada, para provar a existência de um conjunto modelo da ZFC, em que Con(ZFC) é verdadeiro. Já que ZFC satisfaz as condições do segundo teorema de Gödel, a consistência da ZFC não é provável na ZFC, se ZFC é consistente. Por isso nenhuma afirmação permitindo tal prova pode ser provada na ZFC, sob esse suposto de consistência. Esse método pode provar que a existência de grandes cardinais não é provável na ZFC, mas não pode provar que a adição de um axioma de grande cardinal não irá gerar novas contradições.

## Críticas

A ZFC já foi criticada tanto por ser excessivamente forte e por ser excessivamente fraca, assim como sua falha em capturar objetos como classes próprias e o conjunto universal.
Muitos teoremas matemáticos podem ser provados em sistemas muito mais fracos que a ZFC, como na aritmética de Peano e na aritmética de segunda ordem (como explorada pelo programa de matemática reversa). Saunders Mac Lane e Solomon Feferman ambos chegaram à essa conclusão. Algumas das "matemáticas da corrente principal" (matemáticas que não estão ligadas diretamente à teoria axiomática dos conjuntos) vão além da aritmética de Peano e aritmética de segunda ordem, mas, ainda assim, elas podem ser executadas em ZC (teoria de conjuntos de Zermelo com escolha), outra teoria mais fraca que a ZFC. Muito do poder da ZFC, incluindo o axioma da regularidade e o axioma da substituição, é incluso principalmente para facilitar o estudo da própria teoria dos conjuntos.
Por outro lado, dentre as teorias axiomáticas de conjuntos, a ZFC é comparativamente fraca. Diferente dos novos fundamentos, a ZFC não admite a existência de um conjunto universal. Por isso o universo de conjuntos dentro da ZFC não é fechado sob operações elementais da álgebra de conjuntos. Diferentemente da teoria de conjuntos de von Neumann-Bernays-Gödel e da teoria dos conjuntos de Morse-Kelley (MK), a ZFC não admite a existência de classes próprias. Essas restrições ontológicas são necessárias para que a ZFC evite o paradoxo de Russell, mas críticos argumentam que essas restrições fazem com que os axiomas da ZFC falhem ao capturar o conceito informal de conjunto. Outra fraqueza da ZFC é que o axioma da escolha incluso no ZFC é mais fraco do que o axioma da escolha global incluso na MK.
Existem muitas afirmações matemáticas indecidíveis na ZFC. Elas incluem a hipótese do contínuo, o problema de Whitehead e a conjectura do espaço normal de Moore. Algumas dessas conjecturas são prováveis com a adição de axiomas como o axioma de Martin e axioma de grande cardinal à ZFC. Alguns outros são decidíveis em ZF+AD, onde AD é o axioma da determinância, uma forte suposição incompatível com a escolha. Um atrativo dos axiomas de grande cardinal é que eles permitem que muitos resultados da ZF+AD possam ser estabelecidos na ZFC unidos por um axioma de grande cardinal. O sistema Mizar adotou a Teoria dos conjuntos de Tarski-Grothendieck ao invés da ZFC para que suas provas envolvendo o universo de Grothendieck (encontrado na teoria da categoria e geometria algébrica) possam ser formalizadas.