Por que a aritmética de Peano basta: PA consegue codificar computações

 (math.stackexchange.com)
1 pontos por GN⁺ 2025-06-15 | 1 comentários | Compartilhar no WhatsApp
  • PA não consegue provar o teorema de Goodstein completo ∀n G(n), mas, para cada número natural padrão n, é possível mostrar dentro da PA a existência de uma prova em PA de G(n)
  • A ideia central é lidar apenas com torres finitas de potências de ω da altura necessária para n, e construir mecanicamente a prova por indução transfinita dentro desse intervalo
  • A altura necessária m corresponde à altura da hereditary base notation de n e é O(log*(n)); usando a notação abreviada ω^[m], o tamanho da prova cai para cerca de O(m log m)
  • Esse resultado quer dizer que “é possível construir a prova de cada caso”, não que a PA prove o teorema de Goodstein completo
  • A PA consegue codificar números, pares, listas, estados de programas e provas formais de lógica em um único número natural, de modo que também é possível verificar dentro da PA se a prova gerada é de fato uma prova em PA

Forma matemática da pergunta

  • O objeto de interesse é a proposição G(n), que afirma que a sequência de Goodstein eventualmente chega a 0

  • A distinção conhecida é a seguinte

    • A PA consegue provar cada caso concreto sobre números naturais padrão, como G(15) e G(268)
    • A PA não consegue provar a proposição geral ∀n ∈ N: G(n)

  • A pergunta é se a PA consegue provar uma proposição da seguinte forma

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

  • P_PA(p, ⌜φ⌝) significa que p é o código de uma prova de φ dentro da PA

  • A conclusão é que, nesse nível, a PA basta

O que a PA precisa provar

  • Para cada n, a PA precisa mostrar estas três coisas
    • É possível calcular o tamanho da prova necessário para provar G(n)
    • O procedimento que constrói essa prova termina
    • A última sentença da prova construída afirma a terminação de G(n)
  • Para cada G(n), é possível construir uma prova em PA de tamanho O(log*(n) log(log*(n)))
  • log* é o logaritmo iterado (iterated logarithm), uma função que cresce muito lentamente
  • À medida que n cresce, a prova necessária também fica maior; por isso, apenas isso não permite que a PA prove o teorema de Goodstein completo

Sequências de Goodstein e notação ordinal

  • Sequências de Goodstein usam hereditary base notation, que se conecta à representação de ordinais em forma normal de Cantor

  • Na construção de John von Neumann, ordinais são construídos como conjuntos

    • 0 é o conjunto vazio
    • Se existe um ordinal ord, então ord ∪ {ord} também é um ordinal
    • Se existe um conjunto X de ordinais, então a união de X também é um ordinal

  • A forma normal de Cantor representa um ordinal na forma

    ((n1, ord1), (n2, ord2), ..., (nk, ordk))
    • Cada ni é um número natural positivo
    • Cada ordi é um ordinal
    • ord1 > ord2 > ... > ordk

  • Essa notação representa o seguinte ordinal

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

  • A comparação é tratada como uma comparação lexicográfica na ordem ord1, n1, ord2, n2; se um lado terminar antes, o lado mais curto é menor

Da indução à indução transfinita

  • O quinto axioma da PA fornece indução sobre os números naturais
    • S(0) é verdadeiro
    • Se S(n) é verdadeiro, então S(s n) também é verdadeiro
    • Então S é verdadeiro para todos os números naturais
  • A partir disso, a PA consegue definir < recursivamente e também provar a indução forte
    • Se, para todo n, mostrar que S(n) é verdadeiro sempre que S for verdadeiro para todos os números menores que n, então S é verdadeiro para todos os números naturais
  • Em ZFC, é possível provar a indução transfinita, que é a indução forte sobre todos os ordinais
  • Para objetos escritos em forma normal de Cantor, usam-se duas propriedades
    • Uma sequência decrescente escrita em forma normal de Cantor é necessariamente finita
    • É possível usar indução transfinita sobre objetos em forma normal de Cantor

