Aritmética de Heyting

Axiomatización de la aritmética

En lógica matemática , la aritmética de Heyting es una axiomatización de la aritmética de acuerdo con la filosofía del intuicionismo . ^[1] Recibe su nombre en honor a Arend Heyting , quien la propuso por primera vez. ${\displaystyle {\mathsf {HA}}}$

Axiomatización

La aritmética de Heyting se puede caracterizar igual que la teoría de primer orden de la aritmética de Peano , excepto que utiliza el cálculo de predicados intuicionista para la inferencia. En particular, esto significa que el principio de eliminación de la doble negación, así como el principio del tercio excluido , no se cumplen. Nótese que decir que no se cumple exactamente significa que la afirmación del tercio excluido no es automáticamente demostrable para todas las proposiciones; de hecho, muchas de esas afirmaciones todavía son demostrables en y la negación de cualquier disyunción de ese tipo es inconsistente. es estrictamente más fuerte que en el sentido de que todos los teoremas - son también -teoremas. ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {IQC}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {PA}}}$

La aritmética de Heyting comprende los axiomas de la aritmética de Peano y el modelo pretendido es la colección de números naturales . La signatura incluye el cero " " y el sucesor " ", y las teorías caracterizan la adición y la multiplicación. Esto impacta la lógica: Con , es un metateorema que puede definirse como y por lo que es para cada proposición . La negación de es de la forma y por lo tanto una proposición trivial. ${\displaystyle {\mathbb {N} }}$ ${\displaystyle 0}$ ${\displaystyle S}$ ${\displaystyle 1:=S0}$ ${\displaystyle \bot }$ ${\displaystyle 0=1}$ ${\displaystyle \neg P}$ ${\displaystyle P\to \bot }$ ${\displaystyle P}$ ${\displaystyle \bot }$ ${\displaystyle P\to P}$

Para los términos , escriba para . Para un término fijo , la igualdad es verdadera por reflexividad y una proposición es equivalente a . Se puede demostrar que entonces se puede definir como . Esta eliminación formal de disyunciones no era posible en la aritmética recursiva primitiva sin cuantificadores . La teoría se puede extender con símbolos de función para cualquier función recursiva primitiva , haciendo también un fragmento de esta teoría. Para una función total , a menudo se consideran predicados de la forma . ${\displaystyle s\neq t}$ ${\displaystyle \neg (s=t)}$ ${\displaystyle t}$ ${\displaystyle t=t}$ ${\displaystyle P}$ ${\displaystyle (t=t)\to P}$ ${\displaystyle P\lor Q}$ ${\displaystyle \exists n.(n=0\to P)\land (n\neq 0\to Q)}$ ${\displaystyle {\mathsf {PRA}}}$ ${\displaystyle {\mathsf {PRA}}}$ ${\displaystyle f}$ ${\displaystyle f(n)=0}$

Teoremas

Dobles negaciones

Con la explosión válida en cualquier teoría intuicionista, si es un teorema para algún , entonces por definición es demostrable si y solo si la teoría es inconsistente. De hecho, en la aritmética de Heyting la doble negación expresa explícitamente . Para un predicado , un teorema de la forma expresa que es inconsistente descartar que podría ser validado para algún . Constructivamente, esto es más débil que la afirmación de existencia de tal . Una gran parte de la discusión metateórica se ocupará de afirmaciones de existencia demostrables clásicamente. ${\displaystyle \neg \neg P}$ ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle \neg P\to 0=1}$ ${\displaystyle Q}$ ${\displaystyle \neg \neg \exists n.Q(n)}$ ${\displaystyle Q(t)}$ ${\displaystyle t}$ ${\displaystyle t}$

Una doble negación implica . Por lo tanto, un teorema de la forma también siempre proporciona nuevos medios para rechazar de manera concluyente enunciados (también positivos) . ${\displaystyle \neg \neg P}$ ${\displaystyle (\alpha \to \neg P)\to (\alpha \to 0=1)}$ ${\displaystyle \neg \neg P}$ ${\displaystyle \alpha }$

Pruebas de enunciados clásicamente equivalentes

Recordemos que la implicación en puede revertirse clásicamente , y con ello también la de . Aquí la distinción es entre la existencia de contraejemplos numéricos versus conclusiones absurdas al suponer validez para todos los números. Insertar dobles negaciones convierte -teoremas en -teoremas. Más exactamente, para cualquier fórmula demostrable en , la traducción negativa de Gödel–Gentzen clásicamente equivalente de esa fórmula ya es demostrable en . En una formulación, el procedimiento de traducción incluye una reescritura de a El resultado significa que todos los teoremas aritméticos de Peano tienen una prueba que consiste en una prueba constructiva seguida de una reescritura lógica clásica. Aproximadamente, el paso final equivale a aplicaciones de eliminación de dobles negaciones. ${\displaystyle {\mathsf {HA}}\vdash \alpha \to \neg \neg \alpha }$ ${\displaystyle {\mathsf {HA}}\vdash {\big (}\exists n.\neg \psi (n){\big )}\to \neg \forall n.\psi (n)}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\big (}\exists n.Q(n){\big )}^{N}}$ ${\displaystyle \neg \forall n.\neg Q^{N}(n).}$

