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).
Propiedad de disyunción
La propiedad de disyunción se satisface mediante una teoría si, siempre que una oración A ∨ B es un teorema , entonces A es un teorema o B es un teorema.
Propiedad de existencia
La propiedad de existencia o propiedad de testigo es satisfecha 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 ) .
Propiedades relacionadas
Rathjen (2005) enumera cinco propiedades que puede poseer una teoría. Estos incluyen la propiedad de disyunción ( DP ), la propiedad de existencia ( EP ) y tres propiedades adicionales:
- La propiedad de existencia numérica (NEP) establece que si la teoría prueba, donde φ no tiene otras variables libres, entonces la teoría demuestra para algunos Aquí es un término en que representa el número n .
- La regla de Church (CR) establece que si la teoría pruebaentonces hay un número natural e tal que, dejandoser la función computable con índice e , la teoría demuestra.
- Una variante de la regla de Church, CR 1 , establece que si la teoría pruebaentonces hay un número natural e tal que la teoría prueba es total y prueba .
Estas propiedades solo pueden expresarse directamente para las teorías que tienen la capacidad de cuantificar sobre números naturales y, para CR 1 , 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 definitoria de la teoría tiene la propiedad mencionada anteriormente (Rathjen 2005).
Antecedentes e historia
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 probado 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 la realizabilidad , que ahora es uno de los principales métodos en el estudio de las teorías constructivas (Kohlenbach 2008; Troelstra 1973).
Si bien los primeros resultados fueron para las teorías constructivas de la aritmética, muchos resultados también son conocidos para las teorías de conjuntos constructivos (Rathjen 2005). John Myhill (1973) mostró que IZF con el axioma de reemplazo eliminado a 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 CZF tiene la propiedad de disyunción y la propiedad de existencia numérica.
La mayoría de las teorías clásicas, como la aritmética de Peano y la ZFC , no tienen la propiedad de existencia o disyunción. Algunas teorías clásicas, como ZFC más el axioma de constructibilidad , tienen una forma más débil de la propiedad de existencia (Rathjen 2005).
En topoi
Freyd y Scedrov (1990) observaron que la propiedad de disyunción se mantiene en álgebras de Heyting libres y topoi 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 adecuados. Junto con la propiedad de existencia, se traduce en la afirmación de quees un objeto proyectivo indecomponible: el funtor que representa (el funtor de sección global) conserva epimorfismos y coproductos .
Relaciones
Hay varias relaciones entre las cinco propiedades discutidas anteriormente.
En el marco de la aritmética, la propiedad de existencia numérica implica la propiedad de disyunción. La prueba utiliza el hecho de que una disyunción se puede reescribir como una fórmula existencial que cuantifica sobre números naturales:
- .
Por tanto, si
- es un teorema de , Asi es .
Por tanto, asumiendo la propiedad de existencia numérica, existe tal que
es un teorema. Desde es un número, se puede comprobar concretamente el valor de : Si luego es un teorema y si luego es un teorema.
Harvey Friedman (1974) demostró que en cualquier extensión recursivamente enumerable de la aritmética intuicionista , la propiedad de disyunción implica la propiedad de existencia numérica. La prueba usa 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 demostrar que una de las disyunciones es demostrable.
Ver también
Referencias
- 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 en Viena , v. 69, págs. 65–66.
- Stephen Cole Kleene, 1945, "Sobre la interpretación de la teoría intuicionista de números", 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, pp. 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 aritmética y análisis intuicionistas , Springer.
enlaces externos
- Lógica intuicionista por Joan Moschovakis, Enciclopedia de Filosofía de Stanford