| rdfs:comment
| - En logique mathématique, le théorème d'accélération de Gödel (ou théorème de speed-up), démontré par Kurt Gödel en 1936, montre l'existence de théorèmes ayant des démonstrations très longues, mais qui peuvent être considérablement raccourcies en utilisant un système d'axiomes légèrement plus puissant. (fr)
- ゲーデルの加速定理（ゲーデルのかそくていり、英: Gödel's speedup theorem）は、クルト・ゲーデルにより証明された、数理論理学における定理である。この定理によれば、弱い形式的体系では非常に長い形式的証明しか存在しないが、より強い形式的体系では極めて短い形式的証明が存在する、というような文が存在する。より正確にいえば、それはn階算術の体系で証明可能な命題であって、n+1階算術ではより短い証明を持つものが存在するというものである。 (ja)
- In mathematics, Gödel's speed-up theorem, proved by Gödel, shows that there are theorems whose proofs can be drastically shortened by working in more powerful axiomatic systems. Kurt Gödel showed how to find explicit examples of statements in formal systems that are provable in that system but whose shortest proof is unimaginably long. For example, the statement: "This statement cannot be proved in Peano arithmetic in fewer than a googolplex symbols" (en)
- 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” (pt)
|
| has abstract
| - In mathematics, Gödel's speed-up theorem, proved by Gödel, shows that there are theorems whose proofs can be drastically shortened by working in more powerful axiomatic systems. Kurt Gödel showed how to find explicit examples of statements in formal systems that are provable in that system but whose shortest proof is unimaginably long. For example, the statement: "This statement cannot be proved in Peano arithmetic in fewer than a googolplex symbols" is provable in Peano arithmetic (PA) but the shortest proof has at least a googolplex symbols, by an argument similar to the proof of Gödel's first incompleteness theorem: If PA is consistent, then it cannot prove the statement in fewer than a googolplex symbols, because the existence of such a proof would itself be a theorem of PA, a contradiction. But simply enumerating all strings of length up to a googolplex and checking that each such string is not a proof (in PA) of the statement, yields a proof of the statement (which is necessarily longer than a googolplex symbols). The statement has a short proof in a more powerful system: in fact the proof given in the previous paragraph is a proof in the system of Peano arithmetic plus the statement "Peano arithmetic is consistent" (which, per the incompleteness theorem, cannot be proved in Peano arithmetic). In this argument, Peano arithmetic can be replaced by any more powerful consistent system, and a googolplex can be replaced by any number that can be described concisely in the system. Harvey Friedman found some explicit natural examples of this phenomenon, giving some explicit statements in Peano arithmetic and other formal systems whose shortest proofs are ridiculously long. For example, the statement "there is an integer n such that if there is a sequence of rooted trees T1, T2, ..., Tn such that Tk has at most k+10 vertices, then some tree can be homeomorphically embedded in a later one" is provable in Peano arithmetic, but the shortest proof has length at least A(1000), where A(0)=1 and A(n+1)=2A(n). The statement is a special case of Kruskal's theorem and has a short proof in second order arithmetic. If one takes Peano arithmetic together with the negation of the statement above, one obtains an inconsistent theory whose shortest known contradiction is equivalently long. (en)
- En logique mathématique, le théorème d'accélération de Gödel (ou théorème de speed-up), démontré par Kurt Gödel en 1936, montre l'existence de théorèmes ayant des démonstrations très longues, mais qui peuvent être considérablement raccourcies en utilisant un système d'axiomes légèrement plus puissant. (fr)
- ゲーデルの加速定理（ゲーデルのかそくていり、英: Gödel's speedup theorem）は、クルト・ゲーデルにより証明された、数理論理学における定理である。この定理によれば、弱い形式的体系では非常に長い形式的証明しか存在しないが、より強い形式的体系では極めて短い形式的証明が存在する、というような文が存在する。より正確にいえば、それはn階算術の体系で証明可能な命題であって、n+1階算術ではより短い証明を持つものが存在するというものである。 (ja)
- 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). (pt)
|
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)