Propiedades de disyunción y existencia

En lógica matemática , las propiedades de disyunción y existencia son los "sellos distintivos" de las teorías constructivas como la aritmética de Heyting y las teorías de conjuntos constructivos (Rathjen 2005).

• La propiedad de disyunción se satisface en una teoría si, siempre que una oración A ∨ B es un teorema , entonces A es un teorema o B es un teorema.
• La propiedad de existencia o propiedad testigo se satisface por una teoría si, siempre que una oración (∃ x ) A ( x ) es un teorema, donde A ( x ) no tiene otras variables libres, entonces hay algún término t tal que la teoría prueba A ( t ) .

Rathjen (2005) enumera cinco propiedades que puede poseer una teoría, entre ellas la propiedad de disyunción ( PD ), la propiedad de existencia ( PE ) y tres propiedades adicionales:

• La propiedad de existencia numérica (NEP) establece que si la teoría demuestra que , donde φ no tiene otras variables libres, entonces la teoría demuestra que para alguna Aquí hay un término en que representa el número n .${\displaystyle (\exists x\in \mathbb {N} )\varphi (x)}$${\displaystyle \varphi ({\bar {n}})}$${\displaystyle n\in \mathbb {N} {\text{.}}}$${\displaystyle {\bar {n}}}$${\displaystyle T}$
• La regla de Church (CR) establece que si la teoría demuestraque , entonces existe un número natural e tal que, siendola función computable con índice e , la teoría demuestra que.${\displaystyle (\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)}$${\displaystyle f_{e}}$${\displaystyle (\forall x)\varphi (x,f_{e}(x))}$
• Una variante de la regla de Church, CR ₁ , establece que si la teoría prueba que entonces existe un número natural e tal que la teoría prueba que es total y prueba que .${\displaystyle (\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)}$${\displaystyle f_{e}}$${\displaystyle \psi (f_{e})}$