En particular, al no existir proposiciones atómicas indecidibles, para cualquier proposición que no incluya cuantificaciones existenciales o disyunciones, se tiene . ${\displaystyle \psi }$ ${\displaystyle {\mathsf {PA}}\vdash \psi \iff {\mathsf {HA}}\vdash \psi }$

Principios y reglas válidos

La lógica mínima demuestra la eliminación de la doble negación para fórmulas negadas. En términos más generales, la aritmética de Heyting demuestra esta equivalencia clásica para cualquier fórmula de Harrop . ${\displaystyle \neg \neg (\neg \alpha )\leftrightarrow (\neg \alpha )}$

Y los resultados también se comportan bien: la regla de Markov en el nivel más bajo de la jerarquía aritmética es una regla de inferencia admisible , es decir, para con libre, ${\displaystyle \Sigma _{1}^{0}}$ ${\displaystyle \varphi }$ ${\displaystyle n}$

${\displaystyle {\mathsf {HA}}\vdash \neg \neg \exists m.\varphi (n,m)\iff {\mathsf {HA}}\vdash \exists m.\varphi (n,m)}$

En lugar de hablar de predicados libres de cuantificadores, se puede formular esto de manera equivalente para el predicado recursivo primitivo o el predicado T de Kleene , llamado , respectivamente y . Incluso es admisible la regla relacionada , en la que el aspecto de manejabilidad de no se basa, por ejemplo, en una condición sintáctica, sino donde el lado izquierdo también requiere . ${\displaystyle {\mathrm {MR} }_{\mathrm {QF} }}$ ${\displaystyle {\mathrm {MR} _{\mathrm {PR} }}}$ ${\displaystyle {\mathrm {MR} _{0}}}$ ${\displaystyle {\mathrm {MR} }_{\mathrm {Dec} }}$ ${\displaystyle \varphi }$ ${\displaystyle \vdash \forall m.\varphi (n,m)\lor \neg \varphi (n,m)}$

Hay que tener en cuenta que al clasificar una proposición en función de su forma sintáctica, no se debe asignar erróneamente una complejidad menor basándose únicamente en alguna equivalencia clásica válida.

Exclusión intermedia

Al igual que con otras teorías sobre la lógica intuicionista, se pueden probar varias instancias de en esta aritmética constructiva. Por introducción de disyunción , siempre que se pruebe la proposición o , entonces también se prueba. Así, por ejemplo, equipado con y a partir de los axiomas, se puede validar la premisa para la inducción del tercero excluido para el predicado . Entonces se dice que la igualdad a cero es decidible. De hecho, demuestra que la igualdad " " es decidible para todos los números, es decir . Más fuerte aún, como la igualdad es el único símbolo de predicado en la aritmética de Heyting, se sigue entonces que, para cualquier fórmula sin cuantificadores , donde son las variables libres , la teoría está cerrada bajo la regla ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle P\lor \neg P}$ ${\displaystyle 0=0}$ ${\displaystyle \forall n.Sn\neq 0}$ ${\displaystyle n=0}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle =}$ ${\displaystyle \forall n.\forall m.(n=m\lor n\neq m)}$ ${\displaystyle \phi }$ ${\displaystyle n,\dots ,m}$

${\displaystyle {\mathsf {HA}}\vdash \forall n.\cdots \forall m.\,\phi (n,\dots ,m)\lor \neg \phi (n,\dots ,m)}$

Toda teoría basada en la lógica mínima se aplica a todas las proposiciones. Por lo tanto, si la teoría es consistente, nunca se puede probar la negación de una proposición de tercero excluido. ${\displaystyle \neg \neg (P\lor \neg P)}$

En términos prácticos, en marcos constructivos más bien conservadores como , cuando se entiende qué tipo de enunciados son decidibles algorítmicamente, entonces un resultado de improbabilidad de una disyunción intermedia excluida expresa la indecidibilidad algorítmica de . ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle P}$

Conservatividad

Para enunciados simples, la teoría no solo valida esas dicotomías binarias clásicamente válidas . La traducción de Friedman se puede utilizar para establecer que todos los teoremas de se prueban mediante : Para cualquier y sin cuantificadores , ${\displaystyle \phi (n,\dots )\lor \neg \phi (n,\dots )}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \Pi _{2}^{0}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle n}$ ${\displaystyle \varphi }$

${\displaystyle {\mathsf {PA}}\vdash \exists m.\varphi (n,m)\iff {\mathsf {HA}}\vdash \exists m.\varphi (n,m)}$

Este resultado puede, por supuesto, expresarse también con clausuras universales explícitas . En líneas generales, las afirmaciones simples sobre relaciones computables que se pueden demostrar clásicamente ya se pueden demostrar de manera constructiva. Aunque en los problemas de detención , no solo las proposiciones libres de cuantificadores sino también las proposiciones - desempeñan un papel importante, y como se argumentará, estas pueden ser incluso clásicamente independientes. De manera similar, la existencia ya única en un dominio infinito, es decir , no es formalmente particularmente simple. ${\displaystyle \forall n}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle \exists !n.Q(n)}$ ${\displaystyle \exists n.\forall w.{\big (}n=w\leftrightarrow Q(w){\big )}}$

