ゲーデルの不完全性定理

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

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

決定不能命題の例

数学と計算機科学（コンピュータ科学）において、「決定不能」という言葉には二つの異なった意味がある。一つ目は証明論の文脈でゲーデルの定理に関連して使われる意味であり、特定の形式的体系の下で或る命題を証明も反証もできないことを言う。二つ目は計算可能性理論に関連した用法であり、命題ではなく決定問題に適用される。決定問題とは入力に対して答が真か偽のいずれかになるような問題である。ある問題を全ての入力に対して正しく解答するようなアルゴリズムが存在しないとき（すなわち特性関数が計算可能関数でないとき）、そうした問題は決定不能であると言う。

不完全性定理は、自然数論が一つ目の意味で決定不能であることを主張している。一方、述語論理の論理式が充足可能か否かを判定する充足可能性問題は決定問題にあたるが、不完全性定理によって、二番目の意味で決定不能である。つまり、述語論理の論理式が充足不能であれば、その論理式から矛盾を導く証明を見つけることができるが、充足可能であるときにその旨、回答を返すアルゴリズムは存在し得ない。

ゲーデルとポール・コーエンの仕事を合わせて、決定不能命題の確かな実例が得られた。連続体仮説はZFC（集合論における標準的な公理系）の下では証明も否定の証明もできない。また、選択公理もZF（ZFCに含まれる公理から選択公理を除いたもの）では証明も否定の証明もできない。これらの結果は不完全性定理を必要としない。1940年、ゲーデルはこれらの命題が何れも ZF または ZFC 集合論では否定を証明できないことを証明した。1960年代、コーエンはこれらがいずれも ZF から証明できず、また連続体仮説が ZFC から証明できないことを証明した。

マチャセビッチによるヒルベルトの第10問題の解決により、決定不能な命題の例が得られる。そのような例はディオファントス方程式の外側に存在量化子を幾つか並べた形として得られる。すなわち不完全性定理の前提条件を満たす形式的体系において、解の存在が証明も反証もできないようなディオファントス方程式が存在する。

1973年、群論におけるホワイトヘッドの問題（英語版）が標準的な集合論では決定不能であることが示された。

1977年、パリスとハーリントンは、ラムゼーの定理の一種であるパリス＝ハーリントンの定理が、一階算術の公理体系であるペアノ算術の下では決定不能だが、より大きな二階算術の体系では証明できることを証明した。カービーとパリスは後にグッドスタインの定理（自然数の数列に関する命題であり、パリス・ハーリントンの原理よりもいくらか易しい）がペアノ算術では決定不能であることを示した。

計算機科学で応用される Kruskal の木定理（英語版）はペアノ算術では決定不能だが集合論では証明できる。実際、Kruskalの木定理（またはその有限版）は、可述主義（英語版）^{[注 9]}と呼ばれる数学的哲学に基づいて構築されたもっと強い体系の下でも決定不能である。これに関連し、更に一般的な graph minors 定理（英語版）（2003年）は計算複雑性理論に影響する。

グレゴリー・チャイティンはアルゴリズム情報理論における決定不能命題を発見し、その状況下で新たな不完全性定理を得た。チャイティンの定理によると、十分な算術を表現可能ないかなる理論においても、どのような数であっても $c$ よりも大きなコルモゴロフ複雑性を有することがその理論上では証明できないような、上限 $c$ が存在する。ゲーデルの定理が嘘つきのパラドックスと関係しているのに対し、チャイティンの結果はベリーのパラドックスに関係している。

脚注

注釈

