Por qué basta con la aritmética de Peano: PA puede codificar el cálculo

 (math.stackexchange.com)
1 puntos por GN⁺ 2025-06-15 | 1 comentarios | Compartir por WhatsApp
  • PA no puede demostrar todo el teorema de Goodstein ∀n G(n), pero para cada número natural estándar n, sí puede mostrar la existencia de una demostración en PA de G(n)
  • La clave es una construcción que genera mecánicamente una demostración de inducción transfinita limitada solo a la torre finita de potencias de ω necesaria para ese n
  • La altura necesaria m corresponde a la altura de la hereditary base notation de n, es O(log*(n)), y si se usa la notación abreviada ω^[m], la longitud de la demostración se reduce a alrededor de O(m log m)
  • Este resultado significa que “se puede construir una demostración para cada caso”, no que PA pueda demostrar todo el teorema de Goodstein
  • PA puede codificar dentro de un solo número natural números, pares, listas, estados de programa y demostraciones de lógica formal, así que también puede verificar dentro de PA si la demostración generada es realmente una demostración válida de PA

La forma matemática de la pregunta

  • El objeto de interés es la proposición G(n), que dice que la sucesión de Goodstein eventualmente llega a 0

  • La distinción conocida es la siguiente

    • PA puede demostrar cada caso concreto sobre naturales estándar, como G(15) o G(268)
    • PA no puede demostrar la proposición total ∀n ∈ N: G(n)

  • La pregunta es si PA puede demostrar una proposición de la siguiente forma

    ∀n ∈ N: ∃p ∈ N: P_PA(p, ⌜G(n)⌝)

  • P_PA(p, ⌜φ⌝) significa que p es el código de una demostración de φ dentro de PA

  • La conclusión es que, en este nivel, PA por sí sola basta

Qué tiene que demostrar PA

  • Para cada n, PA tiene que mostrar estas tres cosas
    • que puede calcularse la longitud de la demostración necesaria para probar G(n)
    • que termina el procedimiento que construye esa demostración
    • que la última oración de la demostración construida afirma la terminación de G(n)
  • Para cada G(n), puede construirse una demostración en PA de longitud O(log*(n) log(log*(n)))
  • log* es el logaritmo iterado (iterated logarithm), una función de crecimiento extremadamente lento
  • Como las demostraciones necesarias crecen cuando n aumenta, esto por sí solo no permite que PA demuestre todo el teorema de Goodstein

Sucesiones de Goodstein y notación ordinal

  • Las sucesiones de Goodstein usan hereditary base notation, que se conecta con representaciones ordinales escritas en forma normal de Cantor

  • En la construcción al estilo de John von Neumann, los ordinales se construyen como conjuntos

    • 0 es el conjunto vacío
    • dado un ordinal ord, ord ∪ {ord} también es un ordinal
    • dado un conjunto X de ordinales, la unión de X también es un ordinal

  • La forma normal de Cantor representa un ordinal de la siguiente manera

    ((n1, ord1), (n2, ord2), ..., (nk, ordk))
    • cada ni es un número natural positivo
    • cada ordi es un ordinal
    • ord1 > ord2 > ... > ordk

  • Esta notación representa el siguiente ordinal

    n1·ω^ord1 + n2·ω^ord2 + ... + nk·ω^ordk

  • La comparación se maneja con orden lexicográfico en la secuencia ord1, n1, ord2, n2, y si una de las dos secuencias termina antes, la más corta es menor

De la inducción a la inducción transfinita

  • El quinto axioma de PA proporciona inducción sobre los números naturales
    • S(0) es verdadera
    • si S(n) entonces S(s n) también es verdadera
    • por lo tanto, S es verdadera para todos los números naturales
  • A partir de esto, PA puede definir < recursivamente y también demostrar inducción fuerte
    • si puede mostrarse que para todo n, cuando S es verdadera para todos los números menores que n, entonces S(n) también lo es, entonces S es verdadera para todos los naturales
  • En ZFC puede demostrarse la inducción transfinita, que es la versión de inducción fuerte para todos los ordinales
  • Para objetos escritos en forma normal de Cantor se usan dos propiedades
    • toda sucesión decreciente escrita en forma normal de Cantor es necesariamente finita
    • puede aplicarse inducción transfinita a los objetos en forma normal de Cantor

El alcance de la inducción transfinita posible dentro de PA

  • PA no puede demostrar inducción transfinita para todos los ordinales
  • En cambio, sí puede manejar dentro de PA ciertos rangos ordinales de altura finita
    • como PA demuestra inducción fuerte, puede manejar inducción transfinita hasta ω
    • por la misma lógica, también puede demostrarse inducción transfinita sobre ω^ω
    • repitiendo de nuevo el mismo método, puede iterarse para torres de altura finita como ω^(ω^ω), ω^(ω^(ω^ω)), etc.
  • La demostración en cada etapa solo cambia la altura de la torre y se genera mecánicamente
  • Si se escribe directamente la m-ésima torre, la longitud total de la demostración es O(m^2)
  • Si se usa una notación abreviada como ω^[m], escribir m requiere solo longitud O(log m), así que la demostración total pasa a ser O(m log m)
  • Para cada ordinal individual por debajo de ε₀, existe una demostración de inducción transfinita dentro de PA, pero unir todas esas demostraciones en una sola requeriría una demostración de longitud infinita
  • Si PA pudiera demostrar inducción transfinita hasta ε₀, entonces podría demostrar la consistencia de PA, lo que chocaría con el segundo teorema de incompletitud de Gödel

Procedimiento para generar la demostración de cada G(n)

  • Para un n concreto, solo hace falta llegar hasta la altura de torre de su hereditary base notation
  • Esa altura es O(log*(n)) y puede tratarse en PA como una función fácil de calcular
  • Dado un n de entrada, el programa puede producir lo siguiente
    • demostraciones de hechos comunes sobre PA
    • una demostración de que G(n) sigue una sucesión decreciente dentro de ω^[m] para algún m
    • el proceso para calcular ese m y una demostración del valor de m
    • una demostración de inducción transfinita para ω^[0]
    • una demostración de que la inducción transfinita sobre ω^[i] implica la inducción transfinita sobre ω^[i+1]
    • las demostraciones de inducción transfinita para cada etapa desde i = 0 hasta m-2
    • una demostración de que la inducción transfinita sobre ω^[m-1] implica que toda sucesión decreciente dentro de ω^[m] es finita
    • la conclusión de que G(n) termina
  • PA puede demostrar sobre este procedimiento lo siguiente
    • que el procedimiento termina
    • que el procedimiento genera una lista de oraciones
    • que la lista comienza con los axiomas de Peano
    • que cada oración se sigue lógicamente de las anteriores
    • que por inducción todas las oraciones quedan demostradas
    • que la última oración es “G(n) termina”
  • Por lo tanto, PA demuestra que, para cualquier número natural n, PA demuestra la terminación de G(n)

Cómo codifica PA el cálculo

  • “Codificar” significa fijar una manera en la que cierto número natural represente una estructura específica
  • Los ingredientes básicos de PA son los siguientes
    • 0
    • la función sucesor (s n)
    • la igualdad
    • el predecesor (p n) para números distintos de 0
    • definiciones recursivas justificadas por inducción
    • condicionales que bifurcan según 0 o 1
  • Dentro de PA pueden definirse recursivamente funciones aritméticas básicas como
    • <
    • min, max
    • +
    • *
    • potenciación
    • residuo %
    • división entera //
  • Las propiedades básicas de estas funciones pueden demostrarse dentro de PA por inducción

Construir estructuras de datos con un solo número natural

  • Para codificar dos números naturales dentro de uno solo, puede usarse un método que entrelaza bits binarios
    • los bits en posiciones impares son head
    • los bits en posiciones pares son tail
  • A partir del número que forma el par, luego pueden recuperarse head y tail
  • Si pueden construirse pares, también pueden representarse listas enlazadas
    • usar 0 como nil
    • lista vacía
    • agregar un elemento al frente
    • leer cabeza y cola
    • calcular longitud
    • acceder a una posición arbitraria
    • insertar y eliminar
  • Con números, pares y listas, también pueden representarse dentro de un solo número natural estructuras como pilas, colas, árboles, documentos de texto o una máquina virtual

Lisp y la codificación de procedimientos de cálculo

  • Lisp se usa como lenguaje conveniente para explicar análisis sintáctico e interpretación por su estructura de paréntesis y su forma de command and arguments
  • Los números naturales dentro de PA pueden interpretarse como pares (type, value)
    • número
    • booleano
    • par
    • lista
    • texto, etc.
  • Algunos números naturales pueden no ser valores válidos de cierto tipo específico, pero los valores válidos sí pueden representar de manera única alguna estructura
  • Sobre esta codificación pueden construirse estructuras de datos de Lisp, una máquina virtual de Lisp y un intérprete de Lisp
  • Como Lisp es Turing complete, por esta vía puede codificarse dentro de PA cualquier procedimiento computable y también el estado de ese procedimiento
  • Incluso puede representarse y seguirse dentro de PA el estado del cálculo después de una cantidad específica de pasos

PA también codifica las demostraciones de PA

  • Una demostración en lógica de primer orden puede verse como una lista de oraciones
    • cada oración es un paso de inferencia
    • pueden escribirse oraciones incorrectas o inferencias inválidas, pero un procedimiento de verificación puede descartarlas
  • Dentro de PA puede crearse un tipo como type-proof y codificar una demostración como una lista de oraciones
  • También puede codificarse dentro de PA el siguiente procedimiento de verificación
    • comprobar si la demostración está bien formada
    • comprobar si cada paso de la demostración es válido
    • comprobar qué axiomas se están suponiendo
    • comprobar si la conclusión final es la oración deseada
  • Si existe una demostración de alguna oración a partir de ciertos axiomas, entonces también existe un número natural específico de PA que representa esa demostración
  • Como PA puede expresar el cálculo que verifica si ese número es realmente el código de una demostración válida, la propia noción de “demostración dentro de PA” también puede tratarse dentro de PA
  • Gödel codificó la lógica dentro de PA sin necesidad de codificar todo el cálculo, pero desde la perspectiva de un programador, entenderlo pasando por la codificación del cálculo es un camino más natural

Lecturas relacionadas