Por lo tanto, -conservativa sobre . Por el contrario, mientras que la teoría clásica de la aritmética de Robinson prueba todos los teoremas - , algunos teoremas - simples son independientes de ella. La inducción también juega un papel crucial en el resultado de Friedman : por ejemplo, la teoría más viable obtenida al reforzar con axiomas sobre ordenación y, opcionalmente, igualdad decidible, prueba más enunciados - que su contraparte intuicionista. ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \Pi _{2}^{0}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {Q}}}$ ${\displaystyle \Sigma _{1}^{0}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {Q}}}$ ${\displaystyle \Pi _{2}^{0}}$

El análisis que se presenta aquí no pretende ser exhaustivo. Existen diversos resultados para cuando un teorema clásico ya está implícito en la teoría constructiva. También cabe señalar que puede ser relevante qué lógica se utilizó para obtener resultados metalógicos. Por ejemplo, muchos resultados sobre realizabilidad se obtuvieron de hecho en una metalógica constructiva. Pero cuando no se da un contexto específico, es necesario suponer que los resultados indicados son clásicos.

Afirmaciones indemostrables

Los resultados de independencia se refieren a proposiciones tales que ni ellas ni sus negaciones pueden ser probadas en una teoría. Si la teoría clásica es consistente (es decir, no prueba ) y la contraparte constructiva no prueba uno de sus teoremas clásicos , entonces esa es independiente de este último. Dadas algunas proposiciones independientes, es fácil definir más a partir de ellas, especialmente en un marco constructivo. ${\displaystyle \bot }$ ${\displaystyle P}$ ${\displaystyle P}$

La aritmética de Heyting tiene la propiedad de disyunción : Para todas las proposiciones y , ^[2] ${\displaystyle {\mathrm {DP} }}$ ${\displaystyle \alpha }$ ${\displaystyle \beta }$

${\displaystyle {\mathsf {HA}}\vdash \alpha \lor \beta \iff {\mathsf {HA}}\vdash \alpha {\text{ or }}{\mathsf {HA}}\vdash \beta }$

De hecho, esto y su generalización numérica también se exhiben en la aritmética constructiva de segundo orden y en las teorías de conjuntos comunes como y . Es un desideratum común para la noción informal de una teoría constructiva. Ahora bien, en una teoría con , si una proposición es independiente , entonces la clásicamente trivial es otra proposición independiente, y viceversa. Un esquema no es válido si hay al menos una instancia que no se puede probar, que es como llega a fallar. Uno puede romper adoptando una declaración de tercero excluido axiomáticamente sin validar ninguno de los disyuntos, como es el caso en . ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {IZF}}}$ ${\displaystyle {\mathrm {DP} }}$ ${\displaystyle P}$ ${\displaystyle P\lor \neg P}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {DP} }}$ ${\displaystyle {\mathsf {PA}}}$

Se puede decir más: si es incluso clásicamente independiente, entonces también la negación es independiente, esto se cumple independientemente de si es equivalente o no a . Entonces, constructivamente, el tercio débil excluido no se cumple, es decir, el principio que se cumpliría para todas las proposiciones no es válido. Si es , la imposibilidad de demostrar la disyunción manifiesta la ruptura de - , o lo que equivale a una instancia de para una función recursiva primitiva. ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle \neg \neg P}$ ${\displaystyle P}$ ${\displaystyle {\mathrm {WPEM} }}$ ${\displaystyle \neg \alpha \lor \neg \neg \alpha }$ ${\displaystyle P}$ ${\displaystyle \Sigma _{1}^{0}}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {WLPO} }}$

Proposiciones clásicamente independientes

El conocimiento de los teoremas de incompletitud de Gödel ayuda a comprender el tipo de enunciados que son demostrables pero no demostrables. ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {HA}}}$

La resolución del décimo problema de Hilbert proporcionó algunos polinomios concretos y ecuaciones polinómicas correspondientes , de modo que la afirmación de que estas últimas tienen una solución es algorítmicamente indecidible . La proposición puede expresarse como ${\displaystyle f}$

${\displaystyle \exists w_{1}.\cdots \exists w_{n}.f(w_{1},\dots ,w_{n})=0}$

Algunas de estas afirmaciones de existencia de valor cero tienen una interpretación más particular: teorías como o demuestran que estas proposiciones son equivalentes a la afirmación aritmetizada de la propia inconsistencia de las teorías. Por lo tanto, tales proposiciones pueden incluso ser escritas para teorías de conjuntos clásicas fuertes. ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {ZFC}}}$

En una teoría aritmética coherente y sólida, tal afirmación de existencia es una proposición independiente. Entonces , al introducir una negación a través del cuantificador, se ve que es una proposición independiente de tipo Goldbach , o . Para ser explícito, la doble negación (o ) también es independiente. Y cualquier triple negación es, en cualquier caso, ya intuicionistamente equivalente a una negación simple. ${\displaystyle {\mathrm {I} _{f}}}$ ${\displaystyle \Sigma _{1}^{0}}$ ${\displaystyle {\mathrm {C} _{f}}:=\neg {\mathrm {I} _{f}}}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle \neg \neg {\mathrm {I} _{f}}}$ ${\displaystyle \neg {\mathrm {C} _{f}}}$

PA viola el PD

