ゲーデルの定理-4.3- 対角化定理(その証明)

前回からの続き

　ではゲーデルの対角化定理の証明に入ります。以下の証明は簡単と言えば簡単ですっきりしていますが、論理式、そのゲーデル数、その自然数を記述する記号や式、その記号や式のゲーデル数、とまあ色々複雑な関係が出てきますから、そこの絡みをキチンと見分けないと混乱します。

【再掲】ゲーデルの対角化定理(前原の定理8.3,Ref-3-p130)
　任意の１変数論理式Ｒ(ｘ)について、次の式を満たす確定文Ａが存在する。
　式4.1-1 Ａ⇔Ｒ(ａ)　ただしａ＝~Ａ~

　まず、１変数述語式Ａ(ｘ)と、その変数記号ｘに対象項ｔを代入した確定文Ａ(ｔ)を考えます。そして、前３者のゲーデル数ａ,ｂ,ｃから確定文Ａ(ｔ)のゲーデル数ｋを返す関数Ｓｂ(ａ,ｂ,ｃ)を考えます。これはｘをａで置換(Substitute)したときのゲーデル数を返す関数といった意味を持つので"Substitute"の頭文字から記号を付けています。

関数定義4.3-1a 　Ｓｂ(ａ,ｂ,ｃ)の値ｋは、
　　ａ＝~Ａ(ｘ)~、ｂ＝~ｘ~、ｃ＝~ｔ~　のとき、ｋ＝~Ａ(ｔ)~
　　それ以外のとき　　ｋ＝０

　この関数は論理式で表現されますが、証明は複雑なので後回しにします。また変数記号ｘは形式的体系で用意されているどの変数記号でも構いませんが、以下の議論の間は固定しておけますし、その間はｂ＝~ｘ~も固定できますから、ｂは以後省略した表記を使います。つまり２変数関数として考えます。

関数定義4.3-1b 　Ｓｂ(ａ,ｃ)の値ｋは、
　　ａ＝~Ａ(ｘ)~、ｃ＝~ｔ~　のとき、ｋ＝~Ａ(ｔ)~
　　それ以外のとき　　ｋ＝０

　このＳｂ関数は表現可能で、次の命題が成り立ちます。

命題4.3-1a ａ＝~Ａ(ｘ)~、ｃ＝~ｔ~　のとき、Ｓｂ(ａ,ｃ)＝ｋなるｋが存在し、有限の手順でｋを得ることができる。
命題4.3-1b このとき、Ｓｂ(ａ,ｃ)＝ｋはペアノ公理系で証明できる

　命題4.3-1aはＳｂ関数の定義から明らかで、単に~Ａ(ｔ)~を求めるだけの手続きです。まるで言うまでもないことに見えますが、きちんと明示しておくと後に何かと便利なのです。命題4.3-1bは前述の通り、証明は少し複雑です。

　さてｔには対象式、つまりなんらかの自然数を記述する式(定数記号か関数式)が当てはめられますが、ここでｔを、自然数ｎを記述する定数記号ｎに限定します^*1。そしてｃ＝~ｎ~を次のような関数Ｚ(ｎ)に置き換えます。

関数定義4.3-2　Ｚ(ｎ)の値ｃは、　ｃ＝~ｎ~

　すると任意の１変数述語式Ａ(ｘ)と任意の自然数ｎについて次の命題が成り立ちます。

命題4.3-2a ａ＝~Ａ(ｘ)~　のとき、Ｓｂ(ａ,Ｚ(ｎ))＝ｋなるｋが存在し、有限の手順でｋを得ることができる。ｋ＝~Ａ(ｎ)~ 。
命題4.3-2b このとき、　|--- Ｓｂ(ａ,Ｚ(ｎ))＝ｋ

　ここでｎ＝ａ＝~Ａ(ｘ)~とおけば、任意の自然数１変数述語式Ａ(ｘ)について次の命題が成り立ちます。後述のように、このｎ＝ａとおく手法が対角化と呼ばれる所以です。

命題4.3-3a ａ＝~Ａ(ｘ)~　のとき、Ｓｂ(ａ,Ｚ(ａ))＝ｋなるｋが存在し、有限の手順でｋを得ることができる。ｋ＝~Ａ(ａ)~ 。
命題4.3-3b このとき、　|--- Ｓｂ(ａ,Ｚ(ａ))＝ｋ　

　ここまで準備したところで任意の１項関係Ｒ(ｘ)を考えます。任意の１項関係Ｒ(ｘ)について、おなじ数を代入した命題は同値なので次の命題が成り立ちます。ここでＡ(ａ)も任意です。

