ゲーデルの加速定理とは - わかりやすく解説 Weblio辞書

すべての辞書から再検索する

ウィキペディア

索引トップ用語の索引ランキングカテゴリー

ゲーデルの加速定理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/09/01 15:58 UTC 版)

ゲーデルの加速定理（ゲーデルのかそくていり、英: Gödel's speedup theorem）は、クルト・ゲーデル^[1]により証明された、数理論理学における定理である。この定理によれば、弱い形式的体系では非常に長い形式的証明しか存在しないが、より強い形式的体系では極めて短い形式的証明が存在する、というような文が存在する。より正確にいえば、それはn階算術の体系で証明可能な命題であって、n+1階算術ではより短い証明を持つものが存在するというものである。

注釈

^ もっとも、この場合は文そのものにとてつもなく長大な数字（グーゴルプレックス）が埋め込まれているかもしれず、それが原因で証明が長くなってしまっている可能性を排除できない。この可能性を排除する為には、次のようにすればよい。論理式 $\pi (x,y)$ を「 $x$ （をコードとして持つ論理式）は高々 $y$ 個の記号からなる形式的証明を持たない」という論理式とする。この論理式は $\Delta _{1}(PA)$ で書ける。グーゴルプレックスを（ペアノ算術において）定義する短い $\Delta _{1}(PA)$ -論理式 $\psi (x)$ を見出す。すると $PA\vdash \forall y(\psi (y)\to \pi (x,y))\equiv \exists y(\psi (y)\land \pi (x,y))$ であるから、この同値な $\Delta _{1}(PA)$ -論理式を $\pi (x)$ とおく。形式化された対角線論法によって $PA\vdash \varphi \equiv \pi (\lceil \varphi \rceil )$ を満たす $\varphi$ が得られる。この $\varphi$ は前述の文と同じ内容を持つが、その長さはグーゴルプレックスより遥かに短い。

出典

^ Gödel, Kurt (1936), “Über die Länge von Beweisen” (German), Ergebinisse eines mathematischen Kolloquiums 7: 23–24, Reprinted with English translation in volume 1 of his collected works.
^ Smoryński, C. (1982), “The varieties of arboreal experience”, Math. Intelligencer 4 (4): 182–189, doi:10.1007/bf03023553, MR 0685558
^ Andrzej Ehrenfeucht and Jan Mycielski (1971), Abbreviating proofs by adding new axioms, Bulletin of the American Mathematical Society 77(3): 366-367.
^ Keita Yokoyama (2010), Formalizing non-standard arguments in second-order arithmetic, Journal of Symbolic Logic 75(4): 1199-1210.
^ 菊地誠（2014）『不完全性定理』共立出版