Lo que sigue ilustra el significado involucrado en tales afirmaciones independientes. Dado un índice en una enumeración de todas las pruebas de una teoría, se puede inspeccionar de qué proposición es una prueba. es adecuado en el sentido de que puede representar correctamente este procedimiento: hay un predicado recursivo primitivo que expresa que una prueba es una de las proposiciones absurdas . Esto se relaciona con el predicado aritmético más explícito anterior, sobre el valor de retorno de un polinomio que es cero. Se puede razonar metalógicamente que si es consistente, entonces de hecho se prueba para cada índice individual . ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \mathrm {F} (w):=\mathrm {Prf} (w,\ulcorner 0=1\urcorner )}$ ${\displaystyle 0=1}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \neg \mathrm {F} ({\underline {\mathrm {w} }})}$ ${\displaystyle {\mathrm {w} }}$

En una teoría efectivamente axiomatizada, se puede realizar sucesivamente una inspección de cada prueba. Si una teoría es efectivamente consistente, entonces no existe una prueba de un absurdo, lo que corresponde a la afirmación de que la mencionada "búsqueda del absurdo" nunca se detendrá. Formalmente en la teoría, lo primero se expresa mediante la proposición , que niega la afirmación de inconsistencia aritmetizada. La proposición equivalente - formaliza la nunca detención de la búsqueda al afirmar que todas las pruebas no son una prueba de un absurdo. Y de hecho, en una teoría omega-consistente que represente con precisión la demostrabilidad, no hay prueba de que la búsqueda del absurdo alguna vez concluya deteniéndose (inconsistencia explícita no derivable), ni tampoco -como lo muestra Gödel- puede haber una prueba de que la búsqueda del absurdo nunca se detenga (consistencia no derivable). Reformulado, no hay prueba de que la búsqueda del absurdo nunca se detenga (la consistencia no es derivable), ni hay prueba de que la búsqueda del absurdo nunca se detenga (la consistencia no es rechazable). Para reiterar, ninguno de estos dos disyuntos es -demostrable, mientras que su disyunción es trivialmente -demostrable. De hecho, si es consistente entonces viola . ${\displaystyle \neg \exists w.\mathrm {F} (w)}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle \forall w.\neg \mathrm {F} (w)}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathrm {DP} }}$

La proposición - que expresa la existencia de una prueba de es una afirmación lógicamente positiva. No obstante, históricamente se denota , mientras que su negación es una proposición - denotada por . En un contexto constructivo, este uso del signo de negación puede ser una nomenclatura engañosa. ${\displaystyle \Sigma _{1}^{0}}$ ${\displaystyle 0=1}$ ${\displaystyle \neg {\mathrm {Con} }_{\mathsf {PA}}}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathrm {Con} }_{\mathsf {PA}}}$

Friedman estableció otra afirmación interesante e indemostrable: una teoría consistente y adecuada nunca prueba su propiedad de disyunción aritmetizada.

Principios clásicos indemostrables

La lógica mínima ya prueba lógicamente todas las afirmaciones de no contradicción, y en particular y . Dado que también , el teorema puede leerse como una disyunción de tercio excluido doblemente negada demostrable (o afirmación de existencia). Pero a la luz de la propiedad de disyunción, el tercio excluido simple no puede ser -demostrable. Por lo tanto, una de las leyes de De Morgan tampoco puede cumplirse intuicionistamente en general. ${\displaystyle \neg ({\mathrm {I} _{f}}\land \neg {\mathrm {I} _{f}})}$ ${\displaystyle \neg ({\mathrm {C} _{f}}\land \neg {\mathrm {C} _{f}})}$ ${\displaystyle ({\mathrm {C} _{f}}\land \neg {\mathrm {C} _{f}})\leftrightarrow \neg ({\mathrm {I} _{f}}\lor \neg {\mathrm {I} _{f}})}$ ${\displaystyle \neg ({\mathrm {C} _{f}}\land \neg {\mathrm {C} _{f}})}$ ${\displaystyle {\mathrm {C} _{f}}\lor \neg {\mathrm {C} _{f}}}$ ${\displaystyle {\mathsf {HA}}}$

Se ha explicado la descomposición de los principios y . Ahora bien, en , el principio del número mínimo es solo una de las muchas afirmaciones equivalentes al principio de inducción. La prueba a continuación muestra cómo implica , y por lo tanto por qué este principio tampoco puede ser generalmente válido en . Sin embargo, el esquema que concede la existencia del número mínimo doblemente negado para cada predicado no trivial, denotado , es generalmente válido. A la luz de la prueba de Gödel, la descomposición de estos tres principios puede entenderse como la aritmética de Heyting siendo consistente con la lectura de demostrabilidad de la lógica constructiva. ${\displaystyle {\mathrm {WPEM} }}$ ${\displaystyle {\mathrm {WLPO} }}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathrm {LNP} }}$ ${\displaystyle {\mathrm {LNP} }}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle \neg \neg {\mathrm {LNP} }}$

El principio de Markov para predicados recursivos primitivos no se cumple como esquema de implicación para , y mucho menos para el estrictamente más fuerte . Aunque en la forma de las reglas correspondientes, son admisibles, como se mencionó. De manera similar, la teoría no prueba la independencia del principio de premisa para predicados negados, aunque está cerrada bajo la regla para todas las proposiciones negadas, es decir, se puede extraer el cuantificador existencial en . Lo mismo se aplica a la versión en la que el enunciado existencial se reemplaza por una mera disyunción. ${\displaystyle {\mathrm {MP} _{\mathrm {PR} }}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {MP} _{\mathrm {Dec} }}}$ ${\displaystyle {\mathrm {IP} }}$ ${\displaystyle \neg P\to \exists n.Q(n)}$

