Propriedades de disjunção e existência

Na lógica matemática, as propriedades de disjunção e existência são as "marcas" das teorias construtivas como a aritmética de Heyting e as teorias de conjuntos construtivos (Rathjen 2005). A propriedade de disjunção é satisfeita por uma teoria se, sempre que uma sentença A v B é um teorema, então ou A é um teorema, ou B é um teorema. A propriedade de existência ou propriedade de testemunha é satisfeita por uma teoria se, sempre que uma sentença (∃x)A(x) é um teorema, onde A(x) não possui outras variáveis livres, então existe algum termo t tal que a teoria prove A(t).

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

Kurt Gödel (1932) provou que a lógica proposicional intuicionista (sem axiomas adicionais) possui a propriedade de disjunção; este resultado foi estendido para a lógica de predicados intuicionista por Gerhard Gentzen (1934,1935). Stephen Cole Kleene (1945) provou que a aritmética de Heyting possui a propriedade de disjunção e a propriedade de existência. O método de Kleene introduziu a técnica da realizabilidade, a qual é agora um dos principais métodos de estudo das teorias construtivas (Kohlenbach 2008; Troelstra 1973).

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.

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.

Ligações externas

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