La aritmética de Peano es suficiente, porque la aritmética de Peano puede codificar el cálculo

• La aritmética de Peano (PA) puede expresar procesos de cálculo mecánicos, por lo que es posible demostrar en PA la terminación de cada sucesión individual de Goodstein
• Mediante la forma normal de Cantor y la notación hereditaria de base, se pueden expresar las sucesiones de Goodstein y su carácter descendente, lo que permite construir demostraciones de longitud finita
• A través de la inducción (inducción fuerte / inducción transfinita), es posible extender las demostraciones por separado hasta ordinales de cierto orden
• PA puede demostrar que para todo número natural n, “G(n) llega a 0”, pero no puede dar una demostración total del teorema completo de Goodstein (para todo n)
• Con PA también es posible implementar suficientemente la codificación del cálculo, estructuras de datos (List, Pair, etc.) e incluso del propio lenguaje de programación (Lisp), así como la codificación de su propio proceso de demostración

---

Introducción y contexto del problema

• Este texto describe que la aritmética de Peano (PA) puede demostrar que la sucesión de Goodstein “llega a 0 para cada n (G(n) terminates)”
• Aunque esto puede parecer obvio para un lógico, se explica desde la perspectiva de la codificación del cálculo para que pueda entenderlo un programador
• Para cada caso de una sucesión de Goodstein, es posible construir dentro de PA una rutina concreta de demostración

Ordinals y sucesiones de Goodstein

• Se generan ordinales (Sets as Ordinals) al estilo de Von Neumann
  • 0 es el conjunto vacío, 1 es {0}, 2 es {0,1}, ω es {0,1,2,…}, ω+1 es {0,1,2,…,ω}, etc., con un orden bien definido
• La sucesión de Goodstein se describe mediante notación hereditaria en base usando la forma normal de Cantor
  • Ejemplo: ω^ω es ((1,ω)), es decir, ((1,(1,1)))
  • El orden < se determina por comparación lexicográfica de los ordinales/coficientes de cada término

Inducción e inducción transfinita

• Inducción en la aritmética de Peano: si vale para 0 y si vale para n→n+1, entonces vale para todos los números naturales
• La inducción fuerte también puede demostrarse en PA
• Inducción transfinita: en ZFC y sistemas similares puede extenderse a ordinales infinitos, y puede aplicarse a números escritos en forma normal de Cantor
  • Teorema 1: toda sucesión descendente en forma normal de Cantor es siempre finita
  • Teorema 2: puede usarse inducción transfinita para números en forma normal de Cantor

Inducción transfinita en PA y longitud de las demostraciones de sucesiones de Goodstein

• PA puede generar una demostración de la terminación de la sucesión de Goodstein para cualquier n
  • La demostración puede construirse según la altura de torre m=O(log* n) (logaritmo iterado) de la forma normal de Cantor
  • Combinando m demostraciones por etapa, la longitud total de la demostración es O(m^2), o puede reducirse a O(m log m) si se introduce una notación especial (ω[m])
• Sin embargo, la demostración del teorema completo de Goodstein (para todo n) es imposible en PA (no se puede hacer inducción transfinita hasta ε0)
  • Si fuera posible, también podría demostrarse la consistencia de PA, lo que entraría en conflicto con el segundo teorema de incompletitud de Gödel

Codificación de programas y estructuras de datos en PA

