A aritmética de Peano é suficiente, porque a aritmética de Peano consegue codificar computação

• A aritmética de Peano (PA) consegue expressar processos mecânicos de computação, portanto é possível provar em PA a extinção de toda sequência individual de Goodstein
• Por meio da forma normal de Cantor e da notação hereditária de ordinais, é possível expressar sequências de Goodstein e seu decrescimento, o que torna possível construir provas de comprimento finito
• Por meio de indução (indução forte/indução transfinita), é possível estender as provas separadamente até ordinais de certa ordem
• A PA pode provar, para todo número natural n, que “G(n) chega a 0”, mas não é possível uma prova total do teorema de Goodstein inteiro (para todo n)
• A PA é suficiente para implementar a codificação de computação, estruturas de dados (List, Pair etc.) e até da própria linguagem de programação (Lisp), além da codificação do próprio processo de prova

---

Introdução e contexto do problema

• Este texto descreve que a aritmética de Peano (PA) pode provar que a sequência de Goodstein “para cada n chega a 0 (G(n) terminates)”
• Isso pode parecer óbvio para lógicos, mas é explicado da perspectiva da codificação de computação para que programadores consigam entender
• Para cada caso de sequência de Goodstein, é possível construir uma rotina concreta de prova dentro da PA

Ordinals (números ordinais) e sequências de Goodstein

• Os ordinais (Sets as Ordinals) são gerados no estilo de Von Neumann
  • 0 é o conjunto vazio, 1 é {0}, 2 é {0,1}, ω é {0,1,2,…}, ω+1 é {0,1,2,…,ω} etc., com a ordem bem definida
• A sequência de Goodstein é descrita por meio de notação hereditária em base usando a forma normal de Cantor
  • Ex.: ω^ω é ((1,ω)), isto é, ((1,(1,1)))
  • A ordem < é determinada por comparação lexicográfica dos ordinais/coefs de cada termo

Indução e indução transfinita

• Indução na aritmética de Peano: se vale para 0 e se vale para n→n+1, então vale para todos os números naturais
• Indução forte também pode ser provada em PA
• Indução transfinita: em ZFC etc., ela pode ser estendida a ordinais infinitos e aplicada a números escritos na forma normal de Cantor
  • Teorema 1: uma sequência decrescente na forma normal de Cantor é sempre finita
  • Teorema 2: é possível usar indução transfinita para números na forma normal de Cantor

Indução transfinita em PA e comprimento da prova das sequências de Goodstein

• A PA consegue gerar uma prova da extinção da sequência de Goodstein para qualquer n
  • É possível construir a prova de acordo com a altura da torre m=O(log* n) (logaritmo iterado) da forma normal de Cantor
  • Combinando m provas por etapa, o comprimento total da prova é O(m^2), ou pode ser reduzido para O(m log m) com a introdução de uma notação especial (ω[m])
• No entanto, uma prova do teorema de Goodstein completo (para todo n) é impossível em PA (não é possível indução transfinita até ε0)
  • Se isso fosse possível, também seria possível provar a consistência da própria PA, o que entraria em conflito com a segunda incompletude de Gödel

Codificação de programas e estruturas de dados em PA

