ゲーデルの加速定理

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

現実的には証明できない命題

具体的な例を見るために、最短の形式的証明がとてつもなく長大となる文を構成しよう。形式化された対角線論法によって

φ「この文は高々グーゴルプレックス個の記号からなる（ペアノ算術からの）形式的証明を持たない」

なる内容的意味を持つ文を構成する。（ここで「グーゴルプレックス個の記号からなる」という部分を取り除くと不完全性定理の決定不能な文が得られる。）コーディングを工夫すれば φ がΣ₁論理式となるようにできる。φ はペアノ算術から証明可能である：もし証明不能なら「高々グーゴルプレックス個の記号からなる（ペアノ算術からの）形式的証明を持たない」が標準模型で真なので、Σ₁完全性より φ は証明可能である。これは不合理。したがって φ は証明可能である。するとΣ₁健全性より φ は標準模型で真である。つまり「φ は高々グーゴルプレックス個の記号からなる（ペアノ算術からの）形式的証明を持たない」から、φ の形式的証明はグーゴルプレックス個よりも多くの記号から構成される。

φはより強い体系ではもっと短い形式的証明を持つ：例えばペアノ算術に自身の無矛盾性を表す公理 Con(PA) を追加した体系を用いればよい。（追加された公理は不完全性定理よりペアノ算術からは証明不能である。）すると、上の背理法による議論を体系内で実行することができ、より短い形式的証明が得られる： ¬φ と仮定する。ここから Provable_PA(φ) を得る。他方で ¬φ に形式化されたΣ₁完全性を適用すれば Provable_PA(¬φ) を得る。ここに形式化されたモーダス・ポネンスを適用すれば Provable_PA(⊥) すなわち ¬Con(PA) を得る。公理 Con(PA) とモーダス・ポネンスによって矛盾 ⊥ を得る。背理法によって（仮定なしで） φ を得る。

以上の議論におけるペアノ算術は、別のより強い無矛盾な体系に置き換えられる。またグーゴルプレックスもその体系で（短く）記述できる別の任意の数字に置き換えられる。

ハービー・フリードマンは上のような性質を満たすような明示的で自然な例をいくつか見つけた。それはペアノ算術やほかの形式的体系における文であり、その最短の証明は非常に長い。例えば、以下の主張

「ある自然数 $n$ が存在して、もし根付き木からなる列 $T_{1},\ldots ,T_{n}$ で $T_{k}$ が高々 $k+10$ 頂点からなるとき、 ある木はそれより後の木へ同相的に埋め込める」

はペアノ算術において証明可能だが、その最短の証明は少なくとも長さ $A(1000)$ を持つ。ここで $A(0)=1$ かつ $A(n+1)=2^{A(n)}$ である。この主張はクラスカルの定理の特別な場合であり、二階算術においてより短い証明を持つ。

ペアノ算術に上記の主張の否定を付け加えたならば、矛盾した理論であって、その最短の矛盾（の証明）が想像を絶するほどに長いものが得られる。上記の主張を $\varphi$ とおく。いま $PA+\neg \varphi$ から矛盾に至る証明が与えられたとする。すると（論理が適切に形式化されている限り）証明の長さを定数倍程度しか増やさない仕方で、$PA$ から $\varphi$ に至る証明が得られる。（例えば、ベースとなる論理体系が帰謬法を推論規則として陽に含む場合、証明の長さは1ステップ分しか増えない。）後者の証明は途轍もなく長いので、前者の証明もまた途轍もなく長い。

エーレンフォイヒト・ミッシェルスキーの加速定理

帰納的理論 $T$ と文 $\varphi$ について $T+\neg \varphi$ は決定不可能であると仮定する。したがってとくに $\varphi$ は $T$ で証明できない。この条件を満たす例としては、ロビンソン算術と加法や乗法の交換法則、ペアノ算術とグッドスタインの定理やパリス・ハーリントンの定理、ZFと選択公理や決定性公理、ZFCと連続体仮説や巨大基数公理などがある。

$T$ における証明と $T+\varphi$ における証明の複雑性を比較したい。ただし証明の複雑性を測る関数 $|\cdot |$ は静的複雑性測度の条件を満たすものとする。すなわち、証明の複雑さの上限を固定する毎に、その複雑さ未満の証明は有限個に限られ、かつそのような証明全体の成す有限集合を（与えられた上限から）計算できるものとする。理論 $T'$ における文 $\psi$ の証明の複雑さの最小値を $\Vert \psi \Vert _{T'}$ と書くことにする。この証明の最小の複雑さを与える関数は（証明可能な文全体を定義域とする）計算可能関数である。

エーレンフォイヒトとミッシェルスキーは計算可能性理論を用いて次の加速定理を証明した：

任意の計算可能関数 $r$ に対して、$T$ で証明可能な文 $\psi$ が存在して $r(\Vert \psi \Vert _{T+\varphi })\leq \Vert \psi \Vert _{T}$ が成り立つ。

例えば $r(x)=2x$ とすると $2\Vert \psi \Vert _{T+\varphi }\leq \Vert \psi \Vert _{T}$ より $\Vert \psi \Vert _{T+\varphi }\leq \Vert \psi \Vert _{T}/2$ となる。つまり証明のサイズが半分に落ちる。同様に、$r$ を指数関数とすれば、後式の右辺は対数関数となる。このように、増加の激しい関数 $r$ を取る毎に、その逆関数（これは増加が緩やかとなる）に対応した証明の短縮（加速）が起こる。

