Lo que puede ser demostrado en la aritmética de Peano, pero no Heyting aritmética?

Question

Hola. Voy a confesar desde el principio a no ser lógico. De hecho esta pregunta, surgió no de la investigación, pero durante una discusión con un amigo sobre si la clásica prueba de que $\sqrt{2}$ es irracional puede hacerse aceptable a un intuitionist. (Que puede ser.)

La pregunta es: ¿hay alguna "natural" de las declaraciones que pueden ser probados en la Aritmética de Peano, pero no en Heyting Aritmética (Aritmética de Peano, pero con una lógica que no admite la ley del medio excluido)?

De hecho, ninguna de las declaraciones, incluso patológico-que se que puede ser comprobado en uno pero el otro no sería interesante para mí, ya que yo no era capaz de encontrar ninguna. (Incluso después de hacer un par de búsquedas en la web!) Pero, por supuesto, el más cercano a la superficie, mejor.

Answer 1

El primer ejemplo que se me ocurre es (una formalización en el lenguaje de la aritmética, a través de la codificación, de) "Para cada máquina de Turing M y cada entrada x, en el cálculo de M en el input x finaliza o no terminar." Con la lógica clásica, esto es trivialmente comprobable, como una instancia de la ley del medio excluido. Pero no intuitionistically comprobable, porque la detención problema es indecidible. (En un poco más de detalle, si es demostrable, entonces sería realizable de forma recursiva, y el realizer sería un índice para un algoritmo que resuelve el cese problema).

Answer 2

En primer lugar, desde la Aritmética de Peano (PA) es simplemente Heyting Aritmética (HA) con la Ley de Medio Excluido, todo comprobable en HA es demostrable en PA. La negativa de la traducción puede ser utilizado para transformar cada declaración de $\phi$ en una declaración de $\phi^N$ tales que (1) PA demuestra que $\phi$ e $\phi^N$ son lógicamente equivalentes, y (2) PA demuestra $\phi$ si y sólo si HA demuestre $\phi^N$. Así que PA y HA están relativamente cerca unos de otros.

Para una declaración demostrable en PA, pero no en HA, considerar la clásica afirmación válida $\forall \bar{x}(p(\bar{x}) \neq 0) \lor \exists \bar{x}(p(\bar{x}) = 0)$ donde $p(\bar{x})$ es un polinomio en las variables $\bar{x} = x_1,\dots,x_n$. En orden para que esto sea demostrable en HA, se debe tener una prueba de $\forall \bar{x}(p(\bar{x}) \neq 0)$ o una prueba de $\exists \bar{x}(p(\bar{x}) = 0)$. Una prueba de lo anterior sería mostrar que el problema de $p(\bar{x}) = 0$ no tiene solución, y una prueba de esto último demuestra que el problema de $p(\bar{x}) = 0$ tiene una solución. Dado que las pruebas son finitos, esto le da un procedimiento eficaz para decidir si la ecuación de Diophantine $p(\bar{x}) = 0$ tiene una solución. Debido a la negativa de la solución de Hilbert del Décimo Problema, sabemos que hay algunos polinomio $p(\bar{x})$ tal que $\forall \bar{x}(p(\bar{x}) \neq 0) \lor \exists \bar{x}(p(\bar{x}) = 0)$ no es comprobable en HA.

Answer 3

Según Harvey Friedman, el siguiente teorema es demostrable en PA, pero no HA:

Cada polinomio $P:\mathbb{Z}^n \to \mathbb{Z}^m$ con coeficientes enteros supone un valor más cercano al origen.

Es decir, hay un valor que sea al menos tan cerca del origen, en el La distancia euclídea, que cualquier otro valor. Esto es improbable en HECTÁREAS incluso cuando $m=1$.

Answer 4

Una prueba de HECTÁREAS de declaraciones como $\forall m\forall x (\exists y T(m,x,y) \vee \neg\exists y T(m,x,y))$ es, en sí misma, no es suficiente para extraer las funciones recursivas de resolución de problemas insolubles (que muestran que estas declaraciones no son demostrables en HA).

Se ha sugerido que esto de alguna manera se sigue de la disyunción y de la existencia de propiedades (DP, EP) de HECTÁREAS (véase François comentario'), sin embargo sólo se puede aplicar el DP y el parlamento europeo sobre cerrado declaraciones, mientras que declaraciones como la de arriba tiene un prefijo $\forall m \forall x \cdots$.

Es por eso que en recursiva realizabilidad (Kleene número realizabilty), que extrae las funciones recursivas de intuitionistic aritmética de las pruebas, uno debe asumir una versión formal de la aritmética de la Iglesia de la Tesis, como CT$_0$: $\forall x\exists y A(x,y) \to \exists e\forall x\exists u (T(e,x,u)\wedge A(x,U(u))$, que permite transformar el $\forall\exists$-cuantificador-alternancia de $\forall m\forall x\exists z ((z=0\to\exists y T(m,x,y)) \wedge (z\neq 0 \to \neg\exists y T(m,x,y)))$ a una $\exists\forall$-uno. Ahora, como el resultado es un cerrado declaración se puede aplicar EP para extraer una función recursiva, la solución de un problema insoluble.

Sin embargo, el último argumento podría mostrar que sólo el original de la declaración no es comprobable en HA+CT$_0$, mientras que ser demostrable en PA -- ignorar el hecho de que $\neg$CT$_0$ es demostrable en PA.

De hecho, la declaración de $\neg$CT$_0$ es un ejemplo de una declaración demostrable en PA, pero no es demostrable en HA. El último de la siguiente manera, de la existencia de modelos de HA refutar CT$_0$ (por ex. PA sí mismo).

Por otro lado, un natural de la declaración exigida en la pregunta original, y no estoy seguro de $\neg$CT$_0$ es tan natural.