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

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

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

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

2017-05-11

北田発見への道 9章

論理学

9章証明の数値的表現

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

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

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

2017-05-11

北田発見への道 8章

論理学

8章証明の再帰性

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

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

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

2017-05-10

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

2017-05-09

北田発見への道 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において証明可能でない。

議論はまぁ明快。対角化定理の証明が乗っていない。ロッサー文は、拡張されたゲーデルの不完全性定理といわれているらしいが、どこをどう拡張したのかは書かれていないのが不満。個人的には、関係の数値的に表現可能なことは自明で、任意の関係について成立しそうに思うのだが、なにか勘違いしていそうな予感。

ゆるゆるべんきょう

暇だから哲学・数学・物理学をゆるく勉強しているよ

参考書

哲学史

古典論理

集合論

暗号通貨

論理学ちゃんと勉強

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

10章ゲーデル述語

北田発見への道 9章

9章証明の数値的表現

北田発見への道 8章

8章証明の再帰性

Wikipedia - ゲーデルの不完全性定理

北田発見への道 7章

7章ゲーデルナンバリング

暗号通貨

10章 ゲーデル述語

9章 証明の数値的表現

8章 証明の再帰性

7章 ゲーデルナンバリング

10章ゲーデル述語

9章証明の数値的表現

8章証明の再帰性

7章ゲーデルナンバリング