Se puede demostrar que la implicación válida también se cumple en su forma inversa, utilizando el silogismo disyuntivo. Sin embargo, el desplazamiento de la doble negación no es demostrable intuicionistamente, es decir, el esquema de conmutatividad de " " con cuantificación universal sobre todos los números. Esta es una descomposición interesante que se explica por la consistencia de para algunos , como se analiza en la sección sobre la tesis de Church. ${\displaystyle \neg \neg (\alpha \to \beta )\to (\alpha \to \neg \neg \beta )}$ ${\displaystyle {\mathrm {DNS} }}$ ${\displaystyle \neg \neg }$ ${\displaystyle \neg {\mathrm {Dec} _{M}}}$ ${\displaystyle M}$

Principio del número mínimo

Haciendo uso de la relación de orden en los naturales, el principio de inducción fuerte se lee

${\displaystyle \forall n.{\Big (}{\big (}\forall (k<n).\phi (k){\big )}\,\to \,\phi (n){\Big )}\,\to \,\forall m.\phi (m)}$

En la notación de clases, como es familiar en la teoría de conjuntos, un enunciado aritmético se expresa como donde . Para cualquier predicado dado de forma negada, es decir , un equivalente lógico a la inducción es ${\displaystyle Q(n)}$ ${\displaystyle n\in B}$ ${\displaystyle B:=\{m\in {\mathbb {N} }\mid Q(m)\}}$ ${\displaystyle \phi (n):=\neg (n\in B)}$

${\displaystyle \neg \exists (n\in B).\neg \exists (k\in B).k<n\,\,\,\leftrightarrow \,\,\,B=\{\}}$

La idea es que entre las subclases , la propiedad de no tener (demostrablemente) el miembro más pequeño es equivalente a estar deshabitada, es decir, a ser la clase vacía. Tomando el contrapositivo resulta un teorema que expresa que para cualquier subclase no vacía, no se puede descartar consistentemente que exista un miembro tal que no haya ningún miembro más pequeño que : ${\displaystyle B\subseteq {\mathbb {N} }}$ ${\displaystyle n\in B}$ ${\displaystyle k\in B}$ ${\displaystyle n}$

${\displaystyle B\neq \{\}\,\to \,\neg \neg \exists (n\in B).\neg \exists (k\in B).k<n}$

En la aritmética de Peano, donde la eliminación por doble negación es siempre válida, esto demuestra el principio del número mínimo en su formulación común. En la lectura clásica, no estar vacío es equivalente a estar (demostrablemente) habitado por algún miembro mínimo.

Una relación binaria " " que valida el esquema de inducción fuerte en la forma anterior es siempre también irreflexiva: Considerando o equivalentemente ${\displaystyle <}$ ${\displaystyle \phi _{c}(n):=(n\neq c)}$

${\displaystyle Q_{c}(n):=(n=c)}$

para algún número fijo , lo anterior se simplifica a la afirmación de que ningún miembro de valida , es decir . (Y esta deducción lógica ni siquiera utilizó ninguna otra propiedad de la relación binaria). De manera más general, si no está vacío y el principio del mínimo número asociado (clásico) se puede utilizar para demostrar algún enunciado de forma negada (como ), entonces se puede extender esto a una prueba completamente constructiva. Esto se debe a que las implicaciones son siempre intuicionistamente equivalentes a la formalmente más fuerte . ${\displaystyle c}$ ${\displaystyle k}$ ${\displaystyle B=\{c\}}$ ${\displaystyle k<c}$ ${\displaystyle \neg (c<c)}$ ${\displaystyle B}$ ${\displaystyle \neg (c<c)}$ ${\displaystyle \alpha \to \neg \beta }$ ${\displaystyle (\neg \neg \alpha )\to \neg \beta }$

Pero en general, sobre la lógica constructiva, el debilitamiento del principio del mínimo número no puede ser eliminado. El siguiente ejemplo lo demuestra: para alguna proposición (por ejemplo, como la anterior), considere el predicado ${\displaystyle P}$ ${\displaystyle {\mathrm {C} _{f}}}$

${\displaystyle Q_{P}(n):=(n=0\land P)\lor (n=1)}$

Esto corresponde a una subclase de los números naturales. Uno puede preguntarse cuál puede ser el miembro más pequeño de esta clase. Cualquier número probado o asumido que está en esta clase es demostrablemente igual o , es decir . Usando la decidibilidad de la igualdad y el silogismo disyuntivo se prueba la equivalencia . Si la proposición subyacente es independiente, entonces el predicado es indecidible en la teoría. Ahora bien, dado que , la proposición es trivialmente verdadera y por lo tanto la clase está habitada : . En particular, la existencia del número más pequeño para esta clase no puede rechazarse. Dado que una conjunción con es trivial, la afirmación de existencia de un número más pequeño que se valida a sí misma se traduce en la afirmación del medio excluido para . El conocimiento del valor de tal número de hecho determina si se cumple o no. Entonces, para independiente , la instancia del principio del número más pequeño con también es independiente de . ${\displaystyle Q_{P}}$ ${\displaystyle b_{P}:=\{z\in \{0\}\mid P\}\cup \{1\}}$ ${\displaystyle 0}$ ${\displaystyle 1}$ ${\displaystyle b_{P}\subseteq \{0,1\}}$ ${\displaystyle P\leftrightarrow Q_{P}(0)}$ ${\displaystyle P}$ ${\displaystyle 1=1}$ ${\displaystyle Q_{P}(1)}$ ${\displaystyle 1\in b_{P}}$ ${\displaystyle Q_{P}(1)}$ ${\displaystyle Q_{P}}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle Q_{P}}$ ${\displaystyle {\mathsf {HA}}}$

