Yhyjyk

As referências deste artigo necessitam de formatação (desde julho de 2015). Por favor, utilize fontes apropriadas contendo referência ao título, autor, data e fonte de publicação do trabalho para que o artigo permaneça verificável no futuro.

Em matemática, o Teorema de Aceleração de Gödel, provado por Kurt Gödel (1936), demonstra que existem teoremas cujas provas podem ser drasticamente reduzidas ao se trabalhar em sistemas axiomáticos mais fortes.

Gödel mostrou como encontrar exemplos explícitos de declarações em sistemas formais que são demonstráveis em tais sistemas, porém cuja menor prova é absurdamente longa. Por exemplo, a declaração:

“Esta declaração não pode ser demonstrada na aritmética de Peano em menos de googolplex símbolos”

é demonstrável na aritmética de Peano (Aritmética de Peano), mas a sua prova mais curta tem pelo menos googolplex símbolos, por um argumento similar à prova do Primeiro Teorema da Incompletude de Gödel: AP (se consistente) não pode provar a declaração em menos de googolplex símbolos, por que a existência de tal prova seria ela mesma um teorema de AP, que viria a contradizer a declaração que AP supostamente provou. Porém ao simplesmente enumerar todas as strings de tamanho até um googolplex e checando se tal string não é uma prova (em AP) da declaração, provém uma prova da declaração que é necessariamente mais longa que googolplex símbolos.

A declaração tem uma prova menor em um sistema mais forte: na realidade é facilmente demonstrável na aritmética de Peano junto com a declaração de que AP é consistente (o que, devido ao teorema da incompletude, não pode ser provado na aritmética de Peano).

Neste argumento, a aritmética de Peano pode ser substituída por um sistema consistente mais forte, e um googolplex pode ser substituído por qualquer número que pode ser descrito concisamente neste sistema.
Harvey Friedman achou alguns exemplos naturais explícitos deste problema, provendo declarações explicitas em aritmética de Peano e outros sistemas formais cujas provas são absurdamente grandes (Smorynski 1982).

Ver também |

Teorema da Aceleração de Blum

References |

• 
  Buss, Samuel R. (1994), «On Gödel's theorems on lengths of proofs. I. Number of lines and speedup for arithmetics», The Journal of Symbolic Logic, ISSN 0022-4812, 59 (3): 737–756, MR 1295967, doi:10.2307/2275906 
  


• 
  Buss, Samuel R. (1995), «On Gödel's theorems on lengths of proofs. II. Lower bounds for recognizing k symbol provability», in: Clote, Peter; Remmel, Jeffrey, Feasible mathematics, II (Ithaca, NY, 1992), ISBN 978-0-8176-3675-3, Progr. Comput. Sci. Appl. Logic, 13, Boston, MA: Birkhäuser Boston, pp. 57–90, MR 1322274 
  


• 
  Gödel, Kurt (1936), «Über die Länge von Beweisen», Ergebinisse eines mathematischen Kolloquiums (em German), 7: 23–24, Reprinted with English translation in volume 1 of his collected works.  !CS1 manut: Língua não reconhecida (link)
  


• 
  Smoryński, C. (1982), «The varieties of arboreal experience», Math. Intelligencer, 4 (4): 182–189, MR 0685558, doi:10.1007/bf03023553