第一不完全性定理を説明してみる


話が複雑すぎて何とか自分で説明してみないと理解できそうになかったので説明を書いた。面倒な話なので読まなくてもいいです。


追記: 夜になってからかなり直した。

短い方の説明は以下。

http://www.at-akada.org/blog/2008/03/200836.html#id_p0

追記2: またちょっと直した。直しすぎでごめん。




スタート地点

話は↓ここからはじまる。

  • こうすれば任意の論理式に自然数が一対一で対応ですよ?
  • つまり、「これは適切な論理式か?」「これは適切な証明か?」という論理学上の問題が、「自然数から自然数への関数をつくる」問題になるよ。

http://www.at-akada.org/blog/2008/01/2008121.html#id_20e69c80e8bf91e381aee3828fe3819fe38197


われわれはついに関数の体系を使って、自然数の体系を形式化したラッセルとホワイトヘッドの体系を自然数の上にコーディングすることに成功した、と仮定する。

* 関数の体系については以下も参照。

http://www.at-akada.org/blog/2008/01/200815.html#id_20e2978fe2889ae296a1


自然数をデコードするとラッセル、ホワイトヘッドの体系上の論理式が得られ、論理式をエンコードすると対応する自然数が得られる。


以下デコードする関数の側をレベル0、関数の体系を使って操作される体系をレベル1と呼ぶ。

何しろ自然数の体系を自然数の上にエンコーディングしたわけだから、レベル0とレベル1が混ざって非常にややこしい。きちんと区別をつけるため、以後レベル1の概念には【数】などと【】をつけて表現する。

以下ではわたしが適当につくった表記法を使ってゲーデルの第一不完全性定理の証明を追っていくことにする。たぶんゲーデルの元の論文よりはわかりやすい。


さて問題は、レベル1体系の完全性、すなわちどんな【式】についても肯定か否定のどちらかが証明できるのかということだ。「肯定も否定も【証明】できない【式】」が存在すれば、不完全性が証明できる

今から「肯定も否定も【証明】できない【式】」を実際につくろう。




decode

まず以下のような関数を考えよう。

  • decode(x)

これは自然数 x をレベル1の【論理式】として解読する操作。

返り値は

"f(x)" みたいな【論理式】を表わす文字列となる。




自己適用的な【式】を考える

では次のようなレベル0の関数の操作を考えよう。

decode(n):(n)

これは「decode(n) に n 自身を【代入】する」と読むことにする。

decode(n) は自然数をデコードし、【論理式】に変換している。【論理式】はこの場合、 "f(x)" のような自由変数を持ったもの、すなわち【代入】が可能なものであるとする。


ここでは、n をデコードしたものに対し n 自身を【代入】している。

たとえば

decode(14)

は、【xは偶数である】という意味の【式】だったとしよう。しかし偶然にも 14自身偶数である。

よってこの場合

decode(14):(14)

は【証明】可能な正しい【式】となる。


こういう

decode(x):(x)

のような操作のことを

「x の自己適用」と呼ぶことにしよう。

x の自己適用は当然ながら【証明】できることもあるし、【否定】が【証明】されることもある。なぜそんなことをするのかはわからないが、別にとりたて不可能そうな操作では無いはずだ。




省略表記

ただし、こんな風にレベル1 の世界の【代入】を行なうとき、いちいち decode(n):(n)と書くのは面倒なので、省略表記を考えよう。

decode(x) は "x(X,Y)" のような【論理式】になる。なるべく decode を使わず二重引用符だけですますことにしよう。また代入される数の側は、decode された【論理式】ではなくただの数であるということをはっきりさせるために [x] と書く。

つまり、decode(x):(x) は

"x([x])"

と書く。




変な関数を考える

さてここで以下のようなレベル0の関数を考えよう。

P(x) = NOT provable( "x([x])" )

P(x) は、

x の自己適用が【証明】できないときにかぎり真を返す。

先の

decode(14):(14)

の場合とは逆に、自分自身をデコードした【論理式】に自分を代入したところ、【証明】できない正しくない【式】しかでてこなかったという場合だ。




変な関数に似た【式】を考える

ところで、P(x) が真を返すということは P(x) が自然数 x の持つ正しい性質だということである。

数の性質はレベル1の世界でも変わらないことが期待されるので、P(x) に対応する【式】p がレベル1の世界にあるはずだ。それを考えよう。

* この辺、だいぶ証明をとばしてますが...。

つまり

P(n) = NOT provable( "n([n])" )

が真ならば、必ず

"p([n])"

も正しくなるような【式】 p を考えよう。


この【式】は正しい【式】なので、レベル1の世界で【証明】できるものでなければならない。

つまり一般に以下のことが成り立つ。

(1)
P(x) = NOT provable( "x([x])" )
が真ならば
provable( "p([x])" )
も真である。

一方P(x) が偽ならば、"p([x])" のレベル1における【否定】が証明できるはずだ。

(2)
NOT P(x) = provable( "x([x])" )
が真ならば
provable( "¬p([x])" )
も真である。



P(p) を考える

つづけて先の(1) で x = p の場合を考えよう。decode される前の p はただの自然数なので x に代入することも可能である。

(3)
P(p)、すなわち
NOT provable ( "p([p])" )
が真ならば 
provable( "p([p])" ) 
も真である。

同様に(2) より、

(4)
NOT P(p)、すなわち
provable ( "p([p])" )
が真ならば
provable ( "¬p([p])" )
も真である

さあ、見た目からして大分あやしい式がでてきた。



おわり

(3), (4) は奇妙な式だ。

まず(4)

"p([p])" が【証明】できるなら

"¬p([p])" が【証明】できる。

と言っている。

しかしこの両方が【証明】できた場合、レベル1の体系は矛盾してしまう。

従って、"p([p])" は【証明】できないと考えるしかない。


では一方、この【式】を【否定】したもの、

すなわち、"¬(p([p])" は証明できるだろうか。


しかし、"p([p])" は【証明】できないのだから(3) の前半が成り立つ。

従って、(3) の後半より

provable( "p([p]" ).

ゆえに "¬p([p])" が【証明】されれば、やはりレベル1の体系は矛盾してしまう。


よって "p([p])" は【証明】できないし、その【否定】も【証明】できない。

整合的な (矛盾しない) 体系において p([p]) は【証明】できるとも【証明】できないとも言えない式だ。

コメント(1)

# Anne Maybus

Seems different from your previous posts. Did YOU write this post, or someone else did? Anyway, I think your readers really enjoyed reading it.

(2008/04/ 9 20:06)

コメントする

トラックバック(0)

このブログ記事を参照しているブログ一覧: 第一不完全性定理を説明してみる

このブログ記事に対するトラックバックURL: http://www.at-akada.org/mt/mt-tb.cgi/891

著者について

赤田敦

nightly[at]at-akada.org

紹介: about

ホーム: at-akada.org

-> 携帯電話用

なかなか更新されないときは...

-> 赤田ブログ生成器

2009年1月

        1 2 3
4 5 6 7 8 9 10
11 12 13 14 15 16 17
18 19 20 21 22 23 24
25 26 27 28 29 30 31