En la notación de la teoría de conjuntos, es equivalente a y por lo tanto , mientras que su negación también es equivalente a . Esto demuestra que los predicados elusivos pueden definir subconjuntos elusivos. Y por lo tanto también en la teoría de conjuntos constructiva , mientras que el orden estándar en la clase de los naturales es decidible, los naturales no están bien ordenados . Pero los principios de inducción fuerte, que constructivamente no implican afirmaciones de existencia irrealizables, también siguen estando disponibles. ${\displaystyle P}$ ${\displaystyle 0\in b_{P}}$ ${\displaystyle b_{P}=\{0,1\}}$ ${\displaystyle b_{P}=\{1\}}$

Extensiones anticlásicas

En un contexto computable, para un predicado , la disyunción infinita clásicamente trivial ${\displaystyle M}$

${\displaystyle \forall n.{\big (}M(n)\lor \neg M(n){\big )}}$,

También se escribe , y puede leerse como una validación de la decidibilidad de un problema de decisión . En la notación de clase, también se escribe . ${\displaystyle {\mathrm {Dec} }_{M}}$ ${\displaystyle M(n)}$ ${\displaystyle n\in M}$

${\displaystyle {\mathsf {HA}}}$no prueba proposiciones que no sean demostrables por y, por lo tanto, en particular, no rechaza ningún teorema de la teoría clásica. Pero también hay predicados tales que los axiomas son consistentes. Nuevamente, constructivamente, tal negación no es equivalente a la existencia de un contraejemplo numérico particular para el tercio excluido para . De hecho, ya la lógica minimal prueba el tercio excluido doblemente negado para todas las proposiciones, y por lo tanto , que es equivalente a , para cualquier predicado . ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle M}$ ${\displaystyle {\mathsf {HA}}+\neg {\mathrm {Dec} }_{M}}$ ${\displaystyle t}$ ${\displaystyle M(t)}$ ${\displaystyle \forall n.\neg \neg {\big (}Q(n)\lor \neg Q(n){\big )}}$ ${\displaystyle \neg \exists n.\neg {\big (}Q(n)\lor \neg Q(n){\big )}}$ ${\displaystyle Q}$

Tesis de la Iglesia

La regla de Church es una regla admisible en . El principio de tesis de Church puede adoptarse en , mientras que lo rechaza: implica negaciones como las que se acaban de describir. ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {CT} _{0}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {PA}}}$

Considere el principio en la forma que establece que todos los predicados que son decidibles en el sentido lógico anterior también son decidibles por una función computable total . Para ver cómo está en conflicto con el tercero excluido, uno solo necesita definir un predicado que no sea computablemente decidible. Para este fin, escriba para predicados definidos a partir del predicado T de Kleene . Los índices de funciones computables totales cumplen . Si bien se puede realizar de manera recursiva primitiva, el predicado en , es decir, la clase de índices de funciones computables parciales con un testigo que describe cómo se detienen en la diagonal, es computablemente enumerable pero no computable . El complemento clásico definido usando ni siquiera es computablemente enumerable, vea el problema de la detención. Este problema demostradamente indecidible proporciona un ejemplo de violación. Para cualquier índice , la forma equivalente expresa que cuando se evalúa la función correspondiente (en ), entonces todas las descripciones concebibles de los historiales de evaluación ( ) no describen la evaluación en cuestión. En concreto, este no ser decidible para funciones establece la negación de lo que equivale a . ${\displaystyle \Delta _{e}(w):=T_{1}(e,e,w)}$ ${\displaystyle e}$ ${\displaystyle \forall x.\exists w.T_{1}(e,x,w)}$ ${\displaystyle T_{1}}$ ${\displaystyle \exists w.\Delta _{e}(w)}$ ${\displaystyle e}$ ${\displaystyle H:=\{e\mid \exists w.\Delta _{e}(w)\}}$ ${\displaystyle M}$ ${\displaystyle \neg \exists w.\Delta _{e}(w)}$ ${\displaystyle e\in M}$ ${\displaystyle e}$ ${\displaystyle \forall w.\neg \Delta _{e}(w)}$ ${\displaystyle e}$ ${\displaystyle w}$ ${\displaystyle {\mathrm {WLPO} }}$