O alcance da indução transfinita possível dentro da PA

  • A PA não consegue provar indução transfinita para todos os ordinais
  • Em vez disso, certos intervalos de ordinais de altura finita podem ser tratados dentro da PA
    • Como a PA prova indução forte, ela consegue tratar a indução transfinita até ω
    • Pela mesma lógica, também é possível provar indução transfinita para ω^ω
    • Repetindo o mesmo método, é possível fazer isso para torres de altura finita como ω^(ω^ω), ω^(ω^(ω^ω)) etc.
  • A prova de cada etapa muda apenas a altura da torre e é gerada mecanicamente
  • Se a m-ésima torre for escrita por extenso, o tamanho total da prova será O(m^2)
  • Usando uma notação abreviada como ω^[m], escrever m exige apenas comprimento O(log m), de modo que a prova total fica em O(m log m)
  • Para cada ordinal abaixo de ε₀, existe dentro da PA uma prova de indução transfinita para ele, mas unificar tudo isso exigiria uma prova de comprimento infinito
  • Se a PA provasse a indução transfinita para ε₀, ela conseguiria provar sua própria consistência, o que entraria em conflito com o segundo teorema da incompletude de Gödel

Procedimento de geração de prova para cada G(n)

  • Para um n específico, só é necessária a altura de torre da hereditary base notation
  • Essa altura é O(log*(n)) e é tratada como uma função que a PA consegue calcular facilmente
  • Para uma entrada n, o programa pode produzir
    • Provas de fatos comuns sobre a PA
    • Uma prova de que G(n) acompanha uma sequência decrescente dentro de ω^[m] para algum m
    • O processo de cálculo desse m e uma prova do valor de m
    • Uma prova de indução transfinita para ω^[0]
    • Uma prova de que a indução transfinita de ω^[i] implica a indução transfinita de ω^[i+1]
    • Provas de indução transfinita para cada etapa de i = 0 até m-2
    • Uma prova de que a indução transfinita de ω^[m-1] implica que toda sequência decrescente dentro de ω^[m] é finita
    • A conclusão de que G(n) termina
  • A PA consegue provar o seguinte sobre esse procedimento
    • O procedimento termina
    • O procedimento gera uma lista de sentenças
    • A lista começa com os axiomas de Peano
    • Cada sentença segue logicamente das sentenças anteriores
    • Por indução, todas as sentenças são provadas
    • A última sentença é “G(n) termina”
  • Portanto, para qualquer número natural n, a PA prova o fato de que a PA prova a terminação de G(n)

Como a PA codifica computações

  • “Codificação” é uma forma de estabelecer que certo número natural representa certa estrutura
  • Os materiais básicos da PA são
    • 0
    • A função sucessor (s n)
    • Igualdade
    • O predecessor (p n) para números diferentes de 0
    • Definições recursivas justificadas por indução
    • Condicionais que ramificam conforme 0 ou 1
  • Dentro da PA, é possível definir recursivamente funções aritméticas básicas como
    • <
    • min, max
    • +
    • *
    • Potenciação
    • Resto %
    • Divisão inteira //
  • As propriedades básicas dessas funções podem ser provadas dentro da PA por indução

Criando estruturas de dados com um único número natural

  • Para codificar dois números naturais em um único número natural, é possível usar um método que intercala bits na representação binária
    • Bits em posições ímpares são head
    • Bits em posições pares são tail
  • A partir do par assim criado, é possível extrair novamente head e tail
  • Se é possível criar pares, também é possível representar listas encadeadas
    • Usar 0 como nil
    • Lista vazia
    • Adicionar um elemento no início
    • Ler cabeça e cauda
    • Calcular comprimento
    • Acessar posição arbitrária
    • Inserir e remover
  • Com números, pares e listas, estruturas como pilhas, filas, árvores, documentos de texto e máquinas virtuais também podem ser representadas por um único número natural

