# Propriedades de disjunção e existência
## Propriedades relacionadas

Rathjen (2005) lista cinco propriedades que uma teoria pode possuir. Estas incluem a propriedade de disjunção (PD), a propriedade de existência (PE) e três propriedades adicionais:
* A propriedade de existência numérica (PEN) afirma que se a teoria prova que $(\exists x\in \mathbb {N} )\varphi (x)$, onde φ não possui outras variáveis livres, então a teoria prova $\varphi ({\bar {n}})$ para algum $n\in \mathbb {N}$. Aqui, ${\bar {n}}$ é um termo em $T$ representando o número n.
* A regra de Church (RC) afirma que se uma teoria prova que $(\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)$ então existe um número natural e tal que, sendo $f_{e}$ a função computável de índice e, a teoria prova que $(\forall x)\varphi (x,f_{e}(x))$.
* A variante da regra de Church (RC') afirma que se a teoria prova que $(\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)$ então existe um número natural e tal que a teoria prova que $f_{e}$ é total e prova $\psi (f_{e})$.
Estas propriedades só podem ser expressadas diretamente por teorias que possuam a habilidade de quantificar sobre números naturais e, para RC', quantificar sobre funções de $\mathbb {N}$ a $\mathbb {N}$. Na prática, pode-se dizer que uma teoria tem uma dessas propriedades se uma extensão definicional da teoria possui a propriedade declarada acima (Rathjen 2005).

## Antecedentes e História

Enquanto os resultados iniciais foram pelas teorias construtivas da aritmética, vários resultados também são conhecidos pelas teorias de conjuntos construtivos (Rathjen 2005). John Myhill (1973) mostrou que ZFI com o axioma da Substituição eliminado para favorecer o axioma da Coleção possui a propriedade de disjunção, a propriedade de existência numérica, e a propriedade de existência. Michael Rathjen (2005) provou que ZFC possui a propriedade de disjunção e a propriedade de existência numérica.
A maioria das teorias clássicas, como a Aritmética de Peano e ZFC não possuem as propriedades de existência ou disjunção. Algumas teorias clássicas, como ZFC além do axioma da construtibilidade, deveras possuem uma forma enfraquecida da propriedade de existência (Rathjen 2005).

## Em topoi

Freyd e Scedrov (1990) observaram que a propriedade de disjunção se mantém nas álgebras de Heyting livres e nos topoi livres. Em termos categóricos, no topos livre, isto corresponde ao fato do objeto terminal, $\mathbf {1}$, não é a junção de dois subobjetos próprios. Juntamente à propriedade de existência se traduz a asserção de que $\mathbf {1}$ é um objeto projetivo indecomponível – o functor que ele representa (o functor de secção global) preserva epimorfismos e coprodutos.

## Relações

Existem diversas relações entre as cinco propriedades discutidas acima.
A propriedade da existência numérica implica a propriedade de disjunção. A prova usa o fato de uma disjunção poder ser reescrita como uma fórmula existencial quantificando sobre números naturais:
    $A\vee B\equiv (\exists n)[(n=0\to A)\wedge (n\neq 0\to B)]$.
Portanto, se $A\vee B$ é um teorema de $T$, $\exists n\colon (n=0\to A)\wedge (n\neq 0\to B)$ também o é. Logo, assumindo a propriedade de existência numérica, existe algum $s$ tal que $({\bar {s}}=0\to A)\wedge ({\bar {s}}\neq 0\to B)$ é um teorema. Como ${\bar {s}}$ é um numeral, pode-se checar concretamente o valor $s$: se $s=0$ então $A$ é um teorema e se $s\neq 0$ então $B$ é um teorema.
Harvey Friedman (1974) provou que em qualquer extensão recursivamente enumerável da aritmética intuicionista, a propriedade da disjunção implica a propriedade da existência numérica. A prova usa sentenças autorreferenciais de maneira similar à prova dos teoremas da incompletude de Gödel. O passo chave é achar uma delimitação no quantificador existencial em uma fórmula (∃x)A(x), produzindo uma fórmula existencial delimitada (∃x<n)A(x). A fórmula delimitada pode em seguida ser escrita como a disjunção finita A(1)∨A(2)∨...∨A(n). Finalmente, a eliminação da disjunção pode ser usada para mostrar que um dos disjuntos é provável.