Estas propiedades sólo pueden expresarse directamente para teorías que tienen la capacidad de cuantificar sobre números naturales y, para CR ₁ , cuantificar sobre funciones de a . En la práctica, se puede decir que una teoría tiene una de estas propiedades si una extensión definicional de la teoría tiene la propiedad establecida anteriormente (Rathjen 2005). ${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$

Casi por definición, una teoría que acepta el tercero excluido y tiene enunciados independientes no tiene la propiedad de disyunción. Por lo tanto, todas las teorías clásicas que expresan la aritmética de Robinson no la tienen. La mayoría de las teorías clásicas, como la aritmética de Peano y la ZFC , a su vez, tampoco validan la propiedad de existencia, por ejemplo, porque validan la afirmación de existencia del principio del número mínimo . Pero algunas teorías clásicas, como la ZFC más el axioma de constructibilidad , sí tienen una forma más débil de la propiedad de existencia (Rathjen 2005).

La aritmética de Heyting es bien conocida por tener la propiedad de disyunción y la propiedad de existencia (numérica).

Si bien los primeros resultados se dieron en el campo de las teorías constructivas de la aritmética, también se conocen muchos resultados en el campo de las teorías constructivas de conjuntos (Rathjen, 2005). John Myhill  (1973) demostró que la IZF con el axioma de reemplazo eliminado en favor del axioma de colección tiene la propiedad de disyunción, la propiedad de existencia numérica y la propiedad de existencia. Michael Rathjen (2005) demostró que la CZF tiene la propiedad de disyunción y la propiedad de existencia numérica.

Freyd y Scedrov (1990) observaron que la propiedad de disyunción se cumple en las álgebras de Heyting libres y en los topos libres . En términos categóricos , en los topos libres, eso corresponde al hecho de que el objeto terminal , , no es la unión de dos subobjetos propios. Junto con la propiedad de existencia, se traduce en la afirmación de que es un objeto proyectivo indecomponible —el funtor que representa (el funtor de sección global) preserva epimorfismos y coproductos . ${\displaystyle \mathbf {1} }$${\displaystyle \mathbf {1} }$

Existen varias relaciones entre las cinco propiedades analizadas anteriormente.

En el contexto de la aritmética, la propiedad numérica de existencia implica la propiedad de disyunción. La prueba utiliza el hecho de que una disyunción puede reescribirse como una fórmula existencial que cuantifica sobre números naturales:

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

Por lo tanto, si

${\displaystyle A\vee B}$es un teorema de , entonces es .${\displaystyle T}$${\displaystyle \exists n\colon (n=0\to A)\wedge (n\neq 0\to B)}$

Así pues, asumiendo la propiedad de existencia numérica, existe algo tal que ${\displaystyle s}$

${\displaystyle ({\bar {s}}=0\to A)\wedge ({\bar {s}}\neq 0\to B)}$

es un teorema. Como es un numeral, se puede comprobar concretamente el valor de : si entonces es un teorema y si entonces es un teorema. ${\displaystyle {\bar {s}}}$${\displaystyle s}$${\displaystyle s=0}$${\displaystyle A}$${\displaystyle s\neq 0}$${\displaystyle B}$

Harvey Friedman (1974) demostró que en cualquier extensión recursivamente enumerable de la aritmética intuicionista , la propiedad de disyunción implica la propiedad numérica de existencia. La prueba utiliza oraciones autorreferenciales de manera similar a la prueba de los teoremas de incompletitud de Gödel . El paso clave es encontrar un límite en el cuantificador existencial en una fórmula (∃ x )A( x ), produciendo una fórmula existencial acotada (∃ x < n )A( x ). La fórmula acotada puede entonces escribirse como una disyunción finita A(1)∨A(2)∨...∨A(n). Finalmente, la eliminación de la disyunción puede usarse para mostrar que una de las disyunciones es demostrable.

Kurt Gödel  (1932) afirmó sin pruebas que la lógica proposicional intuicionista (sin axiomas adicionales) tiene la propiedad de disyunción; este resultado fue demostrado y extendido a la lógica de predicados intuicionista por Gerhard Gentzen  (1934, 1935). Stephen Cole Kleene  (1945) demostró que la aritmética de Heyting tiene la propiedad de disyunción y la propiedad de existencia. El método de Kleene introdujo la técnica de realizabilidad , que ahora es uno de los principales métodos en el estudio de las teorías constructivas (Kohlenbach 2008; Troelstra 1973).

• Teoría de conjuntos constructivos
• Aritmética de Heyting
• Ley del tercero excluido
• Realizabilidad
• Cuantificador existencial

• Peter J. Freyd y Andre Scedrov, 1990, Categorías, Alegorías . Holanda Septentrional.
• Harvey Friedman , 1975, La propiedad de disyunción implica la propiedad de existencia numérica , Universidad Estatal de Nueva York en Buffalo.
• Gerhard Gentzen , 1934, "Untersuchungen über das logische Schließen. I", Mathematische Zeitschrift v. 39 n. 2, págs. 176–210.
• Gerhard Gentzen , 1935, "Untersuchungen über das logische Schließen. II", Mathematische Zeitschrift v. 39 n. 3, págs. 405–431.
• Kurt Gödel , 1932, "Zum intuitionistischen Aussagenkalkül", Anzeiger der Akademie der Wissenschaftischen in Wien , v. 69, págs.
• Stephen Cole Kleene, 1945, "Sobre la interpretación de la teoría de números intuicionista", Journal of Symbolic Logic , v. 10, págs. 109-124.
• Ulrich Kohlenbach , 2008, Teoría de la prueba aplicada , Springer.
• John Myhill , 1973, "Algunas propiedades de la teoría de conjuntos intuicionista de Zermelo-Fraenkel", en A. Mathias y H. Rogers, Cambridge Summer School in Mathematical Logic , Lectures Notes in Mathematics v. 337, págs. 206-231, Springer.
• Michael Rathjen, 2005, "La disyunción y propiedades relacionadas para la teoría de conjuntos constructiva de Zermelo-Fraenkel", Journal of Symbolic Logic , v. 70 n. 4, págs. 1233–1254.
• Anne S. Troelstra , ed. (1973), Investigación metamatemática de la aritmética y el análisis intuicionistas , Springer.

• Moschovakis, Joan (16 de diciembre de 2022). "Lógica intuicionista". En Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .