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 ${\displaystyle (\exists x\in \mathbb {N} )\varphi (x)}$, onde φ não possui outras variáveis livres, então a teoria prova ${\displaystyle \varphi ({\bar {n}})}$ para algum ${\displaystyle n\in \mathbb {N} }$. Aqui, ${\displaystyle {\bar {n}}}$ é um termo em ${\displaystyle T}$ representando o número n.
• A regra de Church (RC) afirma que se uma teoria prova que ${\displaystyle (\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)}$ então existe um número natural e tal que, sendo ${\displaystyle f_{e}}$ a função computável de índice e, a teoria prova que ${\displaystyle (\forall x)\varphi (x,f_{e}(x))}$.
• A variante da regra de Church (RC') afirma que se a teoria prova que ${\displaystyle (\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)}$ então existe um número natural e tal que a teoria prova que ${\displaystyle f_{e}}$ é total e prova ${\displaystyle \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 ${\displaystyle \mathbb {N} }$ a ${\displaystyle \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).

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).

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, ${\displaystyle \mathbf {1} }$, não é a junção de dois subobjetos próprios. Juntamente à propriedade de existência se traduz a asserção de que ${\displaystyle \mathbf {1} }$ é um objeto projetivo indecomponível – o functor que ele representa (o functor de secção global) preserva epimorfismos e coprodutos.

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:

${\displaystyle A\vee B\equiv (\exists n)[(n=0\to A)\wedge (n\neq 0\to B)]}$.

Portanto, se ${\displaystyle A\vee B}$ é um teorema de ${\displaystyle T}$, ${\displaystyle \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 ${\displaystyle s}$ tal que ${\displaystyle ({\bar {s}}=0\to A)\wedge ({\bar {s}}\neq 0\to B)}$ é um teorema. Como ${\displaystyle {\bar {s}}}$ é um numeral, pode-se checar concretamente o valor ${\displaystyle s}$: se ${\displaystyle s=0}$ então ${\displaystyle A}$ é um teorema e se ${\displaystyle s\neq 0}$ então ${\displaystyle 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.

Referências

• Petre J. Freyd and Andre Scedrov, 1990, Categories, Allegories. North-Holland.
• Harvey Friedman, 1975, The disjunction property implies the numerical existence property, State University of New York at Buffalo.
• Gerhard Gentzen, 1934, "Untersuchungen über das logische Schließen. I", Mathematische Zeitschrift v. 39 n. 2, pp. 176–210.
• Gerhard Gentzen, 1935, "Untersuchungen über das logische Schließen. II", Mathematische Zeitschrift v. 39 n. 3, pp. 405–431.
• Kurt Gödel, 1932, "Zum intuitionistischen Aussagenkalkül", Anzeiger der Akademie der Wissenschaftischen in Wien, v. 69, pp. 65–66.
• Stephen Cole Kleene, 1945, “On the interpretation of intuitionistic number theory,” Journal of Symbolic Logic, v. 10, pp. 109–124.
• Ulrich Kohlenbach, 2008, Applied proof theory, Springer.
• John Myhill, 1973, "Some properties of Intuitionistic Zermelo-Fraenkel set theory", in A. Mathias and H. Rogers, Cambridge Summer School in Mathematical Logic, Lectures Notes in Mathematics v. 337, pp. 206–231, Springer.
• Michael Rathjen, 2005, "The Disjunction and Related Properties for Constructive Zermelo-Fraenkel Set Theory", Journal of Symbolic Logic, v. 70 n. 4, pp. 1233–1254.
• Anne S. Troelstra, ed. (1973), Metamathematical investigation of intuitionistic arithmetic and analysis, Springer.

• Intuitionistic Logic por Joan Moschovakis, Stanford Encyclopedia of Philosophy (em inglês)