命題4.3-4a Ｒ(Ｓｂ(ａ,Ｚ(ａ)))⇔Ｒ(ｋ) が成り立つ
　　　ａ＝~Ａ(ｘ)~　、Ｚ(ａ)＝~ａ~　、ｋ＝~Ａ(ａ)~
命題4.3-4b |--- Ｒ(Ｓｂ(ａ,Ｚ(ａ)))⇔Ｒ(ｋ)

　ここでＡ(ｘ)をＲ(Ｓｂ(ｘ,Ｚ(ｘ)))とおくと、Ａ(ｘ)のゲーデル数ｇとＡ(ｇ)のゲーデル数ｋとの間に次の関係が成り立ち、この関係が論理式で表現されます。

命題4.3-4 Ｓｂ(ｇ,Ｚ(ｇ))＝ｋ が成立し、　|--- Ｓｂ(ｇ,Ｚ(ｇ))＝ｋ　
命題4.3-5 Ｒ(Ｓｂ(ｇ,Ｚ(ｇ)))⇔Ｒ(ｋ) が成立し、　|--- Ｒ(Ｓｂ(ｇ,Ｚ(ｇ)))⇔Ｒ(ｋ)　
　　ｇ＝~Ｒ(Ｓｂ(ｘ,Ｚ(ｘ)))~　、Ｚ(ｇ)＝~ｇ~　、ｋ＝~Ｒ(Ｓｂ(ｇ,Ｚ(ｇ)))~

　確定文Ａ(ｇ)をＡとすれば命題4.3-5の式Ｒ(Ｓｂ(ｇ,Ｚ(ｇ)))⇔Ｒ(ｋ)はすなわちＡ(ｇ)⇔Ｒ(~Ａ(ｇ)~)であり、式4.1-1になります。すなわち、任意の１変数論理式Ｒ(ｘ)についてゲーデルの対角化定理を満たす確定文Ａとは、上記のＲ(Ｓｂ(ｇ,Ｚ(ｇ)))のことだったのです。

　ここで対角化と呼ばれる所以を図で示します。


　この図の上の行列は、縦には全ての１変数論理式Ａ[a_i](ｘ)を順番に並べ、横にはそのゲーデル数ａ_iを並べたものです。例えばゲーデル数の小さい順に並べれば、これは可能です。そして行列の中には、各行の論理式Ａ[a_i](ｘ)に、各列の自然数ａ_jを代入した確定文Ａ[a_i](ａ_j)が位置します。ここで各座標の確定文Ａ[a_i](ａ_j)のゲーデル数をｋijとすれば、
　ｋij＝Ｓｂ(ａ,ｃ)、ａ＝~Ａ[a_i](ｘ)~、ｃ＝~ａ_j~

　そして、この行列の対角成分は確定文Ａ(~Ａ(ｘ)~)、すなわち１変数論理式Ａ(ｘ)に自身のゲーデル数を代入した確定文になっています。

　下の行列には、上の行列の各座標の任意の確定文Ａ[a_i](ａ_j)のゲーデル数ｋijを任意の１変数論理式Ｒ(ｘ)に代入した確定文Ｒ(ｋij)が並んでいます。そして下の行列の対角成分は各列の自然数ａ_jと１対１対応しているので、ゲーデル数ａ_jを変数とした１変数関数Ａg(ｘ)の値になります。そしてＡg(ｘ)が１変数論理式Ａg(ｘ)で記述できたならば、そのＡg(ｘ)は縦に並んだ全ての１変数論理式Ａ[a_i](ｘ)のどこかに存在しているはずです。するとＡg(ｘ)にそのゲーデル数ｇを代入した確定文Ａg(g)が、自身もその否定も証明できない論理式となります。

　実数濃度が自然数濃度より大きいことを証明するカントールの対角線論法では、対角線上の要素から作り出した数がどの列にも存在しないことを示したのですが、ゲーデルの対角化定理では、対角線上の要素から作り出した論理式もどこかの列に存在することを利用している、というわけです。

　ここで下の行列の対角線を表す関数Ａg(ｘ)を表現する論理式Ａg(ｘ)が存在することを証明しなくてはなりません。すなわち、これまで積み残してきた、Ｓｂ(ａ,ｂ,ｃ)、Ｚ(ｎ)、Ｂ(ｙ,ｘ)を表現する論理式の存在証明が必要です。これは長い証明を経ずに的確に説明する自信がありませんので、興味のある方は参考文献などを御参照ください。要領としては基本的な関数の表現可能性からコツコツと積み上げる感じです。

　ひとまずこれにて、第１不完全性定理の証明の話を終わります。

－－－－－－－
*1) 実際には１個の定数記号でなくてもよく、ゲーデルの定理-2.3- 自然数の公理系で示したように、ｓ(ｓ・・・(ｓ(０)・・・))や０''・・・''のような後者関数を使った記号列でもよい。要は自然数と１対１対応している記号や記号列であれば関数Ｚ(ｎ)が定義できるのである。