# Teoria dos conjuntos/Revendo o axioma da separação

No texto do axioma da separação:
    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.
Ou, em sua forma mais genérica, qualquer fórmula $\phi \!$ na linguagem da teoria dos conjuntos 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 ))$
Um ponto que pode não ter ficado muito claro é que tipo de fórmula ou propriedade é admissível para Φ.
Este capítulo tem o objetivo de explorar estas fórmulas.

## Exemplo: conjuntos unitários

Seja Φ a propriedade definida como:
    $\Phi (x)=(\exists y,(y\in x\land \forall z,(z\in x\implies z=y)))\,$
Em Português, o que esta propriedade afirma?
    $\exists y,y\in x\,$ - significa que x não é o conjunto vazio.
    $\forall z,(z\in x\implies z=y)\,$ - significa que se x tem algum elemento, então este elemento é igual ao y
Em outras palavras, Φ(x) expressa, na linguagem da teoria dos conjuntos, que x é um conjunto unitário.
Por exemplo, podemos demonstrar (exercício) que Φ(1), Φ({1}) e Φ({2}) são verdadeiros, e que $\Phi (\varnothing )\,$, Φ(2) e Φ({1,2}) são falsos.
Como aplicação do esquema de axiomas, seja A = {1, 2}. Então o conjunto $B=\{x\in A|\Phi (x)\}\,$ é o conjunto B = {1}.
Ao aplicar a propriedade Φ na formação de subconjuntos, deve-se tomar o cuidado de não repetir os símbolos. Se temos uma demonstração lógica que já utilizou os símbolos x, y ou z, devemos usar a definição de Φ trocando o símbolo por algum outro.
Note-se que, pelos axiomas até agora apresentados, a expressão $\{x|\Phi (x)\}\,$ não denota um conjunto - aliás, é possível mostrar (usando uma variação do paradoxo de Russell) que este conjunto não existe, ou seja, que para todo conjunto A existe um conjunto unitário B que não é um elemento de A.

## A fórmula do axioma

A fórmula Φ do axioma deve ser uma fórmula bem formada, na linguagem da lógica clássica de primeira ordem.
Isto significa o seguinte:
* Podem ser usadas constantes e fórmulas previamente definidas, e variáveis novas
* Podem ser usados os conectivos lógicos da lógica proposicional (e, ou, não, implica, etc, combinados com parêntesis para mostrar prioridade de avaliação)
* Variáveis devem ser introduzidas pelos quantificadores existe e para todo, e seu uso deve ser limitado à proposição que se segue ao quantificador.
* Variáveis devem se relacionar entre si e com as constantes através unicamente de $\in \,$, ou de outros símbolos definidos anteriormente por fórmulas bem formadas.
* As fórmulas bem formadas são recursivas, ou seja, elementos de uma fórmula bem formada são fórmulas bem formadas.
Como exemplos, sendo A, B e C constantes:
* $x\in A\,$ é um fórmula bem formada na variável x
* $\exists x,x\in A\,$ não é uma fórmula bem formada na variável x, porque x não está livre
* $x\in A\implies x\in B\,$ é uma fórmula bem formada na variável x
* $x\in A\implies (\forall y,(y\in B\implies x\in y))\,$ é uma fórmula bem formada na variável x
* $x\in A\land y\in B\implies x=y\,$ é uma fórmula bem formada nas variáveis x e y
* $\exists y,(y\in x\lor \forall y(y\in A))\,$ não é uma fórmula bem formada em x: y aparece em um quantificador ($\forall y\,$) dentro de uma expressão condicional a outro quantificador $\exists y\,$)
* $(\forall y,z\in x,(y\in z\lor y=z\lor z\in y))\land (\forall y,z\in x,(y\in x\land z\in y\implies z\in x))\,$ é uma fórmula bem formada na variável x (esta é uma das definições de um número ordinal)

## Sementinha do mal

Agora é um bom ponto para plantar uma sementinha do mal. O axioma diz explicitamente que para todo conjunto x e toda fórmula φ existe um subconjunto y dos elementos de x que satisfazem esta propriedade.
Uma pergunta interessante é inverter o enunciado do axioma: será que, para todo subconjunto y de x, existe uma fórmula bem formada φ (que, obviamente, seja livre de y) de modo que y seja definido através dela?
Esta pergunta aparentemente inocente tem profundas implicações, mas, por enquanto, ainda não temos ferramentas adequadas para explorá-la.