Los principios formales de Church están asociados con la escuela recursiva, naturalmente. El principio de Markov es comúnmente adoptado, por esa escuela y por las matemáticas constructivas en general. En presencia del principio de Church, es equivalente a su forma más débil . Este último generalmente puede expresarse como un solo axioma, a saber, la eliminación de la doble negación para cualquier . La aritmética de Heyting junto con ambos + prueba la independencia de la premisa para predicados decidibles, . Pero no van juntos, consistentemente, con . también niega . La escuela intuicionista de LEJ Brouwer extiende la aritmética de Heyting mediante una colección de principios que niegan ambos así como . ${\displaystyle {\mathrm {MP} _{\mathrm {Dec} }}}$ ${\displaystyle {\mathrm {MP} _{\mathrm {Dec} }}}$ ${\displaystyle {\mathrm {MP} _{\mathrm {PR} }}}$ ${\displaystyle \neg \neg \exists w.T_{1}(e,x,w)}$ ${\displaystyle {\mathrm {MP} _{\mathrm {Dec} }}}$ ${\displaystyle {\mathrm {ECT} _{0}}}$ ${\displaystyle {\mathrm {IP} }_{0}}$ ${\displaystyle {\mathrm {IP} }}$ ${\displaystyle {\mathrm {CT} _{0}}}$ ${\displaystyle {\mathrm {DNS} }}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {CT} _{0}}}$

Modelos

Consistencia

Si una teoría es consistente, entonces ninguna prueba es absurda. Kurt Gödel introdujo la traducción negativa y demostró que si la aritmética de Heyting es consistente, entonces también lo es la aritmética de Peano. Es decir, redujo la tarea de consistencia para a la de . Sin embargo, los teoremas de incompletitud de Gödel, acerca de la incapacidad de ciertas teorías para demostrar su propia consistencia, también se aplican a la propia aritmética de Heyting. ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {HA}}}$

El modelo estándar de la teoría clásica de primer orden , así como cualquiera de sus modelos no estándar, es también un modelo para la aritmética de Heyting . ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {HA}}}$

Teoría de conjuntos

También hay modelos de teoría de conjuntos constructivos para la semántica completa y su semántica prevista. Las teorías de conjuntos relativamente débiles son suficientes: adoptarán el axioma de infinito , el esquema axiomático de separación predicativa para demostrar la inducción de fórmulas aritméticas en , así como la existencia de espacios de funciones en dominios finitos para definiciones recursivas . Específicamente, esas teorías no requieren , el axioma completo de separación o inducción de conjuntos (y mucho menos el axioma de regularidad ), ni espacios de funciones generales (y mucho menos el axioma completo de conjunto potencia ). ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle \omega }$ ${\displaystyle {\mathrm {PEM} }}$

${\displaystyle {\mathsf {HA}}}$Además, es biinterpretable con una teoría de conjuntos constructiva débil en la que la clase de ordinales es , de modo que la colección de naturales de von Neumann no existe como un conjunto en la teoría. ^{[3] [4]} Metateóricamente, el dominio de esa teoría es tan grande como la clase de sus ordinales y esencialmente dado a través de la clase de todos los conjuntos que están en biyección con un natural . Como axioma, esto se llama y los otros axiomas son aquellos relacionados con el álgebra de conjuntos y el orden: Unión e Intersección Binaria, que está estrechamente relacionada con el esquema de Separación Predicativa, Extensionalidad, Emparejamiento y el esquema de Inducción de Conjuntos . Esta teoría es entonces ya idéntica a la teoría dada por sin Infinitud Fuerte y con el axioma de finitud agregado. La discusión de en esta teoría de conjuntos es como en la teoría de modelos. Y en la otra dirección, los axiomas teóricos de conjuntos se prueban con respecto a la relación recursiva primitiva ${\displaystyle \omega }$ ${\displaystyle {\mathrm {Fin} }}$ ${\displaystyle n\in \omega }$ ${\displaystyle V={\mathrm {Fin} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {HA}}}$

${\displaystyle x\in y\iff \exists (r<2^{x}).\exists (s<y).{\big (}2^{x}(2s+1)+r=y{\big )}}$

Ese pequeño universo de conjuntos puede entenderse como la colección ordenada de secuencias binarias finitas que codifican su pertenencia mutua. Por ejemplo, el conjunto '-ésimo contiene otro conjunto y el conjunto '-ésimo contiene otros cuatro conjuntos. Véase predicado BIT . ${\displaystyle 100_{2}}$ ${\displaystyle 110101_{2}}$

Realizabilidad

Para algún número en la metateoría, el numeral en la teoría del objeto estudiado se denota por . ${\displaystyle \mathrm {n} }$ ${\displaystyle {\underline {\mathrm {n} }}}$

En aritmética intuicionista, la propiedad de disyunción es normalmente válida. Y es un teorema que cualquier extensión de la aritmética para la que se cumple también tiene la propiedad de existencia numérica : ${\displaystyle {\mathrm {DP} }}$ ${\displaystyle {\mathrm {NEP} }}$

${\displaystyle {\mathsf {HA}}\vdash \exists n.\psi (n)\iff {\text{ exists }}{\mathrm {n} }{\text{ }}{\mathsf {HA}}\vdash \psi ({\underline {\mathrm {n} }})}$

Por lo tanto, estas propiedades son equivalentes metalógicamente en la aritmética de Heyting. La propiedad de existencia y disyunción de hecho sigue siendo válida cuando se relativiza la afirmación de existencia mediante una fórmula de Harrop , es decir, para demostrable . ${\displaystyle \alpha }$ ${\displaystyle \alpha \to \exists n.\psi (n)}$