1 comentarios

 
GN⁺ 2025-06-15
Opiniones en Hacker News

  • Es una publicación que amplía una pregunta de Stack Overflow en forma de entrada de blog.
    Trata sobre los límites de lo que se puede demostrar con los axiomas de Peano y cómo empezar a hacer bootstrap de Lisp dentro de ellos.
    Todos los malos chistes están en la segunda sección, y se agradecen correcciones o preguntas de seguimiento.

    • Después de leer todo el artículo, vi que en el ejemplo (defun not (x) ...) de la sección "Why Lisp?" hay una parte con paréntesis desbalanceados.
      Me pareció bastante gracioso en relación con la parte donde más adelante escribe que “hacer que una computadora encuentre paréntesis balanceados es realmente fácil”, y también fue divertida la observación de la sección "Basic Number Theory" sobre que “el montón de paréntesis de cierre deja de verse”.
      Aunque hace mucho que no uso Lisp, el texto me pareció bueno porque pude seguirlo de nuevo y captar la idea principal.
    • Todavía no leí mucho más allá de la introducción, pero me parece interesante la premisa de que cada caso concreto de la sucesión de Goodstein puede demostrarse dentro de PA que termina en 0, mientras que no puede demostrarse el enunciado de que todas las sucesiones terminan.
      También es extrañamente fascinante que se pueda codificar el cálculo solo con los axiomas de Peano, como si apareciera una capa más de autorreferencia.
      Hace poco empecé a estudiar más teoría de conjuntos y llegué hasta las sucesiones de Goodstein; me interesaría recibir recomendaciones de libros de texto del siguiente nivel sobre teoría avanzada de conjuntos o de textos que traten en profundidad la aritmética de Peano.
    • Boot sector Lisp también se bootstrappea a sí mismo: https://justine.lol/sectorlisp2/
      Varios Lisp de https://t3x.org también implementan números y el resto con celdas cons y apply/eval.
      El evaluador metacircular de John McCarthy es código que Alan Kay llamó “las ecuaciones de Maxwell del software”, y en SectorLISP se implementa con cosas como ASSOC EVAL EVCON APPLY EVLIS PAIRLIS.
      Algunos Forth son parecidos, y Zenlisp de T3X explica el tema en torno a cómo eval/apply se llaman recursivamente entre sí: http://t3x.org/zsp/index.html
    • Hay dos lugares donde dice “omega”, pero parece que debería ser \omega.

  • Como alguien que ha hecho tanto matemáticas como programación, más que la codificación del cálculo en sí, me parece más interesante que se pueda rodear la independencia del teorema de Goodstein con este tipo de autorreferencia.
    Parece significar que PA + “PA es ω-consistente” puede demostrar el teorema de Goodstein, y quizá la inducción transfinita hasta ε₀ también pueda hacerse en general.
    Edición: me pregunto si PA + “PA es consistente” por sí solo también alcanza.

    • Como autor de la pregunta original en SO, agregué algunos enlaces a respuestas relacionadas en la pregunta.
      En esencia, “PA es consistente” por sí solo no alcanza; basta con tener el principio de reflexión uniforme de que “si PA demuestra algo, entonces eso es verdadero”.
      No estoy 100% seguro de si este principio es equivalente a la ω-consistencia, pero leyendo lo siguiente parece que sí: https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relation_to_other_consistency_principles
      Wikipedia describe que T sea ω-consistente como “T + RFN_T + el conjunto de todas las oraciones verdaderas es consistente”, lo que parece significar lo mismo que “T + RFN_T es verdadero”.
    • Me gusta esta estructura recursiva.
      En esencia, se construye una metademostración sobre qué demuestra PA, y si uno confía en PA, termina confiando también en esa metademostración.
      Sin embargo, no veo bien cómo PA + “PA es consistente” sería suficiente.
      Ese sistema parece admitir modelos donde el teorema de Goodstein es verdadero para los números naturales estándar, pero falso para algún entero no estándar N, y justo ese caso parecería quedar excluido por la ω-consistencia más fuerte.
    • Lamentablemente no es así, y parece que con fórmulas puramente universales tampoco se puede hacer otra cosa.
      Es decir, no es un problema específico de Con(PA), sino un fenómeno más general: https://math.stackexchange.com/questions/5003237/can-goodsteins-theorem-be-proven-in-mathrmpa-conpa
      En relación con la primera pregunta, me intriga cómo se codifica la ω-consistencia como una fórmula de PA.
    • En la publicación de Math Exchange dicen que PA + inducción transfinita sobre ε₀ demuestra la consistencia de PA.
      Por eso parece que PA + “PA es consistente” podría demostrar la inducción transfinita sobre ε₀.
    • A esta altura los detalles se alejan un poco de lo que puedo afirmar con seguridad.
      ChatGPT dijo que PA + “PA es consistente” por sí solo no alcanza, y como seguramente habrá digerido suficientes libros de lógica, creo que se puede confiar en esa afirmación.

  • Cuando usé por primera vez la aritmética de Peano, me sorprendió bastante su expresividad.
    Al principio parece un sistema básico, pero cuando uno se da cuenta de que el propio cálculo puede codificarse dentro de PA y que se pueden imitar varios tipos de cómputo, las cosas que parecían complejas empiezan a encajar.
    Me interesaría recibir recomendaciones de materiales que expliquen estas técnicas de codificación de manera amable para principiantes.

  • Esto es muy parecido a la teoría de Boyer-Moore. Esta teoría también construye las matemáticas a nivel de los axiomas de Peano.
    Boyer y Moore también crearon un demostrador automático de teoremas adaptado a esta teoría, y dejaron una copia que funciona en GNU Common Lisp en https://github.com/John-Nagle/nqthm/tree/master
    Según su explicación, es fácil pensar en el programa como si fuera un estudiante de matemáticas bastante bueno. Si solo se le dan los axiomas de Peano, es difícil esperar que demuestre o descubra el teorema de factorización prima, pero si junto con los axiomas de Peano se le da una lista de teoremas como “demuestra la conmutatividad de la suma”, “demuestra que la multiplicación distribuye sobre la suma” y “demuestra que el resultado de la función GCD divide a ambos argumentos”, entonces puede manejarlo bien.
    Paper: https://www.cs.utexas.edu/~boyer/acl.pdf

  • El comentario dirigido a JoJoModding en Math StackExchange está equivocado.
    La explicación de que “PA puede demostrar que produce una demostración, pero quizá no pueda demostrar que esa demostración tiene longitud finita” no apunta al núcleo del asunto.
    Si PA demuestra “PA demuestra X”, entonces PA puede demostrar X.
    Lo importante no es que existan modelos no estándar, sino que el modelo estándar de los números naturales es un modelo de PA.
    Por lo tanto, si PA demuestra “PA demuestra X”, entonces realmente existe un número natural finito estándar que corresponde a la demostración codificada de “PA demuestra X”, y con ese número natural se puede construir una demostración de X dentro de PA.

    • La versión en lenguaje natural presentada es ambigua, así que la distinción es importante.
      Lo que se mostró no es “PA demuestra Provable(forall n, G(n))”, sino más bien “PA demuestra forall n, Provable(G(n))”.
      Si fuera lo primero, de hecho se seguiría que “PA demuestra forall n, G(n)”, pero lo segundo es diferente.
      Sin referirse a las sucesiones de Goodstein, me gustaría ver un argumento de que, para una proposición general P, 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 verdadera.
      Dentro de PA se puede construir una función que busca todas las demostraciones que PA puede producir, y con base en eso se puede construir una función will-return que analiza si cierta función y cierta entrada van a retornar.
      Esto se parece a un intento de resolver el problema de la parada, así que no siempre funciona, pero en muchos casos sí.
      Si aquí se construye opposite-return, puede configurarse para intentar retornar cuando la función y la entrada dadas no retornan, y para no retornar cuando sí retornan.
      Al considerar (opposite-return opposite-return opposite-return) de la misma forma que en la demostración estándar del problema de la parada, PA puede demostrar que “si PA puede demostrar que opposite-return retorna, entonces en realidad no retorna”, “si PA puede demostrar que no retorna, entonces en realidad retorna”, “si PA pudiera demostrar efectivamente todo lo que demuestra que demuestra, entonces tendría que tener una demostración de una de las dos proposiciones anteriores” y “por lo tanto, en tal caso PA es inconsistente”.
      Esto es una forma del segundo teorema de incompletitud de Gödel, y por eso hay que distinguir entre “PA demuestra” y “PA demuestra que ella misma demuestra”.
    • Que el modelo estándar sea un modelo de PA solo se cumple cuando PA es consistente, y PA no puede demostrar su propia consistencia. Mientras no sea inconsistente, es imposible por el teorema de Gödel.
      Por eso la demostración propuesta no funciona dentro de PA, y ese parece ser precisamente el punto del comentario.

  • https://math.stackexchange.com/questions/4408124/what-does-the-kirby-paris-theorem-mean

  • Hablando con alguien sobre tipos de datos inductivos, le mostré una definición zero/succ como Nat en Lean o Rocq.
    La otra persona preguntó: “¿eso es todo? ¿Y los axiomas de Peano? ¿Hay algo más primitivo que los tipos de datos inductivos?”, y me pareció interesante.
    Me hizo recordar que conviene ver los axiomas de Peano como una de varias decisiones de diseño, más que como algo obviamente incorporado.

    • Veo a los números naturales como más primitivos que los tipos de datos inductivos.
      Porque todos los tipos de datos inductivos pueden construirse usando los números naturales junto con constructores primitivos de tipos y universos, por ejemplo Π, Σ, =, Ω, etc.

  • Incluso el cálculo lambda puro es suficiente, porque el cálculo lambda codifica el cómputo.

  • En relación con la consistencia de PA, se puede demostrar dentro de PA: https://youtu.be/6pjLmmkZnIA

    • Para quienes no son lógicos, el contexto es imprescindible.
      El segundo teorema de incompletitud de Gödel muestra que, si PA puede demostrar su propia consistencia, entonces PA es inconsistente y, por lo tanto, puede demostrar cualquier cosa, incluidas falsedades.
      El trabajo enlazado no mostró la inconsistencia de PA, sino que definió un nuevo significado más débil de que PA “demuestra su propia consistencia”, y luego mostró que PA puede hacer esa tarea más débil.
      Es un trabajo interesante, pero para que tenga sentido ya hay que saber bastante lógica.

  • Este artículo recibió 123 puntos, pero la publicación enlazada de SO solo tiene 11 votos positivos.

    • En Stack Overflow se necesita 15 de reputación para votar positivo.
      Sumado al problema de reputación de que, si publicas allí, es fácil que te borren el post, y al límite de 15 puntos, parece que mucha gente no puede votar positivo.