Lisp e codificação de procedimentos computacionais

  • Lisp é usado como uma linguagem conveniente para explicar parsing e interpretação por causa de sua estrutura de parênteses e do formato command and arguments
  • Um número natural dentro da PA pode ser interpretado como um par (type, value)
    • Número
    • Booleano
    • Par
    • Lista
    • Texto etc.
  • Alguns números naturais podem não ser valores válidos de um tipo específico, mas os valores válidos podem representar uma estrutura de forma única
  • Sobre essa codificação, é possível construir estruturas de dados Lisp, uma máquina virtual Lisp e um interpretador Lisp
  • Como Lisp é Turing complete, por esse caminho é possível codificar dentro da PA qualquer procedimento computável e o estado desse procedimento
  • O estado de uma computação após um número específico de etapas também pode ser representado e rastreado dentro da PA

A PA também codifica provas da PA

  • Uma prova em lógica de primeira ordem pode ser vista como uma lista de sentenças
    • Cada sentença é uma etapa de inferência
    • Sentenças inválidas ou inferências inválidas também podem ser escritas, mas um procedimento de verificação consegue filtrá-las
  • Dentro da PA, é possível criar um tipo como type-proof e codificar uma prova como lista de sentenças
  • Os seguintes procedimentos de verificação também podem ser codificados dentro da PA
    • Verificar se a prova é bem formada
    • Verificar se cada etapa da prova é válida
    • Verificar quais axiomas são assumidos
    • Verificar se a conclusão final é a sentença desejada
  • Se existe uma prova de certa sentença a partir de certos axiomas, então também existe um número natural específico da PA que representa essa prova
  • Como a PA consegue expressar a computação que verifica se esse número é de fato um código de prova, é possível tratar a própria “prova dentro da PA” dentro da PA
  • Gödel codificou a lógica dentro da PA sem precisar codificar toda a computação, mas, da perspectiva de programadores, entender isso via codificação de computações é um caminho natural

Leituras relacionadas

