ゲーデルの加速定理のソースを表示

'''ゲーデルの加速定理'''（ゲーデルのかそくていり、{{lang-en-short|Gödel's speedup theorem}}）は、[[クルト・ゲーデル]]<ref>{{Citation | last1=Gödel | first1=Kurt | title=Über die Länge von Beweisen | url=https://books.google.co.jp/books?id=5ya4A0w62skC&pg=PA396&redir_esc=y&hl=ja | language=German | id=Reprinted with English translation in volume 1 of his collected works. | year=1936 | journal=Ergebinisse eines mathematischen Kolloquiums | volume=7 | pages=23–24}}</ref>により証明された、数理論理学における定理である。この定理によれば、弱い形式的体系では非常に長い形式的証明しか存在しないが、より強い形式的体系では極めて短い形式的証明が存在する、というような[[論理式 (数学)|文]]が存在する。より正確にいえば、それはn階算術の体系で証明可能な命題であって、n+1階算術ではより短い証明を持つものが存在するというものである。

==定理の主張==
{{節スタブ}}

==現実的には証明できない命題==
具体的な例を見るために、最短の形式的証明がとてつもなく長大となる文を構成しよう。形式化された対角線論法によって
:&phi;「この文は高々[[グーゴルプレックス]]個の記号からなる（[[ペアノ算術]]からの）形式的証明を持たない」
なる内容的意味を持つ文を構成する。（ここで「グーゴルプレックス個の記号からなる」という部分を取り除くと[[不完全性定理]]の決定不能な文が得られる。）コーディングを工夫すれば &phi; が&Sigma;<sub>1</sub>論理式となるようにできる。&phi; はペアノ算術から証明可能である：もし証明不能なら「高々[[グーゴルプレックス]]個の記号からなる（[[ペアノ算術]]からの）形式的証明を持たない」が標準模型で真なので、&Sigma;<sub>1</sub>完全性より &phi; は証明可能である。これは不合理。したがって &phi; は証明可能である。すると&Sigma;<sub>1</sub>健全性より &phi; は標準模型で真である。つまり「&phi; は高々[[グーゴルプレックス]]個の記号からなる（[[ペアノ算術]]からの）形式的証明を持たない」から、&phi; の形式的証明はグーゴルプレックス個よりも多くの記号から構成される。<ref group="注釈">もっとも、この場合は文そのものにとてつもなく長大な数字（グーゴルプレックス）が埋め込まれているかもしれず、それが原因で証明が長くなってしまっている可能性を排除できない。この可能性を排除する為には、次のようにすればよい。論理式 <math>\pi(x, y)</math> を「<math>x</math> （をコードとして持つ論理式）は高々 <math>y</math> 個の記号からなる形式的証明を持たない」という論理式とする。この論理式は <math>\Delta_1(PA)</math> で書ける。グーゴルプレックスを（ペアノ算術において）定義する短い <math>\Delta_1(PA)</math>-論理式 <math>\psi(x)</math> を見出す。すると <math>PA \vdash \forall y(\psi(y) \to \pi(x, y)) \equiv \exists y(\psi(y) \land \pi(x, y))</math> であるから、この同値な <math>\Delta_1(PA)</math>-論理式を <math>\pi(x)</math> とおく。形式化された対角線論法によって <math>PA \vdash \varphi \equiv \pi(\lceil \varphi \rceil) </math> を満たす <math>\varphi</math> が得られる。この <math>\varphi</math> は前述の文と同じ内容を持つが、その長さはグーゴルプレックスより遥かに短い。</ref>

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

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

[[ハービー・フリードマン]]は上のような性質を満たすような明示的で自然な例をいくつか見つけた。それはペアノ算術やほかの形式的体系における文であり、その最短の証明は非常に長い。<ref>{{citation|mr=0685558|last=Smoryński|first= C.
|title=The varieties of arboreal experience
|journal=Math. Intelligencer |volume=4 |year=1982|issue= 4|pages= 182–189|doi=10.1007/bf03023553}}</ref>例えば、以下の主張
:「ある自然数 <math>n</math> が存在して、もし根付き木<!-- 訳注：木を順序集合の特別な場合（或いは有限列からなる集合であって、「部分列である」という順序関係について、適当な性質を満たすもの）として定義した場合、根は自明に存在する。それはその順序集合の最小元（或いは空列）である。一方で、木を無向グラフの特別な場合（連結なグラフであってループを含まないもの）として定義した場合、どの頂点を根と見做すかに任意性がある。テーブルに置いた後者の意味の木の頂点を「摘んで持ち上げる」と前者の意味の木が得られる。摘んだ頂点が根となる。-->からなる列 <math>T_1,\ldots,T_n</math> で <math>T_k</math> が高々 <math>k+10</math> 頂点からなるとき、 ある木はそれより後の木へ同相的に{{仮リンク|埋め込める|en|graph embedding}}」
はペアノ算術において証明可能だが、その最短の証明は少なくとも長さ <math>A(1000)</math> を持つ。ここで <math>A(0)=1</math> かつ <math>A(n+1)=2^{A(n)}</math> である。この主張は[[クラスカルの定理]]の特別な場合であり、[[二階算術]]においてより短い証明を持つ。

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

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

[[帰納的集合|帰納的理論]] <math>T</math> と文 <math>\varphi</math> について <math>T+\neg\varphi</math> は[[決定可能性|決定不可能]]であると仮定する。したがってとくに <math>\varphi</math> は <math>T</math> で証明できない。この条件を満たす例としては、[[ロビンソン算術]]と加法や乗法の[[交換法則]]、[[ペアノ算術]]と[[グッドスタインの定理]]や{{仮リンク|パリス・ハーリントンの定理|en|Paris-Harrington's theorem}}、[[ZF]]と[[選択公理]]や[[決定性公理]]、[[ツェルメロ＝フレンケル集合論|ZFC]]と[[連続体仮説]]や[[巨大基数公理]]などがある。

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

{{仮リンク|エーレンフォイヒト|en|Andrzej Ehrenfeucht}}と{{仮リンク|ミッシェルスキー|en|Jan Mycielski}}<ref>Andrzej Ehrenfeucht and Jan Mycielski (1971), Abbreviating proofs by adding new axioms, Bulletin of the American Mathematical Society 77(3): 366-367.</ref>は計算可能性理論を用いて次の加速定理を証明した：
: 任意の計算可能関数 <math>r</math> に対して、<math>T</math> で証明可能な文 <math>\psi</math> が存在して <math>r(\Vert\psi\Vert_{T+\varphi}) \leq \Vert\psi\Vert_T</math> が成り立つ。

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

=== 証明 ===
いま <math>T+\varphi</math> で証明できて <math>T</math> で証明できない文（つまり「新しい定理」）の全体を <math>D</math> とおく。この集合の計算論的な複雑さを解析することで定理が証明される。この集合は次のように性質を持つ：
:<math> \varphi \vee \psi \in D \iff T \not\vdash \varphi \vee \psi \iff T+\neg\varphi \not\vdash \psi.</math>
したがって <math>D</math> は[[帰納的可算]]でない。ただし[[極限計算可能関数|d-帰納的可算]]ではある。

いま加速定理の主張が成立しないと仮定してみよう。つまり、<math>T+\varphi</math> で証明可能な任意の文 <math>\psi</math> に対して、
: <math>T \vdash \psi</math> ならば <math> r(\Vert\psi\Vert_{T+\varphi}) > \Vert\psi\Vert_{T}</math>
が成り立つ。よって、<math>T+\varphi</math> で証明可能な定理 <math>\psi</math> が「新しい定理」であるか否かは、<math>T</math> から複雑さ <math>r(\Vert\psi\Vert_{T+\varphi})</math> 以下で証明可能であるか否かを見ればよい。すなわち、前記の集合 <math> D</math> は次を満たす：
: <math>\psi \in D \iff</math>  <math>T+\varphi \vdash \psi</math> かつ、複雑さ <math>r(\Vert\psi\Vert_{T+\varphi})</math> 未満の <math>\Pi</math> はどれも <math>T \vdash \psi</math> の証明ではない。 
ここで静的複雑性の条件より、<math>\Pi</math> に関する[[全称量化]]は{{仮リンク|有界量化|en|Bounded quantifier}}と見做せる。ゆえに <math>D</math> は帰納的可算である。これは上で示したことに反する。

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

===限界===
この定理は同じ言語で書かれたふたつの理論の間の加速可能性しか教えてくれない。理論 <math>T</math> が言語 <math>L</math> で書かれ、理論 <math>T' \supsetneq T</math> が言語 <math>L' \supsetneq L</math> で書かれている場合、この定理は加速可能な <math>L'</math>-文の存在は教えてくれるが、加速可能な <math>L</math>-文の存在は教えてくれない。例えば、二階算術の部分体系[[逆数学|ACA<sub>0</sub>]]とその[[超準解析|超準的]]な拡大理論との間には、多項式増大度を越える加速定理が成立しないことが知られている。<ref>Keita Yokoyama (2010), Formalizing non-standard arguments in second-order arithmetic, Journal of Symbolic Logic 75(4): 1199-1210.</ref>すなわち言語の拡大を伴う場合には反例が存在する。

また <math>T</math> が帰納的でない場合にも反例が存在する。例えば <math>T,\varphi</math> を定理の条件を満たすペアとする。<math>T</math> で証明可能な文全体（演繹閉包） <math>T'</math> と <math>\varphi</math> は帰納性の条件を除いて定理の条件を満たす。<math>T'</math> で証明可能な任意の文 <math>\psi</math> は
: <math>\psi</math>
とだけ書かれた証明を持つ。（厳密には「<math>T'</math> における証明」の形式化の仕方に依存するが、以下の議論は、適当な修正のもとで、どんなリーズナブルな形式化にも通用する。）一般に <math>\psi</math> とだけ書かれた（ベースとなる論理における）推論の複雑さを <math>f(\psi)</math> と定義する。すると <math>\Vert \psi \Vert_{T'} \leq f(\psi)</math> が成り立つ。いま <math>g(x)</math> を「<math>x</math> 以下の複雑さの推論の末尾（帰結）に現れる論理式 <math>\psi</math> に対する <math>f(\psi)</math> の総和」と定める。すると <math>g(\Vert \psi\Vert_{T'+\varphi}) \geq f(\psi) \geq \Vert \psi \Vert_{T'}</math> となる。

証明の複雑さの尺度として、証明に現れる論理式の個数や、推論規則の適用回数を採用した場合にも、やはり反例が存在する。<ref>菊地誠（2014）『不完全性定理』共立出版</ref><math>T</math> を任意の帰納的可算理論とすると、<math>T</math> と同値な[[原始帰納的]]理論 <math>\mathrm{Craig}(T)</math> が[[クレイグのトリック]]によって得られる。すなわち、<math>\varphi_0,\varphi_1,\ldots</math> を <math>T</math> の定理の計算可能な枚挙とするとき、
: <math>\mathrm{Craig}(T) := \{ \varphi_{n}^{n+1} \mid n \in \mathbb{N} \}</math>
である。ただし <math>\varphi^{n}</math> は <math>\varphi</math> の <math>n</math> 個のコピーを論理積で結合したものとする。<math>\mathrm{Craig}(T)</math> で証明可能な文はどれも（適切な論理体系に於いては）全く同じ形の証明を持つ。（例えば[[自然演繹]]においては <math>\wedge</math>-除去規則を一度だけ使用する形の証明を持つ。）したがって、証明に現れる論理式の個数や、推論規則の適用回数は、ともにある定数で抑えられる。

==注釈==
{{Reflist|group="注釈"}}

==出典==
{{reflist}}

==関連項目==
* [[ブラムの加速定理]]
* [[加速定理]]

==参考文献==
*{{Citation | last1=Buss | first1=Samuel R. | title=On Gödel's theorems on lengths of proofs. I. Number of lines and speedup for arithmetics | url=https://doi.org/10.2307/2275906 | doi=10.2307/2275906 | id={{MR|1295967}} | year=1994 | journal=The Journal of Symbolic Logic | issn=0022-4812 | volume=59 | issue=3 | pages=737–756}}
*{{Citation | last1=Buss | first1=Samuel R. | editor-last=Clote | editor1-first=Peter | editor2-last=Remmel | editor2-first=Jeffrey | title=Feasible mathematics, II (Ithaca, NY, 1992) | publisher=Birkhäuser Boston | location=Boston, MA | series=Progr. Comput. Sci. Appl. Logic | isbn=978-0-8176-3675-3 | id={{MR|1322274}} | year=1995 | volume=13 | chapter=On Gödel's theorems on lengths of proofs. II. Lower bounds for recognizing k symbol provability | pages=57–90}}
*{{citation| last=Parikh | first=Rohit | title=Existence and Feasibility in Arithmetic | url=http://www.jstor.org/discover/10.2307/2269958?uid=3738328&uid=2133&uid=2&uid=70&uid=4&sid=21104096791051 | year=1971 | journal=Journal of Symbolic Logic | volume=36 | pages=494-508}}

{{デフォルトソート:けえてるのかそくていり}}
[[Category:クルト・ゲーデル]]
[[Category:証明論]]
[[Category:数学基礎論の定理]]
[[Category:数学に関する記事]]