Pruebas constructivas y consistencia de los omega

Question

Ese viejo MSE pregunta se analiza la noción de "constructiva" a prueba, y las respuestas explicar que no hay una definición de lo "constructivo" o "no constructiva".

Recientemente, he pensado en la siguiente definición : supongamos que una teoría de la $T$ (al menos tan fuerte como la aritmética de Peano, digamos) es "constructivo" si cada vez que un no constructiva prueba sobre enteros existe, entonces no es un constructiva equivalente, es decir, para cuando $T$ demuestra ("no constructiva") $\exists \ \text{integer } n,\ \phi(n)$ para algunos predicado $\phi$, entonces no es un número entero $n_0$ tal que $T$ demuestra $\phi(n_0)$.

Hay una conexión entre esta noción y $\omega$-consistencia : si $T$ es consistente pero $\omega$-inconsistente, entonces T no es "constructivo". Pero (a menos que me he perdido algo), si sólo sabemos $T$ $\omega$- de acuerdo, no podemos saber de antemano si $T$ será constructiva o no.

Se sabe si PA,ZF o ZFC son "constructivas" en este sentido ?

Answer 1

PA no es constructivo en este sentido. Para nota

$PA \vdash \exists x(\varphi(x) \lor \forall y\neg\varphi(y))$.

Ahora tomemos el caso donde$\varphi(x)$$T(e,e,x)$, lo cual expresa la relación que mantiene al $x$ códigos de los pasos en una paralización de la computación por la máquina de Turing número $e$ en la entrada de $e$. Este Kleene relación es decidable, y de hecho es expresable en el lenguaje de la $PA$. Si, por $e$, siempre hubo un número $n$ tal que

$PA \vdash (T(e, e, n) \lor \forall y\neg T(e, e, y))$,

entonces podríamos hacer una nueva búsqueda para $n$ $e$ enumerando $PA$ pruebas, y luego decidir si $T(e,e,n)$ se decidirá si la máquina de Turing $e$ se detiene en la entrada de $e$, asumiendo $PA$ es el sonido. Pero sabemos que la detención problema es indecidible.

Answer 2

Esta propiedad se denomina la "propiedad de existencia numérica". Es común en sistemas constructivos y rara en sistemas con lógica clásica. Hay un artículo en la Wikipedia que muestra varias referencias.