# Axioma da substituição

Em teoria dos conjuntos, o axioma da substituição é um esquema de axiomas que garante a existência de um conjunto que é imagem de outro conjunto. Em termos simples, se existe alguma regra tal que y = f(x) se comporta como se f fosse uma função para todo x, $x\in A\,$, então existe um conjunto B de todos os y = f(x), $x\in A\,$. Este axioma é essencial para a construção de determinados conjuntos infinitos.

## Enunciado

Seja P(x,y) uma propriedade tal que para todo x existe um único y para o qual P(x,y) é válida. Para todo conjunto A, existe um conjunto B tal que, para todo x, $x\in A\,$, existe $y\in B\,$ para o qual P(x,y) é válida.

## Esquema axiomático da substituição

Seja uma fórmula com ao menos duas variáveis livres, φ(x, y). A seguinte fórmula, na linguagem formal dos axiomas de Zermelo-Fraenkel, é um axioma:
$(\forall x,y,z\,,\,\varphi (x,y)\wedge \varphi (x,z)\rightarrow y=z)\Rightarrow \forall A\exists B\,,\,\forall b\,(b\in B\leftrightarrow \exists a\in A:\varphi (a,b))$

## Exemplo

The número ordinal ω·2 = ω + ω (usando a definição moderna, devida a von Neumann) é o primeiro ordinal que não pode ser construído sem o axioma da substituição. O axioma do infinito garante a existência da sequência infinita ω = {0, 1 ,2 ,...}, e apenas esta sequência infinita. O objetivo é definir ω·2 como a união da sequência {ω, ω + 1, ω + 2,...}. O problema é que uma classe de ordinais pode não ser um conjunto (a classe de todos os ordinais, por exemplo, não é um conjunto - ver o paradoxo de Burali-Forti). O axioma da substituição permite substituir cada número finito n em ω pelo (único) ω + n, e garante que esta classe é um conjunto. Note-se que o axioma não é necessário para se construir um conjunto bem-ordenado isomórfico a ω·2 - basta tomar a união disjunta de duas cópias de ω, definindo-se que qualquer elemento da segunda cópia é maior que qualquer elemento da primeira; este conjunto, porém, não é um número ordinal (segundo von Neumann) porque não é totalmente ordenado pela relação $\in \,$.

## Aspecto histórico

O axioma da substituição é um esquema de axiomas da teoria dos conjuntos introduzidas de forma independente em 1922 por Abraham Adolf Fraenkel e Skolem Thoralf . Ela garante a existência de conjuntos que não poderiam ser obtidos na teoria dos conjuntos de Ernst Zermelo , e fornece um quadro mais fiel à teoria dos conjuntos axiomática de Georg Cantor . Ao adicionar a teoria de Zermelo, o esquema do axioma da substituição, obtemos a teoria de Zermelo-Fraenkel, ZF (ou ZFC, dependendo se se inclui ou não o axioma da escolha).
A inclusão de substituição envolve uma grande diferença a partir do ponto de vista da Teoria da Prova : a adição deste esquema para os axiomas de Zermelo torna este sistema logicamente muito mais forte, permitindo a demonstração de muitas afirmações. Em particular, ZF pode provar a consistência de Z por meio da construção do universo de von Neumann, V$_{ω2}$, como um modelo . (Lembrando que segundo o teorema da incompletude de Gödel, nenhuma dessas teorias pode provar sua própria consistência.)

## Independência

O axioma da substituição não pode ser demonstrado a partir do resto da teoria dos conjuntos de Zermelo-Fraenkel (ZF), já que podemos construir um modelo em que o resto dos axiomas são verdadeiros, bem como a negação do axioma da substituição.

## Utilização

O esquema de axiomas da substituição é útil por exemplo para as definições por indução em uma boa ordem . Assim, em teoria dos conjunto de Zermelo, isto é, na ausência do regime de substituição, não podemos demonstrar que qualquer conjunto bem ordenada é isomorfo a um ordinal von Neumann. Mas o regime de substituição é "inútil" se a relação funcional em jogo é um conjunto de pares , isto é, para dizer se é uma função no sentido da teoria dos conjuntos. Neste caso, o esquema de axioma de compreensão , que é simples de entender e usar, basta, basicamente, (você precisa do axioma do par). Além disso, o Axioma da compreensão é uma conseqüência - diria mesmo um caso especial - do Axioma da substituição. Da mesma forma o Axioma do par é deduzido a partir do Axioma da substituição, na presença do Axioma da potência

## Relação com o axioma da compreensão

O esquema de axiomas da compreensão pode ser obtida quase inteiramente a partir do esquema de axiomas da substituição. Por isso, o esquema de axiomas da compreensão é muitas vezes omitido nas listas modernas dos axiomas de Zermelo-Fraenkel. No entanto, ainda é importante por razões históricas, e as comparações com axiomatizações alternativas da teoria dos conjuntos. Por exemplo, a derivação do esquema da especificação explora o Lei do terceiro excluído e, depois a especificação não pode ser omitida em uma teoria definida intuicionista .