1 comentários

 
GN⁺ 2025-06-15
Opiniões no Hacker News

  • É um texto que expande uma pergunta do Stack Overflow em um post de blog
    Trata dos limites do que pode ser provado com os axiomas de Peano e de como começar a fazer bootstrap de Lisp dentro deles
    As piadas ruins estão todas na segunda seção, e correções ou perguntas de acompanhamento são bem-vindas

    • Depois de ler o texto inteiro, notei um ponto em que os parênteses não batem no exemplo (defun not (x) ...) da seção "Why Lisp?"
      Isso ficou bem engraçado em conjunto com a parte posterior em que ele escreve que “é realmente fácil fazer um computador encontrar parênteses balanceados”, e também foi divertida a observação na seção "Basic Number Theory" sobre “deixar de enxergar a pilha de parênteses de fechamento”
      Mesmo sem mexer com Lisp há muito tempo, consegui acompanhar de novo e pegar a ideia central, então achei o texto bom
    • Ainda não li muita coisa depois da introdução, mas achei interessante a premissa de que é possível provar dentro de PA que cada caso concreto da sequência de Goodstein termina em 0, mas não provar a proposição de que todas as sequências terminam
      Também é estranhamente fascinante que seja possível codificar computação usando apenas os axiomas de Peano, como se surgisse mais uma camada de autorreferência
      Comecei recentemente a estudar mais teoria dos conjuntos e cheguei até as sequências de Goodstein; gostaria de recomendações de livros-texto para o próximo nível em teoria dos conjuntos avançada ou de materiais que tratem a aritmética de Peano em profundidade
    • O Lisp em setor de boot também faz bootstrap de si mesmo: https://justine.lol/sectorlisp2/
      Vários Lisps de https://t3x.org também implementam números e o restante usando células cons e apply/eval
      O avaliador metacircular de John McCarthy é o código que Alan Kay chamou de “as equações de Maxwell do software”, e no SectorLISP ele é implementado com coisas como ASSOC EVAL EVCON APPLY EVLIS PAIRLIS
      Alguns Forths também são parecidos, e o Zenlisp da T3X explica em torno da forma como eval/apply chamam um ao outro recursivamente: http://t3x.org/zsp/index.html
    • Há dois lugares em que foi escrito “omega”, mas acho que deveria ser \omega

  • Do ponto de vista de alguém que já fez tanto matemática quanto programação, mais do que a codificação da computação em si, o mais interessante é que a independência do teorema de Goodstein possa ser contornada por esse tipo de autorreferência
    Parece significar que PA + “PA é ω-consistente” consegue provar o teorema de Goodstein, e talvez indução transfinita até ε₀ também possa ser possível de modo geral
    Edit: fico pensando se PA + “PA é consistente” já não seria suficiente

    • Como autor da pergunta original no SO, acrescentei à pergunta alguns links para respostas relacionadas
      Em essência, “PA é consistente” por si só não basta; se houver o princípio de reflexão uniforme de que “se PA prova algo, então isso é verdadeiro”, aí é suficiente
      Não tenho 100% de certeza se esse princípio é equivalente à ω-consistência, mas pelo conteúdo a seguir parece ser essa a leitura: https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relation_to_other_consistency_principles
      A Wikipedia descreve T ser ω-consistente como “T + RFN_T + o conjunto de todas as sentenças verdadeiras é consistente”, o que parece significar o mesmo que “T + RFN_T é verdadeiro”
    • Gosto dessa estrutura recursiva
      Essencialmente, você constrói uma metaprova sobre o que PA prova e, se confia em PA, acaba confiando também nessa metaprova
      Mas não entendo bem como PA + “PA é consistente” seria suficiente
      Esse sistema parece permitir um modelo em que o teorema de Goodstein é verdadeiro nos naturais padrão, mas falso para algum inteiro não padrão N; e justamente esse caso parece ser excluído pela ω-consistência, mais forte
    • Infelizmente não é assim, e parece que, só com uma fórmula puramente universal, outras coisas também não funcionam
      Ou seja, não é um problema específico de Con(PA), mas um fenômeno mais geral: https://math.stackexchange.com/questions/5003237/can-goodsteins-theorem-be-proven-in-mathrmpa-conpa
      Em relação à primeira pergunta, fico curioso sobre como codificar a ω-consistência como uma fórmula de PA
    • O post no Math Exchange diz que PA + indução transfinita sobre ε₀ prova a consistência de PA
      Então parece que PA + “PA é consistente” poderia provar a indução transfinita sobre ε₀
    • Agora os detalhes já estão um pouco fora da minha zona de conforto para eu falar com confiança
      O ChatGPT disse que PA + “PA é consistente” por si só não é suficiente e, como deve ter digerido bastante livro-texto de lógica, acho que dá para confiar nessa afirmação

  • Quando usei aritmética de Peano pela primeira vez, fiquei bastante surpreso com seu poder expressivo
    No começo ela parece um sistema básico, mas, depois que você percebe que a própria computação pode ser codificada dentro de PA e que vários tipos de computação podem ser simulados, coisas que pareciam complicadas começam a se encaixar
    Gostaria de recomendações de materiais que expliquem essas técnicas de codificação de forma amigável para iniciantes

  • Isto é muito parecido com a teoria de Boyer-Moore. Essa teoria também constrói a matemática a partir do nível dos axiomas de Peano.
    Boyer e Moore também criaram um provador automático de teoremas adaptado a essa teoria, e há uma cópia que roda em GNU Common Lisp em https://github.com/John-Nagle/nqthm/tree/master
    Segundo a explicação deles, fica fácil pensar no programa como um estudante de matemática razoavelmente bom. Se você der apenas os axiomas de Peano, é difícil esperar que ele prove ou descubra o teorema da fatoração em primos, mas, se junto com os axiomas de Peano você fornecer uma lista de teoremas como “prove a comutatividade da adição”, “prove que a multiplicação é distributiva em relação à adição”, “prove que o resultado da função GCD divide os dois argumentos”, ele consegue lidar bem com isso.
    Artigo: https://www.cs.utexas.edu/~boyer/acl.pdf

  • O comentário feito a JoJoModding no Math StackExchange está errado.
    A explicação de que “PA pode provar que ela mesma produz uma prova, mas talvez não consiga provar que essa prova tem comprimento finito” erra o ponto central.
    Se PA prova “PA prova X”, então PA pode provar X.
    O ponto importante não é que existam modelos não padrão, mas que o modelo padrão dos números naturais é um modelo de PA.
    Portanto, se PA prova “PA prova X”, então de fato existe um número natural finito padrão que corresponde à prova codificada de “PA prova X”, e com esse número é possível construir uma prova de X dentro de PA.

    • A versão em linguagem natural apresentada é ambígua, então a distinção é importante.
      O que foi mostrado não é “PA prova Provable(forall n, G(n))”, mas sim “PA prova forall n, Provable(G(n))”.
      No primeiro caso, de fato se seguiria que “PA prova forall n, G(n)”, mas o segundo é diferente.
      Sem fazer referência às sequências de Goodstein, eu gostaria de ver um argumento de que, para uma proposição geral P, provar forall n, Provable(P(n)) não permite provar Provable(forall n, P(n)).
    • A afirmação “se PA prova ‘PA prova X’, então PA prova X” não é verdadeira.
      Dentro de PA, é possível construir uma função que pesquisa todas as provas que PA pode produzir e, com base nisso, criar uma função will-return que analisa se determinada função e entrada irão retornar.
      Isso se parece com uma tentativa de resolver o problema da parada, então nem sempre funciona, mas funciona em muitos casos.
      Se então criarmos opposite-return, ela pode ser construída para tentar retornar quando a função e a entrada dadas não retornam, e para não retornar quando retornam.
      Considerando (opposite-return opposite-return opposite-return) da mesma forma que na prova padrão do problema da parada, PA pode provar que “se PA puder provar que opposite-return retorna, então na verdade ela não retorna”, “se PA puder provar que ela não retorna, então na verdade ela retorna”, “se PA puder realmente provar tudo aquilo que prova que ela mesma prova, então deve ter uma prova de uma das duas proposições anteriores”, “portanto, nesse caso, PA é inconsistente”.
      Isso é uma forma do segundo teorema da incompletude de Gödel, e por isso “PA prova” e “PA prova que ela mesma prova” precisam ser distinguidos.
    • O fato de o modelo padrão ser um modelo de PA só vale quando PA é consistente, e PA não pode provar sua própria consistência. A menos que seja inconsistente, isso é impossível por causa do teorema de Gödel.
      Portanto, a prova proposta não funciona dentro de PA, e parece que esse é justamente o ponto do comentário.

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

  • Conversando com alguém sobre tipos de dados indutivos, mostrei uma definição zero/succ como o Nat do Lean ou do Rocq.
    A outra pessoa perguntou: “isso é tudo? E os axiomas de Peano? Existe algo mais primitivo que tipos de dados indutivos?”, e achei interessante.
    Isso me lembrou que é melhor ver os axiomas de Peano como uma dentre várias escolhas de projeto, em vez de algo obviamente embutido.

    • Vejo os números naturais como mais primitivos que tipos de dados indutivos.
      Isso porque todo tipo de dado indutivo pode ser construído usando números naturais junto com construtores primitivos de tipos, por exemplo Π, Σ, =, Ω etc.

  • Apenas o cálculo lambda puro também é suficiente. Isso porque o cálculo lambda codifica a computação.

  • Sobre a consistência de PA, é possível provar dentro de PA: https://youtu.be/6pjLmmkZnIA

    • Para quem não é lógico, o contexto é indispensável.
      O segundo teorema da incompletude de Gödel mostra que, se PA puder provar sua própria consistência, então PA é inconsistente e, portanto, pode provar qualquer coisa, incluindo falsidades.
      O trabalho linkado não mostrou uma inconsistência de PA; ele definiu um novo sentido mais fraco para a afirmação de que PA “prova sua própria consistência” e então mostrou que PA consegue fazer essa coisa mais fraca.
      É um trabalho interessante, mas só faz sentido para quem já sabe bastante lógica.

  • Este texto recebeu 123 pontos, mas o post do SO linkado tem apenas 11 votos positivos.

    • No Stack Overflow, é preciso ter 15 pontos de reputação para votar positivamente.
      Somando a reputação de que postar ali torna fácil ter o conteúdo apagado com o limite de 15 pontos, parece que muita gente não consegue votar positivamente.