• A PA consegue codificar suficientemente computação/programas/estruturas de dados (números, pares, listas e qualquer outra estrutura)
• É possível implementar várias funcionalidades das seguintes formas:
  • lógica e operações básicas (+, *, pow, //, %, min, max etc.)
  • pattern matching e desvio condicional (if, cond etc.)
  • codificar um número como dois números (par) e expandir repetidamente de par para lista e para estruturas mais complexas (listas recursivas, árvores, texto etc.)
• Com essa codificação de estruturas de dados, é possível construir até mesmo um interpretador para máquina virtual/linguagem de programação arbitrária (como Lisp)

Bootstrap para Lisp e codificação

• Usando Lisp como exemplo, o texto explica como implementar operações numéricas e lógicas básicas, estruturas de dados e um interpretador/interpreter de linguagem de programação
• Toda a estrutura do Lisp (mapeamento de comandos/argumentos, formas especiais, macro etc.) pode ser implementada em PA por combinações adequadas de funções
• Indo além, é possível codificar e implementar simbolicamente em PA o próprio processo de prova em PA, procedimentos de prova lógica e estruturas autorreferenciais

Codificação da própria lógica dentro de PA

• Em lógica matemática, o processo de prova da lógica de primeira ordem pode ser codificado como dados numéricos da PA
• Cada etapa da prova/proposição/regra de inferência/verificação de prova válida pode ser reconhecida e processada como uma série de funções numéricas e processamento de listas
• Essa codificação metateórica e autorreferencial leva às provas da incompletude de Gödel e do problema da parada

Conclusão

• Computação, estruturas de dados, programas e até processos de prova lógica podem ser suficientemente codificados, provados e interpretados em PA
• Portanto, qualquer sequência de Goodstein (para n, a extinção de G(n)) pode ser provada concretamente dentro da PA
• No entanto, uma prova de que “a PA prova o teorema de Goodstein dentro da própria PA” para o teorema inteiro (todo n) é impossível devido aos limites da lógica
• Do ponto de vista do programador, a PA é uma base lógica completa capaz de codificar a própria computação

[GN⁺]

Comentários no Hacker News

• Este texto é uma versão em post de blog de algo que perguntei no Stack Overflow. Inclui uma explicação sobre os limites do que pode ser provado no sistema de axiomas de Peano e sobre como fazer bootstrap de Lisp dentro da aritmética de Peano. A maioria das piadas está na segunda seção. Correções ou perguntas adicionais são bem-vindas.
  • Lendo este texto, encontrei um trecho com parênteses desbalanceados na seção "Why Lisp?" (veja o exemplo (defun not (x) (if x false true)). Quando alguém começa a usar parênteses, eu instintivamente verifico se eles estão corretamente fechados. Depois, quando o texto menciona que "é fácil programar um computador para verificar se os parênteses estão balanceados", eu ri alto. Esse tipo de piada foi muito engraçado, e também achei marcante o comentário ; After a while, you stop noticing that stack of closing parens. na seção "Basic Number Theory". Fazia tempo que eu não reencontrava Lisp, e o texto foi realmente divertido.
  • Este texto é realmente fascinante. Ainda só li a introdução, mas é interessante que, dentro da aritmética de Peano (PA), seja possível provar que todo caso particular de uma sequência de Goodstein chega a 0, mas não seja possível provar que todos os casos chegam a 0. É interessante e empolgante, mesmo que no fundo seja um resultado esperado. E o fato de que só com a aritmética de Peano já se consegue codificar computação é realmente estranho; em princípio é natural, mas eu nunca tinha pensado em mais esse nível de autorreferência. Por coincidência, recentemente venho tentando estudar mais teoria dos conjuntos e cheguei justamente à parte sobre sequências de Goodstein em Intro to Set Theory. Se alguém tiver alguma recomendação de livro avançado de teoria dos conjuntos, ou de algum texto que aprofunde bastante a aritmética de Peano, eu agradeceria. Um pequeno objetivo meu é entender por que a PA não basta para provar o teorema de Goodstein, mas também aceito recomendações de outros caminhos.
  • Em dois lugares com ômega no texto, esqueceram de escrever \omega.
• Isso é muito parecido com a teoria de Boyer-Moore. Essa teoria constrói matemática no nível da aritmética de Peano. Boyer e Moore desenvolveram um provador automático de teoremas que implementa essa teoria, e também existe uma cópia que roda em GNU Common LISP. Vale a pena ver o artigo "A Computational Logic" e a implementação do nqthm. No artigo, achei especialmente marcante o ponto de que, começando com os axiomas de Peano, teoremas complicados como a multiplicação de números primos são difíceis, mas ainda assim é plenamente possível provar a comutatividade da adição, a distributividade da multiplicação e teoremas sobre a função GCD.
• Tenho formação tanto em matemática quanto em programação, e pessoalmente acho mais interessante o fato de que a parte da independência do teorema de Goodstein talvez possa ser contornada de maneira autorreferente. Imagino que, se adicionarmos à PA a hipótese "PA é ômega-consistente", então talvez fosse possível provar o teorema de Goodstein; e suspeito que isso também permitiria indução transfinita até epsilon_0. EDIT: talvez até só "PA é consistente" já bastasse?
  • Infelizmente não. E há o fato de que não basta nem mesmo Con(PA), nem qualquer fórmula universalmente quantificada. Veja esta resposta relacionada no Math StackExchange. Quanto à primeira pergunta, fiquei curioso sobre como exatamente se codifica ômega-consistência como uma fórmula de PA; isso não me veio imediatamente à cabeça.
  • Eu sou o autor da pergunta no Stack Overflow. Acrescentei alguns links para respostas na pergunta. Essencialmente, só "PA é consistente" não basta, mas algo como o "princípio de reflexão uniforme" — isto é, "se PA prova, então é verdadeiro" — seria suficiente. Não posso afirmar com certeza que isso seja exatamente igual a ômega-consistência, mas pela explicação da Wikipédia parece ser isso. Se T é ômega-consistente, isso significa que T + RFN_T + o conjunto de todas as fórmulas verdadeiras é consistente, e isso pode ser interpretado como equivalente a dizer que T + RFN_T é verdadeiro.
  • Também gosto dessa estrutura indutiva/recursiva. No fim, você constrói uma metaprova sobre o que a PA prova, e se confia na PA, então parece razoável confiar também nessa metaprova. A parte de dizer que simplesmente "PA é consistente" seria suficiente eu não entendo com segurança. Na minha visão, PA + "PA é consistente" permitiria que existisse um modelo em que o teorema de Goodstein fosse verdadeiro nos números naturais padrão, mas ao mesmo tempo um modelo em que ele fosse falso para algum inteiro não padrão N. Acho que a afirmação mais forte de ômega-consistência excluiria esses casos.
  • No post do Math StackExchange foi mencionado que uma prova em PA + indução transfinita até epsilon_0 prova a própria PA. Eu achava que PA + "PA é consistente" já permitiria provar indução transfinita até epsilon_0.
  • Acho que esse assunto já está entrando em detalhes além do que eu consigo comentar com segurança. Segundo o ChatGPT, só PA + "PA é consistente" não basta. Como o ChatGPT aparentemente já devorou muitos livros de lógica, dá vontade de confiar quando ele diz isso.
• O comentário que escrevi para JoJoModding no Stack Overflow não está correto. Eu havia dito que "em modelos não padrão de PA existem números naturais infinitos, então, mesmo que PA prove que produziu alguma prova, ela não consegue provar que essa prova tem comprimento finito". Mas, na verdade, se a PA prova "PA provou X", então a própria PA também prova X. O ponto importante não é a existência de modelos não padrão, e sim o fato de que o modelo padrão dos números naturais é um modelo de PA. Portanto, se "PA prova que prova X", então isso efetivamente gera uma prova correspondente a um número natural finito padrão, e usando esse número é possível construir, dentro da própria PA, uma prova real de X.
  • Não tenho tempo de revisar a lógica em mais detalhe, mas em linguagem natural parece que a diferença crucial é entre "PA prova forall n, G(n)" e "PA prova forall n, Provable(G(n))". Não sou muito forte em lógica, então, se alguém puder explicar concretamente por que provar forall n, Provable(P(n)) não permite provar Provable(forall n, P(n)), eu agradeceria.
  • A proposição "se PA prova 'PA prova X', então PA prova X" não está correta. É possível construir em PA uma função que busca todas as provas possíveis, e eu de fato esbocei esse método no fim da resposta. A partir disso também se podem construir funções como will-return e opposite-return, o que coincide com a prova padrão do problema da parada. Se você considerar o caso opposite-return(opposite-return, opposite-return), então, se a PA provar que opposite-return retorna, ela também prova que na verdade não retorna; e, se provar que não retorna, prova que retorna. Se a PA adotasse uma afirmação mais forte do tipo "tudo o que é demonstrável é de fato demonstrável", isso equivaleria à segunda incompletude de Gödel e significaria que a PA é inconsistente. Portanto, é indispensável distinguir entre "PA prova" e "PA prova que prova".
• Só o cálculo lambda puro já basta, porque o próprio cálculo lambda codifica computação.
• Eu estava conversando com alguém sobre tipos de dados indutivos e mostrei a definição de Nat feita com zero/succ (como se vê em Lean ou Rocq). A pessoa ficou se perguntando: "isso por si só basta?", "é preciso a aritmética de Peano?", "existe algo mais primitivo do que tipos de dados indutivos?" e coisas assim. Isso me fez pensar que é bom lembrar com frequência que a aritmética de Peano não deve ser tratada como algo essencialmente óbvio; ela é apenas um projeto possível.
  • Como resposta para "existe algo mais fundamental do que tipos de dados indutivos?", eu diria que os próprios números naturais são mais primitivos do que tipos de dados indutivos. Todo tipo de dado indutivo pode ser construído apenas com números naturais e alguns poucos construtores de tipos primitivos (Π, Σ, =, Ω).
• Veja também este Q&A sobre o teorema de Kirby-Paris.
• Sobre consistência de PA, compartilho um vídeo mostrando que isso é demonstrável dentro da própria PA: link do YouTube
  • Esse é um ponto que precisa muito de explicação para quem não é da área de lógica. Pelo segundo teorema da incompletude de Gödel, se a PA pudesse provar a própria consistência, então a PA seria inconsistente e passaria a provar qualquer coisa, inclusive falsidades. Este vídeo não prova que a PA é inconsistente; ele mostra que, em um sentido mais fraco, a PA pode provar sua "própria consistência". Sem conhecer os fundamentos de lógica, é difícil entender exatamente o que está sendo dito, mas ainda assim é algo bastante interessante.
• Esse tema está com 123 pontos, mas o post original no SO tem só 11 votos positivos.
  • No Stack Overflow é preciso ter 15 pontos para poder dar upvote. Às vezes as pessoas não se animam a postar por causa da reputação, e esse limite de 15 pontos também parece inibir os upvotes.
• Computação por si só basta? Os números reais computáveis são apenas um subconjunto de todos os números reais.
  • Acho que o próprio nome "números reais" induz a uma interpretação enganosa. Dá para entender reais como razões físicas efetivas. Por exemplo, quando se diz 180,255 libras, isso pode significar a razão física real entre o peso verdadeiro de Jones e a libra-padrão. Essas razões também existem fisicamente, então os números reais podem ser interpretados como razões físicas. Por outro lado, hoje prevalece a visão de número como conceito abstrato separado da realidade, algo tipicamente associado ao platonismo. Mas, no mundo real, medir ou representar qualquer coisa com precisão infinita é impossível. Por exemplo, medições com mais de 50 dígitos de precisão seriam inviáveis por limitações da mecânica quântica. Se você quisesse medir sem erro a órbita dos corpos do sistema solar, acima de 50 dígitos seria preciso considerar o efeito gravitacional de estrelas vizinhas; acima de 100, seria necessário modelar a galáxia inteira; e assim por diante, até influências físicas que não podem ser medidas de fato. Então, na prática, só a matemática de precisão finita é possível. Em princípio tudo é computável, mas, no infinito, o próprio modelo matemático deixa de fazer sentido.
  • Será mesmo? Na verdade, a ideia de que há mais objetos incontáveis nasce de um mal-entendido. Veja minha explicação. Se você aceita que o incontável é "maior", então inevitavelmente assume uma posição controversa sobre o que significa "existir". Veja também esta discussão relacionada. Por fim, mesmo que levemos o raciocínio lógico até o fim, tudo ainda pode ser expresso em um computador. Mesmo adicionando grandes conjuntos ao ZFC, ainda é possível partir da PA e inferir qualquer conclusão arbitrária, então, na prática, considero que só a PA já basta. Se for preciso mais persuasão, recomendo o livro Gödel, Escher, Bach.
  • Minha abordagem é um pouco diferente. Números reais em geral não podem ser manipulados de nenhuma forma — nem por computação, nem por simbolização, nem por registro —, mas as proposições sobre números reais muitas vezes podem ser expressas e trabalhadas de forma útil. Acho realmente fascinante, como fazem Harvey Friedman ou o autor deste texto, tentar produzir valores de complexidade surpreendente dentro de sistemas simples. (Observação: o site audiomulch não está acessível.)
  • Sem um objetivo associado a "basta", a pergunta fica mal definida. O importante é: basta para quê?
  • Acho que a própria pergunta "computação por si só basta?" está errada. Claro que não basta; se bastasse, então uma certa visão do mundo como um mecanismo de relógio facilmente confiável estaria correta. A realidade é muito mais interessante e muito mais complexa do que isso.