Kleene , un estudiante de Church , introdujo importantes modelos de realizabilidad de la aritmética de Heyting. A su vez, su estudiante Nels David Nelson estableció (en una extensión de ) que todos los teoremas cerrados de (lo que significa que todas las variables están acotadas) pueden realizarse. La inferencia en la aritmética de Heyting preserva la realizabilidad. Además, si entonces hay una función recursiva parcial que se realiza en el sentido de que siempre que la función evaluada en termina con , entonces . Esto se puede extender a cualquier número finito de argumentos de función . También hay teoremas clásicos que no son -demostrables pero que sí tienen una realización. ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {HA}}\vdash \forall n.\exists m.\varphi (n,m)}$ ${\displaystyle \varphi }$ ${\displaystyle {\mathrm {n} }}$ ${\displaystyle {\mathrm {m} }}$ ${\displaystyle {\mathsf {HA}}\vdash \varphi ({\underline {\mathrm {n} }},{\underline {\mathrm {m} }})}$ ${\displaystyle {\mathrm {n} }}$ ${\displaystyle {\mathsf {HA}}}$

Georg Kreisel introdujo versiones tipificadas de la realizabilidad , con las que demostró la independencia del principio de Markov, válido clásicamente, para las teorías intuicionistas.

Véase también interpretación de BHK e interpretación de Dialéctica .

En el topos efectivo , ya el subsistema axiomizable finito de la aritmética de Heyting con inducción restringida a es categórico . La categoricidad aquí recuerda al teorema de Tennenbaum . El modelo es válido pero no válido y, por lo tanto, la completitud falla en este contexto. ${\displaystyle \Sigma _{1}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {PA}}}$

Teoría de tipos

Se han implementado en varios lenguajes realizaciones teóricas de tipos que reflejan formalizaciones lógicas basadas en reglas de inferencia .

Extensiones

Se ha analizado la aritmética de Heyting con símbolos de función potenciales añadidos para funciones recursivas primitivas. Esa teoría prueba la función total de Ackermann.

Más allá de esto, la selección de axiomas y formalismos siempre ha sido un debate incluso dentro del círculo constructivista. Muchas extensiones tipificadas de han sido ampliamente estudiadas en la teoría de la prueba , por ejemplo, con tipos de funciones entre números y funciones entre ellos, etc. Las formalidades naturalmente se vuelven más complicadas, con diferentes axiomas posibles que gobiernan la aplicación de funciones. La clase de funciones que son totales se puede enriquecer de esta manera. La teoría con tipos finitos cuando se combina además con la extensionalidad de funciones más un axioma de elección en todavía prueba las mismas fórmulas aritméticas que antes y tiene una interpretación de teoría de tipos. Sin embargo, esa teoría rechaza la tesis de Church para así como que todas las funciones en serían continuas. Pero adoptando, digamos, diferentes reglas de extensionalidad, axiomas de elección, principios de Markov y de independencia e incluso el lema de König —todos juntos pero cada uno con una fuerza o niveles específicos— uno puede definir aritméticas bastante "rellenas" que todavía pueden fallar en probar el medio excluido a nivel de fórmulas. Desde el principio también se investigaron variantes con igualdad intensional y secuencia de elección brouweriana . ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {HA}}^{\omega }}$ ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$ ${\displaystyle {\mathbb {N} }^{\mathbb {N} }\to {\mathbb {N} }}$ ${\displaystyle \Pi _{1}^{0}}$

Se han realizado estudios de matemática inversa de aritmética constructiva de segundo orden. ^[5]

Historia

La axiomatización formal de la teoría se remonta a Heyting (1930), Herbrand y Kleene . Gödel demostró el resultado de consistencia en 1933. ${\displaystyle {\mathsf {PA}}}$

Conceptos relacionados

La aritmética de Heyting no debe confundirse con las álgebras de Heyting , que son el análogo intuicionista de las álgebras de Boole .

Véase también

• Interpretación de BHK
• Análisis constructivo
• Teoría de conjuntos constructivos
• Fórmula de Harrop
• Realizabilidad

Referencias

1. Troelstra 1973:18
2. Sørenson, Morten; Urzyczyn, Paweł (1998), Conferencias sobre el isomorfismo de Curry-Howard , CiteSeerX  10.1.1.17.7385, págs. 240-249
3. Jeon, Hanul (2022), "Interpretación constructiva de Ackermann", Anales de lógica pura y aplicada , 173 (5): 103086, arXiv : 2010.04270 , doi :10.1016/j.apal.2021.103086, S2CID  222271938
4. Shapiro, S., McCarty, C. y Rathjen, M., Conjuntos y números intuicionistas: teoría de conjuntos pequeños y aritmética de Heyting, https://doi.org/10.1007/s00153-024-00935-4, Arch. Math. Logic (2024)
5. Diener, Hannes (2020). "Matemática inversa constructiva". arXiv : 1804.05495 ​​[math.LO].

• Ulrich Kohlenbach (2008), Teoría de la prueba aplicada , Springer.
• Anne S. Troelstra , ed. (1973), Investigación metamatemática de la aritmética y el análisis intuicionista , Springer, 1973.

Enlaces externos

• Enciclopedia de Filosofía de Stanford : "Teoría de números intuicionista" de Joan Moschovakis .
• Fragmentos de la aritmética de Heyting de Wolfgang Burr