ゲーデルの定理-3.4- 第１不完全性定理の証明(証明を意味する論理式)

前回からの続き

1.「論理式Ａは証明できる」という意味の、命題と論理式
　任意の自然数ａについての次のような１項関係Ｂew(ａ)を考えます。これは、「ａをゲーデル数とする論理式Ａは証明できる」という意味を持ちますが、あくまでも自然数の世界Ｎの中での関係です。Ｂew(ａ)は変数ｘを使えば１項関係Ｂew(ｘ)となります。なお、"Ｂew"という表記はRef3,7からの採用です。
　定義3.3-1a　ａ＝~Ａ~ かつ |--- Ａ ならば、Ｂew(ａ)は真
　定義3.3-1b　さもなくば^*1、Ｂew(ａ)は偽

　そして１項関係Ｂew(ｘ)を記述する論理式をＢew(ｘ)とします。ｘにａを代入すればＢew(ａ)となります。すると命題3.1-2a,bは次の命題に置き換えられます。以下で~Ａ~や~Ｕ~は特定の自然数である~Ａ~や~Ｕ~を記述する定数項です。なお、考察対象である形式的体系で論理式Ｂew(ｘ)がうまく構成できることは別途証明しなければなりません。

　命題3.3-1a　　|--- Ａ が真ならば、　|--- Ｂew(~Ａ~)
　　　前原の本の定理8.1[Ref-4) p126]に当たる。
　命題3.3-1b　　|--- Ｂew(~Ａ~) ならば、　|--- Ａ
　　　前原の本の定理8.2[Ref-4) p129]に当たる。

　また式3.1-1とその対偶の式3.1-2は次のようになります。
　式3.3-1 　　Ｕ⇔￢Ｂew(~Ｕ~)
　式3.3-1a　　Ｕ→￢Ｂew(~Ｕ~)
　式3.3-1b　　￢Ｂew(~Ｕ~)→Ｕ
　式3.3-2 　　￢Ｕ⇔Ｂew(~Ｕ~)
　式3.3-2a　　￢Ｕ→Ｂew(~Ｕ~)
　式3.3-2b　　Ｂew(~Ｕ~)→￢Ｕ

　これで式3.3-1,2を満たす論理式Ｕが存在すれば、前回記事の証明3.1-2が成立します。すると残る問題はＵの存在証明と、Ｂew(ｘ)の具体的な構成、および命題3.3-1aと命題3.3-1bの証明です。

2.「論理式Ａの証明列はＢである」という意味の、命題と論理式
　Ｂew(ｘ)の構成のためにまず、任意の自然数ｂ,ａについての次のような２項関係Ｂ(ｂ,ａ)を考えます。これは、「ｂは、ａをゲーデル数とする論理式Ａの証明列Ｂのゲーデル数である」という意味を持ちます。
　　　定義3.3-2a　ａ＝~Ａ~ かつ ｂ＝~Ｂ~ かつ ＢがＡの証明列ならば、Ｂ(ｂ,ａ)は真
　　　定義3.3-2b　さもなくば^*2、Ｂ(ｂ,ａ)は偽

　なお証明できるか否かは公理に依存します。そこで公理の集合をＫとして、その公理系での関係であることを明確に示すためにＢ_Ｋ(ｂ,ａ)といった表記もできます[Ref-4]。しかし本記事の一連の議論の間はＫは固定されていることが多いので、不要な場合は省略することにします。

　さて２項関係Ｂ(ｙ,ｘ)を記述する論理式Ｂ(ｙ,ｘ)が構成できて、Ｂ(ｙ,ｘ)は論理式Ｂ(ｙ,ｘ)で数値別に表現されること、つまり任意の自然数ｂ,ａをｙ,ｘに代入したとき下記が成り立つことが証明されています。実はこの証明はなかなか手間のかかるところなのですが、機会があれば後ほど書いてみましょう。
　　　命題3.3-2a Ｂ(ｂ,ａ)が成立するならば、　|--- Ｂ(ｂ,ａ)
　　　命題3.3-2b Ｂ(ｂ,ａ)が成立しないならば、|--- ￢Ｂ(ｂ,ａ)

