Wikipedia - ゲーデルの不完全性定理
なんか色々誤解をしてそうなのでWikipedia(en) も読むことにしたい。
Gödel's incompleteness theorems - Wikipedia
これからも追記予定
二つの完全性
syntactically complete: Aもしくは￢Aが証明できる
semantically complete: 全ての恒真式が証明可能
・ゲーデルが述語論理に対して示した完全性： semantical complete
・述語論理はsemanticalにはcompleteだが、syntacticallyにはcompleteではない
・ゲーデル第一不完全性定理での完全性: syntactical completeness
ゲーデル文とロッサー文
第一不完全性定理の証明は ω無矛盾を前提としたゲーデル版と 無矛盾を前提としたロッサー版がある。どちらも、証明も反証もできない文の存在を証明する。
・ゲーデル文「私は証明できない」
・ロッサー文「もし私が証明可能なら、その否定はより短い証明でなされる」
ロッサー版の方がより一般的な内容であるが、算術を含む体系はω無矛盾であるので、ゲーデル版がそのまま使える。
併せて読む: Rosser's trick - Wikipedia
北田 発見への道 7章
7章 ゲーデルナンバリング
項・式・証明列が与えられた時、それらを一意に自然数にエンコードすることが可能である。このエンコードの規則をゲーデルナンバリングと呼ぶ（その実装には任意性がある）。その自然数を体系内の自然数と同一視し、変数x にその自然数を代入できる。この操作はSのメタの理論のモデルを対象とするモデルに作成することに対応し、意味論的操作である。
ゲーデル述語 R(a,b) として、「aは式Aのゲーデル数であり、bはAの証明のゲーデル数である」を定義すると、可証性述語すなわち、「式Aの証明が存在する」というメタな述語は、「 ∃b R(a,b)」と表現できる。R(a,b) は数値的に表現可能であるので（2個の自由変数をとるある式 r(a,b) で表現できるので）、可証性述語は 「∃b r(a,b) 」とかけ、「Aは証明できない」という述語は、「∀b￢r(a,b)」と書ける。
対角定理に、この h(a) = ∀b ￢r(a,b) を代入すると、「G ⇔ ∀b ￢r(g,b) すなわち、いかなる証明列もGの証明でないというGが存在する」と意味する言明が得られる。同様に、￢G は「ある証明列はGの証明である」に対応するため、「￢G⇔ ∃b r(g,b)すなわち、 ある証明列は G の証明である。」こうして、証明も反証もできないゲーデル式Gが構成できると考えられる。
実際、このような文はロッサー文として、具体的に書き下すことができる。ロッサー文およびその否定は、Sにおいて証明可能でない。
議論はまぁ明快。対角化定理の証明が乗っていない。ロッサー文は、拡張されたゲーデルの不完全性定理といわれているらしいが、どこをどう拡張したのかは書かれていないのが不満。個人的には、関係の数値的に表現可能なことは自明で、任意の関係について成立しそうに思うのだが、なにか勘違いしていそうな予感。
北田 発見への道 6章
6章 述語計算の完全性
話を少し戻して、述語論理における対象の変域が有限個と可算無限個の場合では、無矛盾性の議論に違いがあることを指摘。加算無限個の場合では、直観主義で排除されている手法を利用している。これを認めるような述語論理を集合論的述語論理と本書では記述し、以下議論の対象とする（ツッコミ：メタの議論で有限のステップを無視しているのでヒルベルトプログラムの範疇を超えた議論をしているという認識でいいんだよね？）。
「Kを理論Tの命題式の集合とする。KがTに対して整合的であれば、Kは対象領域を自然数論Nとするモデルを持つ」ことが示され、これにより完全性が（有限の議論を超えた道具立てで）示されたことになり、「述語論理の命題式Aが恒真であることと定理式であることは同値である」、または「述語論理の命題式Aが定理式であることは、Aが自然数論の任意の構造Mをモデルとすることである」ことが言える。
最後に、ヒルベルト的なメタの取り扱い方だけでいえる以下の定理を紹介して終わり。
「述語論理に証明可能でない式を公理に加えると、形式的自然数論は、ω矛盾する」これもある意味、述語論理の完全性を含意しているものと思われる。
感想：北田先生は直感的な意味でという言葉を使っているが、これは直観主義的な立場でという意味ではなくて、厳密でないがわれわれの理性がこのように把握しうる、という意味で使っている。読み間違いはないがあまり使ってほしい言葉ではない。
結局ゲーデルはある種の完全性を含意するような説明を、有限の立場を超えた道具立てで示した、ということでよいのだろう。結局野谷先生も言っていたように、メタな議論にどのような道具立てを用意するかは悩ましいのであるなあ。
北田 発見への道 5章
5章 述語計算の無矛盾性
今度は述語計算。統語論を定め、推論規則を3つ(MP, GEN, SPEC)提示し、命題論理の公理系11こを引き継ぎ、新たに4つの公理を追加する。
真理値の付与は命題論理の場合よりやや複雑になる。すなわち命題の真理値は、述語関数の意味と、述語関数に渡す定項の意味を与える必要がある。例として 「∃b A(a,b) 」の真理値の付与で、変数の変域が {zero,one} の場合を考える。二変数述語は、引数として、(zero,zero), (zero,one), (one,zero), (one,one) の４通りに対して、どのような真理値を与えるかを考え 2^4 = 16 種類の述語が存在することがわかる。「∃b A(a,b)」はAとしてこの16種類のどの述語に対しても、そして、任意のa への付値（すなわち zero もしくは one）に対しても、その真理値が 1 であるかを分析する。実際には充足はするものの、恒真でないことがわかる。
述語論理の無矛盾性は命題論理の時と同様に示される。すなわち、全ての公理＝11の命題計算の公理＋4つの追加された公理が恒真であることを示す。そののち、3つの推論規則MP, GEN, SPEC に対して真理値が保存されることを示す。これにより全ての定理が恒真であることが示されるので、矛盾式が定理でないことがわかり、無矛盾性が確かめられる。
注：上記の無矛盾性の議論は変数の領域が有限の場合にのみ有効であり、例えば領域がNの場合にどのようになるかは次章で説明する。
上記了解。少し複雑になっただけで、特に引っかかる部分はないかな。野矢先生は述語論理の場合は恒真式ではなく、妥当式と言っていた気がするが・・・まぁいいか。
北田 発見への道4章
4章 命題計算の完全性
拡張命題論理と称するモノから完全性に迫る。すなわち命題式の論理式に対して、命題変数の閉包をとる操作を行うと、（自然数論では変数記号に関する閉包をとる限りこのような事情は発生しない）、任意の式は真理値1か0のみをとるようになる。この議論をつぶさに見ると、「真理値1の閉包命題式は拡張命題論理の定理であり、真理値0の閉包命題式の否定は拡張命題論理の定理である」という予測が得られ、ここから「閉包命題式が真理値1をとることと拡張命題論理の定理であることは同値である」、すなわち「命題論理の命題式Aが恒真式であることと、Aが命題論理の定理であることは同値である」ことが予想される。
実際、「命題論理の恒真式は命題論理の定理式である」ことは数学的帰納法を利用することによって確かめられる（メタでは数学的帰納法は有用な道具立てとされる）。また、命題論理において証明可能でない式を公理に加えると体系が矛盾することを示すことができる。
上記をモデルの言葉でいえば、「命題論理の命題式Aが定理式であることは、Aが自然数論Sの任意の構造Mをモデルとすることと同値である」、または「命題論理の命題式Aが定理式であることは、それが恒真式であることと同値である」
以上、命題論理を自然数論の影とする立場からだとこのように拡張された命題論理を持ち出す必要がある（野矢先生の言葉でいえば、自然数論における命題は、変数の閉包をとる限り---すなわち閉じた式-- である限り、自然数論が真偽を決定することに責任を持つべき数論的命題であることに対応する）。証明とか、ヒューリスティックに関しては納得がいくがもう少しやりようはないのだろうか？命題論理をそれ自体として扱うのではなく、自然数論の影として扱うからこのようになるのだろう。まぁ本の主題がゲーデルの定理であるから仕方ないのかもしれないが、命題論理の枠内だけで完全性定理を証明してほしかった。野矢論理学でも完全性の証明ははしょられているわけだし・・・べつのテキストブックを用意する必要がありそうだ。
北田 発見への道 3章
3章 命題計算の無矛盾性
いったん命題理論から始める。しかし本書では一貫して自然数論Sを前提に置いているため、命題変数は自然数論における命題と同一視する。命題論理自身もSの影としてみる立場のようだ。
統語論、推論規則（MP１つ）、公理系(11こ）を提示。意味論として真理値表を導入する。全ての公理がトートロジーであることが示せる。また、唯一の推論規則MP の前件が真と仮定した際に、後件が真になる、すなわち真理性が保存されることが示せる。トートロジーたる公理からはじめ、MPを有限回用いて定理を導いていくので、全ての定理がトートロジーであることが示せる。したがって矛盾式が定理でないことが示されるので、無矛盾性・整合性が確かめられる。
真理値表を与える代わりに、モデルという概念を導入して、「命題論理の定理式がトートロジーである」の現代版「命題論理の定理式は、自然数論における任意の構造Mにおいて真である」ことを示す。
全体の議論は非常に明快。うまく公理系、推論規則を選んだから、かな。あと、命題論理だとモデルの概念が簡単になりすぎて逆にわかりづらい・・