証明

いま $T+\varphi$ で証明できて $T$ で証明できない文（つまり「新しい定理」）の全体を $D$ とおく。この集合の計算論的な複雑さを解析することで定理が証明される。この集合は次のように性質を持つ：

$\varphi \vee \psi \in D\iff T\not \vdash \varphi \vee \psi \iff T+\neg \varphi \not \vdash \psi .$

したがって $D$ は帰納的可算でない。ただしd-帰納的可算ではある。

いま加速定理の主張が成立しないと仮定してみよう。つまり、$T+\varphi$ で証明可能な任意の文 $\psi$ に対して、

$T\vdash \psi$ ならば $r(\Vert \psi \Vert _{T+\varphi })>\Vert \psi \Vert _{T}$

が成り立つ。よって、$T+\varphi$ で証明可能な定理 $\psi$ が「新しい定理」であるか否かは、$T$ から複雑さ $r(\Vert \psi \Vert _{T+\varphi })$ 以下で証明可能であるか否かを見ればよい。すなわち、前記の集合 $D$ は次を満たす：

$\psi \in D\iff$ $T+\varphi \vdash \psi$ かつ、複雑さ $r(\Vert \psi \Vert _{T+\varphi })$ 未満の $\Pi$ はどれも $T\vdash \psi$ の証明ではない。

ここで静的複雑性の条件より、$\Pi$ に関する全称量化は有界量化と見做せる。ゆえに $D$ は帰納的可算である。これは上で示したことに反する。

なお、この存在証明は帰謬法に基づいているので、具体的にどのような文が加速されるのかは教えてくれない。

限界

この定理は同じ言語で書かれたふたつの理論の間の加速可能性しか教えてくれない。理論 $T$ が言語 $L$ で書かれ、理論 $T'\supsetneq T$ が言語 $L'\supsetneq L$ で書かれている場合、この定理は加速可能な $L'$-文の存在は教えてくれるが、加速可能な $L$-文の存在は教えてくれない。例えば、二階算術の部分体系ACA₀とその超準的な拡大理論との間には、多項式増大度を越える加速定理が成立しないことが知られている。すなわち言語の拡大を伴う場合には反例が存在する。

また $T$ が帰納的でない場合にも反例が存在する。例えば $T,\varphi$ を定理の条件を満たすペアとする。$T$ で証明可能な文全体（演繹閉包） $T'$ と $\varphi$ は帰納性の条件を除いて定理の条件を満たす。$T'$ で証明可能な任意の文 $\psi$ は

$\psi$

とだけ書かれた証明を持つ。（厳密には「$T'$ における証明」の形式化の仕方に依存するが、以下の議論は、適当な修正のもとで、どんなリーズナブルな形式化にも通用する。）一般に $\psi$ とだけ書かれた（ベースとなる論理における）推論の複雑さを $f(\psi )$ と定義する。すると $\Vert \psi \Vert _{T'}\leq f(\psi )$ が成り立つ。いま $g(x)$ を「$x$ 以下の複雑さの推論の末尾（帰結）に現れる論理式 $\psi$ に対する $f(\psi )$ の総和」と定める。すると $g(\Vert \psi \Vert _{T'+\varphi })\geq f(\psi )\geq \Vert \psi \Vert _{T'}$ となる。

証明の複雑さの尺度として、証明に現れる論理式の個数や、推論規則の適用回数を採用した場合にも、やはり反例が存在する。$T$ を任意の帰納的可算理論とすると、$T$ と同値な原始帰納的理論 $\mathrm {Craig} (T)$ がクレイグのトリックによって得られる。すなわち、$\varphi _{0},\varphi _{1},\ldots$ を $T$ の定理の計算可能な枚挙とするとき、

$\mathrm {Craig} (T):=\{\varphi _{n}^{n+1}\mid n\in \mathbb {N} \}$

である。ただし $\varphi ^{n}$ は $\varphi$ の $n$ 個のコピーを論理積で結合したものとする。$\mathrm {Craig} (T)$ で証明可能な文はどれも（適切な論理体系に於いては）全く同じ形の証明を持つ。（例えば自然演繹においては $\wedge$-除去規則を一度だけ使用する形の証明を持つ。）したがって、証明に現れる論理式の個数や、推論規則の適用回数は、ともにある定数で抑えられる。

関連項目

• ブラムの加速定理
• 加速定理

参考文献

• 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 59 (3): 737–756, doi:10.2307/2275906, ISSN 0022-4812, MR1295967, https://doi.org/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), Progr. Comput. Sci. Appl. Logic, 13, Boston, MA: Birkhäuser Boston, pp. 57–90, ISBN 978-0-8176-3675-3, MR1322274 
• Parikh, Rohit (1971), “Existence and Feasibility in Arithmetic”, Journal of Symbolic Logic 36: 494-508, http://www.jstor.org/discover/10.2307/2269958?uid=3738328&uid=2133&uid=2&uid=70&uid=4&sid=21104096791051