Contenido de la prueba de consistencia de Gentzen de PA

Question

Es sorprendente la falta de información sobre la prueba de consistencia de Gentzen -por supuesto, hay algunos contenidos sobre la primera prueba de consistencia de Gentzen de los axiomas de Peano, pero no sobre lo que solemos decir prueba de consistencia de Gentzen. De ahí la pregunta: ¿cuáles serían las descripciones aproximadas de la prueba de consistencia de Gentzen?

Con lo que puedo empezar es con esto: lo que Gentzen quería hacer es partir de un sistema más débil que PA para que las afirmaciones de consistencia no sean controvertidas. Pero un sistema más débil no puede probar la consistencia de PA, así que hay que añadir algo, pero hay que asegurarse de que tal adición puede ser bien aceptada y el sistema resultante no es más fuerte que PA. Esa adición es la inducción libre de cuantificadores hasta $\varepsilon_0$ y el sistema utilizado es el ARP.

Así pues, mi pregunta ahora es, ¿cómo se conectarían el ARP y este principio de inducción para establecer una prueba de consistencia? Aunque una buena referencia, preferiblemente existente en Internet, está bien, creo que sería mejor si esta pregunta se responde directamente, ya que puede servir como una buena referencia para otras personas también.

(Además, es un poco difícil para mí ver cómo podemos formar caso base para $n=0$ . ¿Cuál sería el caso base aquí?)

Answer 1

A grandes rasgos, la prueba de Gentzen es la siguiente. Define funciones primitivas recursivas (con respecto a codificaciones estándar) $C$ de las pruebas en PA a los ordinales $<\epsilon_0$ y $E$ de pruebas a pruebas, con las siguientes propiedades, para todas las pruebas $p$ . (1) Si $C(p)>0$ entonces $C(E(p))<C(p)$ . (2) La conclusión de $E(p)$ es la misma que la de $p$ . (3) Si la conclusión de $p$ es $0=1$ entonces $C(p)>0$ . Estas tres propiedades se demuestran mediante razonamientos finitarios formalizables en ARP.

Dada esta información más la propiedad de buen orden de $\epsilon_0$ obtiene la consistencia de PA de la siguiente manera. Supongamos que hubiera una prueba PA de $0=1$ . Entonces podemos generar más pruebas de $0=1$ iterando $E$ : $p_0=p$ y $p_{n+1}=E(p_n)$ . Todos los $p_n$ son pruebas de $0=1$ por (2); $C(p_n)>0$ por (3); y $C(p_{n+1})<C(p_n)$ por (1). Pero una secuencia decreciente infinita de ordinales $C(p_n)$ contradice la hipótesis del buen orden. Así que no puede haber una prueba PA de $0=1$ .

Obsérvese que el buen orden se utilizó sólo en la forma más débil "No existe una secuencia recursiva infinita, decreciente y primitiva en $\epsilon_0$ ."

Un poco más sobre $C$ y $E$ : En los sistemas deductivos utilizados por Gentzen, una regla particular denominada "corte" es responsable de la mayor parte de la complejidad teórica de las pruebas. En particular, es trivial que $0=1$ no puede demostrarse sin utilizar el corte (propiedad (3) anterior). $C(p)$ mide "cuánto" se corta en la prueba $p$ no se trata sólo del número de aplicaciones de la regla de corte en $p$ sino también la complejidad de las fórmulas a las que se aplica esta regla. $E(p)$ es el resultado de un paso en un proceso llamado eliminación de cortes. El proceso completo, como su nombre indica, se deshace de las aplicaciones de la regla de corte en una demostración, manteniendo la corrección y la conclusión de la demostración (propiedad (2) anterior). Un paso del proceso, es decir, $E$ sólo reduce el rango de corte, es decir, la propiedad (1) anterior.