ゲーデルの加速定理

ゲーデルの加速定理（ゲーデルのかそくていり、）は、クルト・ゲーデルにより証明された、数理論理学における定理である。この定理によれば、弱い形式的体系では非常に長い形式的証明しか存在しないが、より強い形式的体系では極めて短い形式的証明が存在する、というような文が存在する。より正確にいえば、それはn階算術の体系で証明可能な命題であって、n+1階算術ではより短い証明を持つものが存在するというものである。
現実的には証明できない命題.
具体的な例を見るために、最短の形式的証明がとてつもなく長大となる文を構成しよう。形式化された対角線論法によって
なる内容的意味を持つ文を構成する。（ここで「グーゴルプレックス個の記号からなる」という部分を取り除くと不完全性定理の決定不能な文が得られる。）コーディングを工夫すれば φ がΣ1論理式となるようにできる。φ はペアノ算術から証明可能である：もし証明不能なら「高々グーゴルプレックス個の記号からなる（ペアノ算術からの）形式的証明を持たない」が標準模型で真なので、Σ1完全性より φ は証明可能である。これは不合理。したがって φ は証明可能である。するとΣ1健全性より φ は標準模型で真である。つまり「φ は高々グーゴルプレックス個の記号からなる（ペアノ算術からの）形式的証明を持たない」から、φ の形式的証明はグーゴルプレックス個よりも多くの記号から構成される。
φはより強い体系ではもっと短い形式的証明を持つ：例えばペアノ算術に自身の無矛盾性を表す公理 Con(PA) を追加した体系を用いればよい。（追加された公理は不完全性定理よりペアノ算術からは証明不能である。）すると、上の背理法による議論を体系内で実行することができ、より短い形式的証明が得られる： ¬φ と仮定する。ここから ProvablePA(φ) を得る。他方で ¬φ に形式化されたΣ1完全性を適用すれば ProvablePA(¬φ) を得る。ここに形式化されたモーダス・ポネンスを適用すれば ProvablePA(⊥) すなわち ¬Con(PA) を得る。公理 Con(PA) とモーダス・ポネンスによって矛盾 ⊥ を得る。背理法によって（仮定なしで） φ を得る。
以上の議論におけるペアノ算術は、別のより強い無矛盾な体系に置き換えられる。またグーゴルプレックスもその体系で（短く）記述できる別の任意の数字に置き換えられる。
ハービー・フリードマンは上のような性質を満たすような明示的で自然な例をいくつか見つけた。それはペアノ算術やほかの形式的体系における文であり、その最短の証明は非常に長い。例えば、以下の主張
はペアノ算術において証明可能だが、その最短の証明は少なくとも長さ formula_5 を持つ。ここで formula_6 かつ formula_7 である。この主張はクラスカルの定理の特別な場合であり、二階算術においてより短い証明を持つ。
ペアノ算術に上記の主張の否定を付け加えたならば、矛盾した理論であって、その最短の矛盾（の証明）が想像を絶するほどに長いものが得られる。上記の主張を formula_8 とおく。いま formula_9 から矛盾に至る証明が与えられたとする。すると（論理が適切に形式化されている限り）証明の長さを定数倍程度しか増やさない仕方で、formula_10 から formula_8 に至る証明が得られる。（例えば、ベースとなる論理体系が帰謬法を推論規則として陽に含む場合、証明の長さは1ステップ分しか増えない。）後者の証明は途轍もなく長いので、前者の証明もまた途轍もなく長い。
エーレンフォイヒト・ミッシェルスキーの加速定理.
帰納的理論 formula_12 と文 formula_8 について formula_14 は決定不可能であると仮定する。したがってとくに formula_8 は formula_12 で証明できない。この条件を満たす例としては、ロビンソン算術と加法や乗法の交換法則、ペアノ算術とグッドスタインの定理や、ZFと選択公理や決定性公理、ZFCと連続体仮説や巨大基数公理などがある。
formula_12 における証明と formula_18 における証明の複雑性を比較したい。ただし証明の複雑性を測る関数 formula_19 は静的複雑性測度の条件を満たすものとする。すなわち、証明の複雑さの上限を固定する毎に、その複雑さ未満の証明は有限個に限られ、かつそのような証明全体の成す有限集合を（与えられた上限から）計算できるものとする。理論 formula_20 における文 formula_21 の証明の複雑さの最小値を formula_22 と書くことにする。この証明の最小の複雑さを与える関数は（証明可能な文全体を定義域とする）計算可能関数である。
とは計算可能性理論を用いて次の加速定理を証明した：
例えば formula_27 とすると formula_28 より formula_29 となる。つまり証明のサイズが半分に落ちる。同様に、formula_23 を指数関数とすれば、後式の右辺は対数関数となる。このように、増加の激しい関数 formula_23 を取る毎に、その逆関数（これは増加が緩やかとなる）に対応した証明の短縮（加速）が起こる。
証明.
いま formula_18 で証明できて formula_12 で証明できない文（つまり「新しい定理」）の全体を formula_34 とおく。この集合の計算論的な複雑さを解析することで定理が証明される。この集合は次のように性質を持つ：
したがって formula_34 は帰納的可算でない。ただしd-帰納的可算ではある。
いま加速定理の主張が成立しないと仮定してみよう。つまり、formula_18 で証明可能な任意の文 formula_21 に対して、
が成り立つ。よって、formula_18 で証明可能な定理 formula_21 が「新しい定理」であるか否かは、formula_12 から複雑さ formula_44 以下で証明可能であるか否かを見ればよい。すなわち、前記の集合 formula_45 は次を満たす：
ここで静的複雑性の条件より、formula_49 に関する全称量化はと見做せる。ゆえに formula_34 は帰納的可算である。これは上で示したことに反する。
なお、この存在証明は帰謬法に基づいているので、具体的にどのような文が加速されるのかは教えてくれない。
限界.
この定理は同じ言語で書かれたふたつの理論の間の加速可能性しか教えてくれない。理論 formula_12 が言語 formula_54 で書かれ、理論 formula_55 が言語 formula_56 で書かれている場合、この定理は加速可能な formula_57-文の存在は教えてくれるが、加速可能な formula_54-文の存在は教えてくれない。例えば、二階算術の部分体系ACA0とその超準的な拡大理論との間には、多項式増大度を越える加速定理が成立しないことが知られている。すなわち言語の拡大を伴う場合には反例が存在する。
また formula_12 が帰納的でない場合にも反例が存在する。例えば formula_60 を定理の条件を満たすペアとする。formula_12 で証明可能な文全体（演繹閉包） formula_20 と formula_8 は帰納性の条件を除いて定理の条件を満たす。formula_20 で証明可能な任意の文 formula_21 は
とだけ書かれた証明を持つ。（厳密には「formula_20 における証明」の形式化の仕方に依存するが、以下の議論は、適当な修正のもとで、どんなリーズナブルな形式化にも通用する。）一般に formula_21 とだけ書かれた（ベースとなる論理における）推論の複雑さを formula_69 と定義する。すると formula_70 が成り立つ。いま formula_71 を「formula_72 以下の複雑さの推論の末尾（帰結）に現れる論理式 formula_21 に対する formula_69 の総和」と定める。すると formula_75 となる。
証明の複雑さの尺度として、証明に現れる論理式の個数や、推論規則の適用回数を採用した場合にも、やはり反例が存在する。formula_12 を任意の帰納的可算理論とすると、formula_12 と同値な原始帰納的理論 formula_78 がクレイグのトリックによって得られる。すなわち、formula_79 を formula_12 の定理の計算可能な枚挙とするとき、
である。ただし formula_82 は formula_8 の formula_1 個のコピーを論理積で結合したものとする。formula_78 で証明可能な文はどれも（適切な論理体系に於いては）全く同じ形の証明を持つ。（例えば自然演繹においては formula_86-除去規則を一度だけ使用する形の証明を持つ。）したがって、証明に現れる論理式の個数や、推論規則の適用回数は、ともにある定数で抑えられる。