北田 発見への道 10章 （終）

10章 ゲーデル述語

前章からの続き。ロッサー文およびゲーデル文に出てくる述語を数値的に表現する。その際、自身のゲーデル数を自身に代入するという事情のため、ゲーデルナンバリング自体が数論的操作であることを示す必要があり、じっさいにそれを示す。

以上により、ゲーデル述語を実際に構成してみることにより、ロッサー文、およびゲーデル文で存在が予測されていた述語を帰納的に構成することができ、不完全性定理の証明が完成したことになる。

ゲーデルの不完全性定理が完全に統語論的に導かれたとするならば、ヒルベルトプログラムを挫折させたといえるだろうが、その証明にはその意味論的操作が必要であったことは指摘したとおりである。意味論的な操作により、自己言及的な命題が記述可能になり、自己言及的な命題は様々な矛盾や困難を生み出すことになる。また、メタレベルにおいて対象の形式と同じ道具立てを利用しているというのも注目するべき点である。

最近ではメタな議論に選択公理や集合論の公理を仮定することも珍しくなくなっている。

この章で大体ゲーデルの不完全性定理の証明が終わったかな。結局対角化定理を使わないでロッサー型のゲーデル文を証明することで不完全性定理を証明したと。

残りの2章は哲学的なのでさらっと流すことにして、ブログでは、言及しないことにする。短い中でもなかなか示唆に富んだ良い本だったように思う。

北田 発見への道 9章

9章 証明の数値的表現

これまでの議論において、「xは公理である⇔Axiom(x)」や「xは証明列である⇔Proof(x)」といった、ゲーデル数を引数にとる述語を、自然数論の体系 N において再帰的に構成できると述べてきた。それを示している。

なお、「xは証明可能である⇔Pr(x)」、「xは反証可能である⇔Re(x)」もNにおいて表現できるが、それは再帰的ではない。

コンピュータ言語みたいっすなー。一つ一つはきちんと見ていないが実際にできるだろうということは納得がいく。

北田 発見への道 8章

8章 証明の再帰性

本書では、ロッサー文を使った証明でゲーデルの不完全性定理を導いた。その際に前提となっている再帰性/帰納性を議論する。

まず、再帰的関数の定義を行い、これを用いると、再帰的述語および再帰的関係を定義することができる。実際、「普通の」関係ないし述語が再帰的であることが示される。

これまで「有限の立場で」という但し書きで使われるような場面では再帰的であることと同等である、ということかな。

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の場合にどのようになるかは次章で説明する。

上記了解。少し複雑になっただけで、特に引っかかる部分はないかな。野矢先生は述語論理の場合は恒真式ではなく、妥当式と言っていた気がするが・・・まぁいいか。