^ 原文：数学の基礎をめぐる論争の実質的な勝者が形式主義である … ．不完全性定理は数学そのものについての定理ではなく，「形式化された数学」に関する定理であり，形式主義的な数学観についての定理である．^[4]
^ 原文：ゲーデルの不完全性定理は有限の立場（形式主義）で数学の無矛盾性を証明することはできないことを示した．ゲンツェン（Gentzen）は，有限の立場より緩い制限のもとで自然数論の無矛盾性を証明した．^[3]
^
詳細は「ゲーデルの不完全性定理#数学と哲学の分離」を参照
^
詳細は「フランセーン 2011, p. 145.『これらの体系の公理が真であり、そして無矛盾であるという絶対確実な知識をもっていると主張しても、ゲーデルの定理のどこにも相反しないのである』」を参照
^
詳細は「ゲーデルの不完全性定理#誤用例」を参照
^ 歴史的には論理式のゲーデル数化の概念が先に生まれ、後にコンピュータがデータを数値で表すようになった。なお、ゲーデル自身は、素因数分解の一意性を利用して論理式のゲーデル数化を実現している。
^ 実際、 $\lnot ProvableARG(m,m)$ が証明可能なら $\not ProvableARG(m,m)$ の証明系列 $P_{1},\ldots ,P_{n_{0}}$ が存在するので、論理式の列 $P_{1},\ldots ,P_{n_{0}}$ のゲーデル数を $a$ とすると、「Proof $(a,m,m)$ 」が証明可能、したがって特に「 $\exists y:Proof(y,m,m)$ 」=「 $ProvableARG(m,m)$ 」が証明可能。一方我々は「 $\lnot ProvableARG(x,x)$ 」が証明可能な事を仮定していたので、これは矛盾である。
^ ω無矛盾とは $\exists yP(y)$ が証明できれば、 $P(u)$ を満たす自然数 $u$ が実際に存在することを指す。定義より「 $ProvableARG(m,m)$ 」は「 $\exists y:Proof(y,m,m)$ 」であった。ω無矛盾性より、「 $Proof(u,m,m)$ 」を満たす自然数 $u$ が実際に存在し、 $u$ をゲーデル数に持つ論理式の列が $\not ProvableARG(m,m)$ の証明系列になる。
^ 訳注：自己言及的でないこと。
^ 訳注：この場合の「帰納的可算」とは、すべての定理のゲーデル数を枚挙する計算可能関数が存在する（実効的に枚挙可能）ことを意味する。クレイグのトリックによれば、このことは定理集合が帰納的な公理系から生成される（演繹閉包である）ことと同値である。
^
数学基礎論と不完全性定理

…
数学の正しさには一分の隙もなく，数学では矛盾する二つの結論が導かれることは決して無いと昔から信じられている． … そもそも「信じられている」という言葉を使うことは不適切であり，不謹慎でさえあるかも知れない．
この数学の正しさと無矛盾性に対する確信が揺らいだことがかつて一度だけあった． … 19世紀末から20世紀初めにかけて数学の中で次々と逆理が発見された．正しさは数学の絶対的な規範であり，たとえ一ヵ所にでも亀裂が入れば数学の世界全体は粉々に砕けてしまう．^[23] …
この数学の基礎に関する「不安の時代」には … 果たして数学は正しく無矛盾なのか，そもそも定理や証明とは何なのかといった哲学的な問題に対して，伝統的な哲学的手法によってではなく，数学的手法を用いて答えようとする形式主義の試みの中から数学基礎論と呼ばれる数学の一分野が生まれた．^[25]
^
宴のあと

…
数学の危機が真面目に論じられていた「不安の時代〔19世紀末～20世紀初頭〕」は意外に簡単に終わった．現在，数学の基礎を本気で心配している数学者はまずいない． … 「不安の時代」が通り過ぎた後，数学基礎論は哲学と袂を分かち，独自の数学的な問題意識や価値観を見出した．数学基礎論の専門家は「哲学的な動機のもとで数学基礎論を語る時代は終わった」と考えるようになり … 数字基礎論は普通の数学に生まれ変わった．
不完全性定理についても数学基礎論の専門家の間では，哲学的な意義よりも様々な数学的応用可能性のほうが大切であると考えられるようになった．
電子技術の爆発的な発展と共に成長した計算機の基礎理論においても不完全性定理は重要な基本定理の一つであるが，そこでも不完全性定理は定理の主張そのものよりも，定理の証明の中で提案され用いられた様々な考え万や，不完全性定理から導かれる事実のほうが遥かに重要であると考えられているであろう．^[2]
^

数学と哲学
20世紀初頭の数学の基礎に関する「不安の時代」には，数学者と哲学者は共に数学の基礎について論じていた．
それが今では数学者と哲学者は極めて疎遠である．数学者，特に数学基礎論の専門家は哲学者による数学の基礎についての議論を最近の数学を無視した色褪せた100年前の論争の焼き直しに過ぎないと感じ，哲学者は最近の数学としての数学基礎論の進展を重箱の隅をつつくような技術的で瑣末な話題だと考えている．^[26] …
数学基礎論が哲学との繋がりを失ったことを知らない数学者は今でも数学基礎論のことを「哲学のようなもの」と考えている． … この，数学基礎論が「哲学のようなもの」であるという考えは，「哲学のような深い立派なもの」ではなく，「哲学のようなツマラナイコト」という意味であるため，このような考えを「他愛ない無邪気なもの」とは見過ごせない数学基礎論の専門家は，数学基礎論が哲学ではなく数学であることの説得を，何度となく試みてきた．^[27]
^ フランセーンはストックホルム大学で哲学を専攻し、1987年に「Ph.D.（哲学）」を取得^[7]。ルレオ工科大学でのフランセーンのページによると、「（哲学における）自分の博士論文　“my PhD thesis (in philosophy)”」は世界各国の大学図書館で閲覧できる^[28]。