• PA puede codificar suficientemente cálculo/programas/estructuras de datos (números, pares, listas y cualquier otra estructura)
• Se pueden implementar diversas funciones de la siguiente manera:
  • lógica y operaciones básicas (+, *, pow, //, %, min, max, etc.)
  • pattern matching y bifurcación condicional (if, cond, etc.)
  • codificar un número como dos números (par) o expandir repetidamente desde un par hacia estructuras más complejas como listas (listas recursivas, árboles, texto, etc.)
• Gracias a esta codificación de estructuras de datos, incluso es posible construir un intérprete para una máquina virtual arbitraria o un lenguaje de programación (como Lisp)

Bootstrap hacia Lisp y codificación

• Usando Lisp como ejemplo, se explica cómo implementar operaciones numéricas y lógicas básicas, estructuras de datos e intérpretes de lenguajes de programación
• La estructura de Lisp (mapeo de instrucciones/argumentos, formas especiales, macro, etc.) puede implementarse en PA con combinaciones apropiadas de funciones
• Más aún, dentro de PA pueden codificarse e implementarse simbólicamente el propio proceso de demostración de PA, los procedimientos de prueba lógica y estructuras autorreferenciales

Codificación de la propia lógica dentro de PA

• En lógica matemática, el proceso de prueba de la lógica de primer orden puede codificarse como datos numéricos de PA
• Cada paso de una demostración / proposición / regla de inferencia / verificación de prueba válida puede reconocerse y procesarse mediante una serie de funciones numéricas y procesamiento de listas
• Esta codificación metateórica y autorreferencial se conecta con la incompletitud de Gödel y con la demostración del problema de la parada

Conclusión

• El cálculo, las estructuras de datos, los programas e incluso los procesos de prueba lógica pueden codificarse, demostrarse e interpretarse suficientemente dentro de PA
• Por lo tanto, cualquier sucesión individual de Goodstein (para n, la terminación de G(n)) puede demostrarse concretamente dentro de PA
• Sin embargo, una demostración de que “PA demuestra el teorema de Goodstein dentro de PA” para el teorema completo (todos los n) es imposible debido a los límites de la lógica
• Desde la perspectiva de un programador, PA es una base lógica completa capaz de codificar el cálculo mismo

[GN⁺]

Comentarios de Hacker News

• Esta publicación es una entrada de blog basada en algo que pregunté en Stack Overflow; incluye una explicación de los límites de lo que puede probarse con los axiomas de Peano y de cómo arrancar Lisp dentro de la aritmética de Peano. La mayoría de las bromas están en la segunda sección. También son bienvenidas las correcciones o preguntas adicionales.
  • Mientras leía esto, encontré una parte en la sección "Why Lisp?" donde los paréntesis no cuadran (ver el ejemplo (defun not (x) (if x false true)). En cuanto alguien empieza a usar paréntesis, por instinto me pongo a revisar si están bien cerrados. Luego me reí muchísimo cuando más adelante menciona que "es fácil programar en una computadora si los paréntesis están balanceados". Ese chiste me pareció realmente muy bueno, y también me llamó la atención el comentario en la sección "Basic Number Theory": ; After a while, you stop noticing that stack of closing parens.. No veía Lisp desde hace tiempo y el texto me pareció muy divertido.
  • Esto me parece realmente fascinante. Aún voy apenas por la introducción, pero me resulta interesante que dentro de la aritmética de Peano (PA) se pueda demostrar que todos los casos especiales de las sucesiones de Goodstein llegan a 0, pero no que "todos" los casos lleguen a 0 (aunque en cierto sentido sea el resultado esperable, sigue siendo emocionante). Y también es muy extraño que la aritmética de Peano por sí sola pueda codificar computación (en principio es obvio, pero antes no me había detenido a pensar un nivel más de autorreferencia). Justamente hace poco intenté estudiar un poco más de teoría de conjuntos y llegué hasta la parte sobre sucesiones de Goodstein en el libro Intro to Set Theory. Si alguien tiene recomendaciones de textos avanzados sobre teoría de conjuntos o sobre aritmética de Peano en más profundidad, se agradecerían. Entender por qué PA no basta para demostrar el teorema de Goodstein es una pequeña meta personal, aunque también son bienvenidos otros caminos recomendables.
  • En dos lugares con omega en el texto se olvidaron de escribirlo como \omega.
• Es muy similar a la teoría de Boyer-Moore. Esa teoría construye matemáticas al nivel de la aritmética de Peano. Boyer y Moore desarrollaron un demostrador automático de teoremas que implementa esa teoría, y también tengo una copia que corre en GNU Common LISP. Vale la pena ver el artículo "A Computational Logic" y la implementación de nqthm. En el artículo, por ejemplo, me llamó la atención que al partir de los axiomas de Peano los teoremas complejos, como la multiplicación de primos, son difíciles, pero aun así se pueden demostrar sin problema la conmutatividad de la suma, la distributividad de la multiplicación y teoremas relacionados con la función GCD.
• Tengo formación tanto en matemáticas como en programación, y personalmente me parece aún más interesante que la parte sobre la independencia del teorema de Goodstein pueda sortearse de manera autorreferencial. Me pregunto si PA+"PA es omega-consistente" bastaría para demostrar el teorema de Goodstein, y sospecho que eso también permitiría inducción transfinita hasta epsilon_0. EDIT: ¿quizá incluso bastaría con solo "PA es consistente"?
  • Por desgracia no. Y de hecho no solo Con(PA), sino tampoco cualquier fórmula cuantificada universalmente basta. Véase esta respuesta relacionada en Math StackExchange. Respecto de tu primera pregunta, me da curiosidad cómo se codifica la omega-consistencia como fórmula de PA; no se me ocurre de inmediato.
  • Yo soy quien hizo la pregunta en Stack Overflow. Agregué algunos enlaces a respuestas en la pregunta. En esencia, solo "PA es consistente" no basta, pero sí basta una especie de "principio de reflexión uniforme" del tipo "si es demostrable en PA, entonces es verdadero". No estoy seguro de que ese principio sea exactamente lo mismo que la omega-consistencia, pero en la explicación de Wikipedia se entiende como si lo fuera. Si T es omega-consistente, entonces significa que "T + RFN_T + el conjunto de todas las fórmulas verdaderas es consistente", lo cual se interpreta como equivalente a que "T + RFN_T es verdadero".
  • También me gusta esta estructura inductiva (recursiva). Al final, uno construye una metaprueba sobre qué demuestra PA, y si confías en PA, entonces también puedes confiar en esa metaprueba. La parte de que simplemente "PA es consistente" baste no me queda del todo clara. Según yo, PA+"PA es consistente" permitiría que existiera un modelo donde el teorema de Goodstein es verdadero para los naturales estándar, pero también un modelo donde es falso para algún entero no estándar N. Supongo que una afirmación más fuerte como la omega-consistencia sí excluiría esos casos.
  • En la publicación de Math Exchange se menciona que una prueba en PA+inducción transfinita (epsilon_0) demostraría a su vez PA. Yo pensaba que PA+"PA es consistente" bastaría para demostrar inducción transfinita hasta epsilon_0.
  • Creo que en este punto el tema ya entra en detalles sobre los que no me siento cómodo opinando. Según ChatGPT, la explicación es que solo "PA+consistencia de PA" no basta. ChatGPT habrá digerido muchísimos libros de lógica, así que si dice eso, suena bastante creíble.
• El comentario que le escribiste a JoJoModding en Stack Overflow no es correcto. Dijiste que "como los modelos no estándar de PA tienen naturales infinitos, aunque PA demuestre que construyó cierta prueba, no puede demostrar que esa prueba tenga longitud finita", pero en realidad si PA demuestra "PA demostró X", entonces PA también demuestra X. Lo importante no es la existencia de modelos no estándar, sino el hecho de que el modelo estándar de los naturales es un modelo de PA. Así que si "PA demuestra que demuestra X", efectivamente se genera una prueba correspondiente a un natural finito estándar, y con ese número puede construirse dentro de PA una prueba real de X.
  • No tengo tiempo para revisar la lógica en detalle, pero en lenguaje natural parece que la diferencia clave es entre "PA demuestra forall n, G(n)" y "PA demuestra forall n, Provable(G(n))". No soy muy fuerte en lógica, así que agradecería si alguien pudiera explicar de manera concreta por qué demostrar forall n, Provable(P(n)) no permite demostrar Provable(forall n, P(n)).
  • La afirmación "si PA demuestra 'PA demuestra X', entonces PA demuestra X" no es correcta. En PA se puede definir una función que busque entre todas las pruebas posibles, y de hecho esbocé ese enfoque al final de la respuesta. A partir de ahí también se pueden construir funciones como will-return y opposite-return, lo cual coincide con la prueba estándar del problema de la detención. Si consideras el caso opposite-return(opposite-return, opposite-return), entonces si PA demuestra que opposite-return retorna, también demuestra que en realidad no retorna; y, a la inversa, si demuestra que no retorna, entonces demuestra que retorna. Si PA adoptara una afirmación más fuerte del estilo "todo lo demostrable es realmente demostrable", eso llevaría directamente al segundo teorema de incompletitud de Gödel, es decir, a que PA sería inconsistente. Por eso hay que distinguir necesariamente entre "PA demuestra" y "PA demuestra que demuestra".
• El cálculo lambda puro también basta. El propio cálculo lambda codifica computación.
• Estaba hablando con alguien sobre tipos de datos inductivos y le mostré la definición de Nat construida con zero/succ (como se ve en Lean o Rocq). La otra persona se preguntaba cosas como "¿de verdad basta con esto?", "¿hacen falta los axiomas de Peano?", "¿hay algo más primitivo que un tipo de dato inductivo?". Me hizo pensar que conviene recordar con frecuencia que la aritmética de Peano no debe darse por obvia en esencia, sino verse como una decisión de diseño entre otras posibles.
  • Sobre la pregunta "¿hay algo más fundamental que un tipo de dato inductivo?", yo diría que los números naturales mismos son más primitivos que los tipos de datos inductivos. Todos los tipos de datos inductivos pueden construirse con los naturales y unos pocos constructores de tipos primitivos adicionales (Π, Σ, =, Ω).
• Véase este Q&A sobre el teorema de Kirby-Paris.
• Comparto un video sobre la consistencia de PA, en relación con qué puede demostrarse dentro de PA: enlace de YouTube
  • Es una parte que definitivamente hay que explicarles a quienes no son lógicos. Según el segundo teorema de incompletitud de Gödel, si PA pudiera demostrar su propia consistencia, entonces PA sería inconsistente (podría demostrar cualquier cosa, incluso falsedades). Este video no muestra que PA demuestre que PA es inconsistente, sino que PA puede demostrar su "propia consistencia" en un sentido más débil. Sin una base en fundamentos de la lógica es difícil entenderlo con precisión, pero aun así resulta muy interesante.
• Este tema lleva 123 puntos, pero la publicación original en SO apenas tiene 11 votos.
  • En Stack Overflow necesitas 15 puntos para poder votar positivamente. A veces la gente no quiere publicar por el tema de la reputación, y ese requisito de 15 puntos probablemente también frena los votos positivos.
• ¿Basta con la computación por sí sola? Los reales computables son un subconjunto de todos los números reales.
  • Creo que el nombre "números reales" ya de por sí induce a error. Puede interpretarse que un número real representa una proporción física real. Por ejemplo, decir 180.255 libras significaría la proporción física real entre el peso real de Jones y la libra patrón. Esas proporciones también existen físicamente; en ese sentido, los números reales pueden interpretarse como razones físicas. En cambio, hoy predomina más la idea de los números como conceptos abstractos separados de la realidad, una postura típicamente platónica. Pero en la práctica es imposible medir o representar algo con precisión infinita. Por ejemplo, medir con más de 50 cifras de precisión sería imposible por límites cuánticos. Si quisieras medir sin error la órbita de los cuerpos del sistema solar, con más de 50 cifras tendrías que considerar el efecto gravitacional de estrellas vecinas, con más de 100 cifras modelarías la galaxia completa, y así sucesivamente hasta incluir influencias físicas imposibles de observar. Así que en la realidad solo tiene sentido una matemática de precisión finita. Es decir, en principio todo es computable, pero al ir hacia el infinito el propio modelo matemático deja de tener significado.
  • ¿De verdad? En realidad, la idea de que hay "más" no numerables parte de un malentendido. Véase mi explicación. Si aceptas que los no numerables son "más", te ves obligado a adoptar una postura discutible sobre lo que significa "existir". Véase también esta discusión relacionada. Por último, aunque llevemos el razonamiento lógico hasta el final, todo puede representarse en una computadora. Incluso si añades grandes conjuntos a ZFC, puedes partir de PA e inferir cualquier conclusión arbitraria, así que en la práctica considero que PA basta por sí sola. Si hace falta algo más persuasivo, recomiendo el libro Gödel, Escher, Bach.
  • Mi enfoque es un poco distinto. Aunque los números reales en general no pueden manipularse de ninguna forma por medio de cálculo, simbolización o registro, muchas veces las "proposiciones" sobre los reales sí pueden expresarse y calcularse de maneras útiles. Me parece fascinante, como en Harvey Friedman o en el autor de este texto, intentar generar valores inimaginablemente complejos dentro de sistemas simples. (Nota: el sitio web de audiomulch no carga).
  • Sin un objetivo asociado a la frase "basta", la pregunta queda mal definida. Lo importante es: ¿basta para qué?
  • Creo que la propia pregunta "¿basta solo con la computación?" está mal planteada. Claro que no basta; si bastara, entonces sería correcta la visión de algunos que imaginan la realidad como una especie de reloj fácil de creer. La realidad es mucho más interesante y compleja que eso.