ゲーデルの加速定理
ゲーデルの加速定理（ゲーデルのかそくていり、英: Gödel's speedup theorem）はテンプレート:Harvsで証明された。この定理によれば、弱い形式的体系では非常に長い形式的証明しか存在しないが、より強い形式的体系では極めて短い形式的証明が存在する、というような文が存在する。
クルト・ゲーデルはそのような性質を持つ文を具体的に構成した。それはn階算術の体系で証明可能な命題であってn+1階算術ではより短い証明を持つものが存在するというものである。類似の例として最短の形式的証明がとてつもなく長大となる文を構成しよう。形式化された対角線論法によって
なる内容的意味を持つ文を構成する。（ここで「グーゴルプレックス個の記号からなる」という部分を取り除くと不完全性定理の決定不能な文が得られる。）コーディングを工夫すれば φ がΣ1論理式となるようにできる。φ はペアノ算術から証明可能である：もし証明不能なら「高々グーゴルプレックス個の記号からなる（ペアノ算術からの）形式的証明を持たない」が標準模型で真なので、Σ1完全性より φ は証明可能である。これは不合理。したがって φ は証明可能である。するとΣ1健全性より φ は標準模型で真である。つまり「φ は高々グーゴルプレックス個の記号からなる（ペアノ算術からの）形式的証明を持たない」から、φ の形式的証明はグーゴルプレックス個よりも多くの記号から構成される。[1]
φはより強い体系ではもっと短い形式的証明を持つ：例えばペアノ算術に自身の無矛盾性を表す公理 Con(PA) を追加した体系を用いればよい。（追加された公理は不完全性定理よりペアノ算術からは証明不能である。）すると上の背理法による議論を体系内で実行することでより短い形式的証明が得られる： ¬φ と仮定する。ここから ProvablePA(φ) を得る。他方で ¬φ に形式化されたΣ1完全性を適用すれば ProvablePA(¬φ) を得る。ここに形式化されたモーダス・ポネンスを適用すれば ProvablePA(⊥) すなわち ¬Con(PA) を得る。公理 Con(PA) とモーダス・ポネンスによって矛盾 ⊥ を得る。背理法によって（仮定なしで） φ を得る。
以上の議論のペアノ算術は別のより強い無矛盾な体系に置き換えられる。またグーゴルプレックスもその体系で記述できる別の任意の数字に置き換えられる。
ハービー・フリードマンは上の性質を満たすような明示的で自然な例をいくつか見つけた。それはペアノ算術やほかの形式的体系における文であり、その最短の証明は非常に長い{{#invoke:Footnotes | harvard_citation }}。
Contents
エーレンフォイヒト・ミッシェルスキーの加速定理
帰納的理論 [math]T[/math] と文 [math]\varphi[/math] について [math]T+\neg\varphi[/math] は決定不可能であると仮定する。したがってとくに [math]\varphi[/math] は [math]T[/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[/math] における証明と [math]T+\varphi[/math] における証明の複雑性を比較したい。ただし証明の複雑性を測る関数 [math]|\cdot|[/math] はstatic complexity measureの条件を満たすものとする。理論 [math]S[/math] における文 [math]\psi[/math] の証明の複雑さの最小値を [math]\Vert\psi\Vert_S[/math] と書くことにする。エーレンフォイヒトとミッシェルスキーは次の加速定理を証明した：任意の計算可能関数 [math]r[/math] に対して、[math]T[/math] で証明可能な文 [math]\psi[/math] が存在して [math]r(\Vert\psi\Vert_{T+\varphi}) \leq \Vert\psi\Vert_T[/math] が成り立つ。
いまこれが成立しないと仮定してみよう。すると、[math]T+\varphi[/math] で証明可能な任意の文 [math]\psi[/math] に対して、
- [math]T \vdash \psi \implies r(\Vert\psi\Vert_{T+\varphi}) \geq \Vert\psi\Vert_{T}[/math]
が成り立つ。したがって
- [math]D = \{ \psi \mid T+\varphi \vdash \psi \text{ and } \forall \Pi (|\Pi| \lt r(\Vert\psi\Vert_{T+\varphi}) \to \Pi\mbox{ is not a proof of }T\vdash\psi) ) \}[/math]
となるから、[math]D[/math] は帰納的可算である。これは上で示したことに反する。
脚注
- ↑ もっとも、この場合は文そのものにとてつもなく長大な数字（グーゴルプレックス）が埋め込まれているので、それが原因で証明が長くなってしまっている可能性を排除できない。
関連項目
参考文献
- 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, テンプレート:MR
- 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, テンプレート:MR
- 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
- Parikh, Rohit (1971), “Existence and Feasibility in Arithmetic”, Journal of Symbolic Logic 36: 494-508