出典

^ 青本 et al. 2005, p. 510.
^ ^a ^b ^c ^d ^e 菊池 2014, p. iii.
^ ^a ^b ^c ^d 青本 et al. 2005, p. 294.
^ ^a ^b 菊池 2014, p. 9.
^ ^a ^b ^c ^d ^e ^f ^g 日本数学会（編） 2011, p. 357.
^ 菊池 2014, pp. ii–iii.
^ ^a ^b ^c ^d フランセーン 2011, p. 奥付け.
^ ^a ^b ^c ^d ^e ^f ^g ^h フランセーン 2011, p. 230.
^ ^a ^b ^c フランセーン 2011, p. 145.
^ フランセーン 2011, p. 4, 7, 126-127.
^ ^a ^b ^c ^d フランセーン 2011, p. 54.
^ 菊池 2014, p. 5.
^ ^a ^b ^c 菊池 2014, p. 248.
^ 照井一成 (2018年). “数理論理学 II (不完全性定理)” (PDF). 2023年4月6日閲覧。
^ 青本 et al. 2005, p. 116.
^ ^a ^b 日本数学会（編） 2011, p. 355.
^ フランセーン 2011, pp. 21–22.
^ ^a ^b フランセーン 2011, p. 22.
^ フランセーン 2011, pp. 22–23.
^ ^a ^b フランセーン 2011, p. 47.
^ フランセーン 2011, pp. 47–48.
^ 菊池 2014, p. 奥付け.
^ ^a ^b 菊池 2014, p. i.
^ 菊池 2014, pp. i–ii.
^ ^a ^b ^c 菊池 2014, p. ii.
^ ^a ^b ^c 菊池 2014, p. 11.
^ ^a ^b 菊池 2014, pp. 11–12.
^ ^a ^b Franzén 2008, p. Torkel Franzén.
^ ^a ^b ^c ^d フランセーン 2011, p. 9.
^ ^a ^b ^c ^d フランセーン 2011, p. 10.
^ ^a ^b ^c ^d ^e ^f フランセーン 2011, p. 4.
^ ^a ^b ^c フランセーン 2011, p. 229.
^ フランセーン 2011, pp. 3–4.
^ フランセーン 2011, pp. 230–231.
^ ^a ^b ^c ^d フランセーン 2011, p. 231.
^ フランセーン 2011, pp. 125–126.
^ ^a ^b ^c ^d ^e ^f フランセーン 2011, p. 126.
^ ソーカル & ブリクモン 2012, p. 262.
^ ^a ^b ^c フランセーン 2011, p. 233.
^ フランセーン 2011, p. 107.
^ ^a ^b フランセーン 2011, p. 108.
^ フランセーン 2011, pp. 108–109.
^ フランセーン 2011, pp. 112–113.
^ ^a ^b ^c ^d フランセーン 2011, p. 120.
^ ^a ^b ^c ^d フランセーン 2011, p. 7.
^ フランセーン 2011, p. 127.
^ フランセーン 2011, p. 128.
^ ^a ^b フランセーン 2011, p. 131.
^ フランセーン 2011, pp. 131–132.
^ ^a ^b フランセーン 2011, p. 132.
^ ^a ^b ^c ^d ^e フランセーン 2011, p. 234.
^ フランセーン 2011, pp. 234–235.

[前の解説]

[続きの解説]

「ゲーデルの不完全性定理」の続きの解説一覧

固有名詞の分類

定理	アペリーの定理四平方定理ゲーデルの不完全性定理中心極限定理リウヴィルの定理 >>固有名詞 >>方式・規則一覧 >>理論・法則一覧 >>定理・公理一覧

>> 「ゲーデルの不完全性定理」を含む用語の索引
ゲーデルの不完全性定理のページへのリンク

ゲーデルの不完全性定理決定不能命題の例