Propiedades de disyunción y existencia.

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

Definiciones

• 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 con una teoría si, siempre que una oración (∃ x ) A ( x ) es un teorema, donde A ( x ) no tiene otras variables libres, entonces existe algún término t tal que la teoría prueba En ) .​​

Propiedades relacionadas

Rathjen (2005) enumera cinco propiedades que puede poseer una teoría. Estas 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 prueba para alguna Aquí hay un término para representar 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 se pruebaentonces existe un número natural e tal que,siendo la función computable con índice e , la teoría se prueba. ${\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 entonces existe un número natural e tal que la teoría prueba es total y prueba . ${\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 números naturales y, para CR ₁ , cuantificar funciones desde hasta . 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 indicada anteriormente (Rathjen 2005). ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$

Resultados

No ejemplos y ejemplos

Casi por definición, una teoría que acepta el tercero excluido y al mismo tiempo tiene enunciados independientes no tiene la propiedad de disyunción. Por 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 menor número . Pero 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).

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 fueron para teorías constructivas de la aritmética, también se conocen muchos resultados para teorías constructivas de conjuntos (Rathjen 2005). John Myhill  (1973) demostró que 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 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 álgebras de Heyting libres y topoi libres . En términos categóricos , en el topos libre, 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 indescomponible : el funtor que representa (el funtor de sección global) conserva epimorfismos y coproductos . ${\displaystyle \mathbf {1} }$ ${\displaystyle \mathbf {1} }$

Relación entre propiedades

Existen varias relaciones entre las cinco propiedades analizadas anteriormente.

En el ámbito 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 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 , también lo es . ${\displaystyle T}$ ${\displaystyle \exists n\colon (n=0\to A)\wedge (n\neq 0\to B)}$

Por lo tanto, 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 verificar 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 de existencia numérica. 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, se puede utilizar la eliminación de disyunciones para demostrar que una de las disyunciones es demostrable.

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 es ahora uno de los principales métodos en el estudio de teorías constructivas (Kohlenbach 2008; Troelstra 1973).

Ver también

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

Referencias

• Peter J. Freyd y Andre Scedrov, 1990, Categorías, Alegorías . Holanda del Norte.
• 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 intuicionista de números", Journal of Symbolic Logic , v. 10, págs.
• Ulrich Kohlenbach , 2008, Teoría de la prueba aplicada , Springer.
• John Myhill , 1973, "Algunas propiedades de la teoría intuicionista de conjuntos 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 constructiva de conjuntos 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 intuicionista , Springer.

enlaces externos

• Moschovakis, Joan (16 de diciembre de 2022). "Lógica intuicionista". En Zalta, Edward N. (ed.). Enciclopedia de Filosofía de Stanford .