　すると、先ほど考えた論理式Ｂew(ａ)は次のように定義できます。「ａ＝~Ａ~である論理式Ａが証明できる」ということは「Ａの証明列Ｙが存在する」ということであり、「証明列Ｙが存在する」ということは「ｙ＝~Ｙ~が存在する」ということだからです。
　定義3.3-3 Ｂew(ａ)≡∃ｙＢ(ｙ,ａ)

　さてこの定義のＢew(ａ)について命題3.3-1aは成立するでしょうか？

証明3.3-1
　1) |--- Ａ が真と仮定する。つまり、論理式の世界でＡが証明できるとする。
　2) それは具体的な証明列Ｂが存在することである。
　3) するとｂ＝~Ｂ~が存在しＢ(ｂ,ａ)が成立する。(ａ＝~Ａ~)
　4) 命題3.3-2aより、|--- Ｂ(ｂ,ａ)である。
　5) ゆえに古典述語論理体系の∃に関する推論規則^*3より |--- ∃ｙＢ(ｙ,ａ)である。

　さらに次の命題も成立すればＢew(ａ)はＢew(ａ)により表現されていることになりますが、これは成立しません。
　　　命題3.3-1c Ｂew(ａ)が偽(つまり |-x- Ａ) ならば、|--- ￢Ｂew(ａ)

　すなわちＢew(ａ)が偽の場合には、「|-x- ￢Ｂew(ａ)かつ|-x- Ｂew(ａ)」という場合もありうるからです。命題3.3-1cは成り立たないが命題3.3-1aだけ成り立つことを、前原は「(論理式Ｂew(ａ)は関係Ｂew(ａ)を)表明している」と書いていました。「表現している」ではなくて。

　次に命題3.3-1bは成立するでしょうか？ 「ゲーデルの定理-3.1-」の記事の証明3.1-1で示したように、命題3.3-1cが成立すれば命題3.3-1bも成立しますが、そうではないので、命題3.3-1bだけを別に証明しなくてはなりません。実はそのためには、10/09の記事で紹介したω無矛盾(ω-consistent)という性質が必要になります。

　まずＢew(ａ)すなわち∃ｙＢ(ｙ,ａ)は￢∀ｙ(￢Ｂ(ｙ,ａ))と同値です。

証明3.3-2
　1) |-x- Ａ と仮定する。
　1-1) 任意のｂにつきＢ(ｂ,ａ)は成立しない。
　1-2) |--- ￢Ｂ(ｂ,ａ)　　∵命題3.3-2b
　1-3) |--- ∀ｙ(￢Ｂ(ｙ,ａ))　∵ω無矛盾ならば
　1-4) |--- ￢∃ｙ(Ｂ(ｙ,ａ))　∵同値に書き換え
　1-5) |-x- ∃ｙ(Ｂ(ｙ,ａ))　∵無矛盾ならば
　2) |-x- Ａ ならば、|-x- ∃ｙ(Ｂ(ｙ,ａ))
　3) |--- ∃ｙ(Ｂ(ｙ,ａ)) ならば、|--- Ａ　∵2)の対偶

　次は式3.3-1を満たす論理式Ｕの存在証明ですが、これにはゲーデルの対角化定理(diagonalization theorem)というものが使われます。

　続く

－－－－－－－－－－－－－
*1) 蛇足だが、大部分の自然数ａにおいて、ａはゲーデル数ではないのでＢew(ａ)は偽である。ただしこれはゲーデル数を前回のように決めるならばであり、全ての自然数をゲーデル数にするように決めたりすれば、その限りではない。
^*2 大部分の自然数対[ａ,ｂ]について、*1と同様にＢ(ｂ,ａ)は偽である。
*3) 例えば1)～4)の推論や「ゲーデルの定理-3.1-」の記事の証明3.1-1では、メタ数学の推論における三段論法や対偶の同値性を使っているが、形式的体系での推論規則は使っていない。∃に関する推論規則はまだ本記事では紹介していない。