Ejecución de programas en modelos no estándar de AP

Question

Me he encontrado con el siguiente problema en varios sitios, parafraseando:

Sea $T$ sea una extensión recursivamente axiomatizable y consistente de PA. Entonces existe existe alguna $e$ de forma que $e'$ Programa $\phi_e$ i $T$ no prueba $Tot(e)$ .

La solución suele ser del tipo

Toma $e$ tal que $\phi_e$ es el programa que, para una enumeración efectiva fija del cierre deductivo de $T$ salidas $0$ en la entrada $n$ si el $n$ La sentencia no es $``0=1"$ y diverge en caso contrario. Entonces $T$ es total por la consistencia de $T$ pero por el (segundo) teorema de incompletitud de Godel $T$ no puede demostrar $Tot(e)$ .

No puedo aceptar esta solución. Claramente $Tot(e)$ implicaría la coherencia de $T$ pero ¿por qué $T$ ¿Piensas eso? Si $T$ de alguna manera no demuestra $Tot(e)\rightarrow Con(T)$ entonces todavía no tenemos una contradicción al teorema de incompletitud de Godel.

Naturalmente entonces para terminar la solución me gustaría demostrar que $T$ PRUEBA $Tot(e)\rightarrow Con(T)$ . Como soy aprensivo a la hora de abordar la sintaxis y la gramática de prueba, prefiero intentar utilizar el teorema de completitud de Godel para establecer este paso, lo que significa que tengo que empezar a considerar lo que le ocurre a mi programa $\phi_e$ cuando intento ejecutarlo en modelos no estándar.

Ahora bien, me gustaría pensar que los algoritmos descritos explícitamente son lo suficientemente robustos como para funcionar en modelos no estándar. Es decir, cuando se define $\phi_e$ utilizando alguna condición como

$\forall n$ si $\psi(n)$ entonces $\phi_e(n)\uparrow$

entonces $PA$ (o $Q$ ) debe probar la sentencia

$\psi(n)\rightarrow \neg (\phi_e(n)\downarrow)$

Tal vez podría decir que $PA$ es lo suficientemente inteligente como para detectar la divergencia intencionada, o que hay una manera de escribir un programa para divergir intencionadamente que $PA$ puede ver.

Answer 1

Tienes que demostrarlo sintácticamente. Una forma es demostrar el siguiente lema:

Para cada $\Sigma^0_1$ fórmula $A(x_1,\ldots,x_k)$ existe un índice $e$ tal que PA demuestre $$(\forall n_1)\cdots(\forall n_k)[ A(n_1,\ldots,n_k) \leftrightarrow \phi_e(n_1,\ldots,n_k)\downarrow]$$

Esto se demuestra por inducción en la estructura de la fórmula $A$ utilizando la definición de la formalización de " $\phi_e(n_1,\ldots,n_k)\downarrow$ " en PA, que en realidad es el predicado T de Kleene.

Es cierto que si $e,n$ son estándar y el modelo estándar piensa que $\phi_e(n)$ converge, entonces también lo hará cualquier modelo no estándar. Pero un modelo no estándar podría pensar que $\phi_e(n)$ converge (en un número de pasos no estándar), incluso cuando $n$ es estándar, incluso si ese cálculo no converge realmente.

Answer 2

Mi opinión personal es que pensar en "ejecutar programas en modelos no estándar" da una intuición equivocada. Un modelo no estándar simplemente afirma cosas sobre los programas, y algunas de estas afirmaciones no son verificables. En la situación en la que te encuentras, el modelo no estándar afirmará que la máquina de Turing funciona para siempre con alguna entrada. Usted le pregunta "¿qué entrada?" y ella responde " $N$ ." Bueno, eso no fue útil. Pregúntale "¿es $N$ superior a $1000$ ?" y responde "sí". En general se comportará como un oráculo adaptativo respondiendo siempre a sus preguntas de forma que se evite una contradicción, pero sin darle nunca datos suficientes para distinguir $N$ como un entero estándar (porque, por supuesto, no es un entero estándar).

Para cualquier número entero estándar fijo $N$ la afirmación "esta máquina de Turing produce esta salida con la entrada $N$ "es demostrable o refutable en PA, por lo que tiene el mismo valor de verdad en todos los modelos.