¿Qué axiomas se utilizan para demostrar los Teoremas de Incompletitud de Godel?

Question

Comprendo Teoremas de Incompletitud de Godel para ser declaraciones sobre generado efectivamente sistemas formales , lo que básicamente los convierte en teoremas sobre algoritmos. Esto es genial, porque a pesar de ser muy abstractos, realmente limitan mis expectativas sobre cómo pueden comportarse los ordenadores y los seres humanos. Pero, siendo teoremas, ¿qué sistema formal son los teoremas en ? Es decir, ¿qué lenguaje formal se utiliza para expresarlos, ¿cómo interpretar ese lenguaje como si se tratara de algoritmos, ¿qué axiomas se asumen y qué reglas de inferencia se utilizan para derivar los teoremas de incompletitud?

Lo pregunto porque estoy buscando una respuesta mejor que " ZFC ", que me han dado en persona unas cuantas veces. ZFC se refiere a todo tipo de cosas que no creo que existan (por ejemplo, conjuntos no recursivamente enumerables, funciones de elección para familias incontables...), al menos no de la misma manera que creo en cosas concretas como ordenadores y algoritmos. Veo, al hojear las pruebas, que probablemente podría inventar un sistema formal en el que se pudieran expresar y demostrar los teoremas, que no hiciera referencia a todas las monstruosidades de ZFC. Sólo quiero saber qué sistema(s) formal(es) estándar y "más simple(s)" se puede(n) utilizar para este propósito.

Answer 1

Como señala Andrés Caicedo en su comentario (a la Pregunta), el modesto fragmento $\sf{PRA}$ (Aritmética Recursiva Primitiva) de $\sf{PA}$ (aritmética de Peano) ya es capaz de verificar los teoremas de incompletitud.

De hecho, la demostración de la prueba de incompletitud de Gödel-Rosser es totalmente sintáctica y puede implementarse fácilmente en un fragmento de $\sf{PRA}$ conocido como $I\Delta_0 + exp$ , donde $I\Delta_0$ es el debilitamiento de $PA$ en el que el esquema de inducción sólo está disponible para $\Delta_0$ -fórmulas, y $exp$ afirma la totalidad de la función exponencial $2^x$ (es bien sabido que $I\Delta_0$ es incapaz de demostrar la totalidad de la función exponencial).

Cabe destacar que en el anterior $I\Delta_0 + exp$ puede incluso reducirse a $I\Delta_0 + \Omega_1$ , donde $\Omega_1$ es el axioma que afirma la totalidad de la función $2^{\left| x\right|^2 }$ , donde $\left| x\right|$ denota la longitud de la expansión binaria de $x$ . La teoría $I\Delta_0 + \Omega_1$ es comúnmente visto como el fragmento más débil de $\sf{PA}$ en la que se puede desarrollar una "teoría de la sintaxis" viable.

PS. Como señala Jeřábek, los teoremas de incompletitud pueden aplicarse en sistemas aún más débiles.

Answer 2

Puede que ya lo sepas, pero si buscas fundamentos de las matemáticas que sean tan débiles que no demuestren la existencia de conjuntos no-r.e., entonces deberías estudiar el libro de Simpson Subsistemas de aritmética de segundo orden la "biblia" de matemáticas inversas . El sistema más débil de ese libro, RCA ₀ tiene como modelo los conjuntos recursivos, y es suficiente para el primer teorema de incompletitud de Goedel e incluso para una versión débil del teorema de completitud de Goedel. Más importante aún, RCA ₀ es suficiente para una gran cantidad de matemáticas.

El libro de Simpson, por supuesto, también investiga lo que no puede ser probado en RCA ₀ . Por ejemplo, el teorema del punto fijo de Brouwer es indemostrable en RCA ₀ , a grandes rasgos porque se puede construir un mapa continuo recursivo del cuadrado hacia sí mismo que no tiene punto fijo recursivo.

Answer 3

Esta es una forma diferente de ver las cosas. Utilice FPA para denotar la Aritmética de Peano de segundo orden menos el Axioma del Sucesor (el axioma que dice que cada número natural tiene un sucesor). FPA no es ni más débil ni más fuerte que IΔ0+Ω1, ya que este último asume el Axioma del Sucesor pero asume una forma más débil de inducción.

El FPA puede demostrar el Primer Teorema de Incompletitud. Sin duda, los fragmentos de FPA también pueden hacerlo.

Más interesante es cuando se aclara la naturaleza del sistema lógico bajo estudio metalógico. Normalmente, la sintaxis de la lógica de primer orden está definida de manera que siempre se pueden concatenar dos cadenas para formar una mayor. Por ejemplo, se utiliza este principio en el Teorema de la Deducción, que es uno de los primeros teoremas metalógicos que se tiende a demostrar. Pero esta suposición, esencialmente equivalente al Axioma del Sucesor, no es necesaria, y uno puede abstenerse de hacerla.

En este entorno (en el que se supone que la sintaxis no es ilimitadamente larga), se puede decir lo siguiente: FPA puede demostrar el Primer Teorema de Incompletitud. Pero la prueba de Godel sólo parece funcionar en el caso de FPA + Axioma del Sucesor. En el caso FPA + Axioma no Sucesor, se formaliza básicamente la idea de que una prueba es generalmente más larga que cualquier axioma. No parece que la prueba de Godel del Segundo Teorema de Completitud funcione, y no sé si esto se puede reparar.

Answer 4

Una prueba muy detallada y de bajo nivel de los teoremas de incompletitud de Gödel es " Conjuntos finitos y teoremas de incompletitud de Gödel ". Se basa en la teoría de los conjuntos hereditarios finitos, que está estrechamente relacionada con la AP.