ゲーデルの定理-4.2B- 対角化定理(「真である」という意味の命題)

共通参考文献はこちら
前回からの続き

　　【再掲】式4.1-1 Ａ⇔Ｒ(ａ)　ただしａ＝~Ａ~

　さてゲーデル文Ａ、すなわち上式を満たすＡを使い、次の性質を持つ論理式Ｔ(ｘ)を考えてみます。

定義4.2-2 すべての確定文(閉論理式)Ａについて、論理式Ａ⇔Ｔ(ａ)が証明できる。

　この論理式Ｔ(ｘ)が記述している命題Ｔ(ｘ)とは、モデルにおいてどんな意味を持つのでしょうか？ まずこのモデルは考えている形式的体系のモデルですから、体系の健全性を仮定すれば、次のような性質を持つモデルが存在します。
　　「この公理系で証明できる論理式が記述する命題は、このモデルで真である。」

　するとＡは確定文であり命題Ａを記述するものなので、論理式Ａが証明できるなら命題Ａは真です。同様に論理式Ｔ(ａ)が証明できるなら命題Ｔ(ａ)は真です。以上を記号で表すと次のようになります。
　1) |--- 論理式Ａ⇔Ｔ(ａ)　　∵Ｔ(ａ)の定義から
　2a) |--- Ａ ならば、命題Ａは真
　2b) |--- Ｔ(ａ) ならば、命題Ｔ(ａ)は真

　さらに次のことが言えます。
　3) |--- Ａ ならば、|--- Ｔ(ａ)　∵1)と三段論法(推論規則のひとつ)
　4) |--- Ａ ならば、命題Ｔ(ａ)は真　　∵3)と2b)からの三段論法

　同様な推論から、
　5) |--- Ｔ(ａ) ならば、命題Ａは真　　

　すなわち命題Ｔ(ａ)とは「命題Ａは真である」という意味を持つと解釈できます。さて実は、このような性質を持つ論理式Ｔ(ｘ)は存在しない、というのが「タルスキの定義不可能性定理」と呼ばれる定理です。

証明　[Ref-3) p139]
　Ｔ(ｘ)が存在すると仮定して、以下の推論から矛盾を導く。
　　1) ある確定文Ｂが存在してｂ＝~Ｂ~とすれば、|--- Ｂ⇔￢Ｔ(ｂ)
　　　　　∵ゲーデルの対角化定理
　　2) Ｔ(ｘ)の定義から、|--- Ｂ⇔Ｔ(ｂ)
　　3) 矛盾である。

　私の言語感覚からすると「定義する」だけなら証明可能性は無関係だと思いたくなるのですが、「タルスキーの定義不可能性定理」の定義の意味には、上記説明の通り「証明可能性」の概念が入っています。実際、論理式Ｔ(ｘ)が「ゲーデル数ｘである論理式は真である」を単に記述するだけなら、真を定義するモデルによっては可能です。例えばゲーデルの定理-2.3-で仮に「ペアノ自然数」と呼んだモデルです。

　　公理系としてペアノ公理系をとる。
　　自然数の集合でペアノ公理系から証明可能な命題のみを真と定義する。
　　真でない命題は偽と定義する。

　するとこの形式的体系での論理式Ｂew(ｘ)「ゲーデル数ｘである論理式は証明できる」は、まさにこのペアノ自然数モデルにおけるＴ(ｘ)になります。すなわち、
　　　Ｔ(ａ)「命題Ａは真である」という命題はＢew(ａ)に対応する。
　　　￢Ｔ(ａ)「命題Ａは偽である」という命題は￢Ｂew(ａ)に対応する。

　しかし後者の場合はＴ(ａ)も￢Ｔ(ａ)も証明できない場合も含みますから、Ｂew(ｘ)は命題Ｔ(ａ)を表現してはいません。

　ところで、そもそも真理式Ｔ(ｘ)を定義する命題4.2-2が証明可能性を使っていますが、替わりに次の命題を使うこともできるはずです。

命題4.2-3 すべての確定文(閉論理式)Ａについて、命題Ａ⇔Ｔ(ａ)が成り立つ。

　この命題を使う場合は、命題Ａ⇔Ｔ(ａ)が成り立つか否かはモデルを特定して、そのモデルについて確認しなければなりません。その代り、公理系をいちいち設定する必要はありません。逆に命題4.2-2を使う場合は、モデルによらず特定の公理系の中だけで話が済みます。ただし「すべての確定文」というのは無限集合ですから、それについて「命題が成り立つ」ことは数学的証明以外の方法では確認できないのが普通です。これでは命題4.2-3は使いずらいですね。

　なお上記の「ペアノ自然数」のモデルは、実は、「ペアノ公理系の確定文」という台集合に「証明できる」という１項関係を加えた構造をモデルにしたものとも言えます。すなわち論理式の世界における、論理式の集合そのものをモデルにしたわけです。するとこのモデルでは「証明できる」と「真である」という命題が一致すると考えてよい、というわけです。

　タルスキの真理定義の詳細は次回とします。