共通参考文献はこちら
前回からの続き
【再掲】式4.1-1 A⇔R(a) ただしa=~A~
さてゲーデル文A、すなわち上式を満たすAを使い、次の性質を持つ論理式T(x)を考えてみます。
定義4.2-2 すべての確定文(閉論理式)Aについて、論理式A⇔T(a)が証明できる。
この論理式T(x)が記述している命題T(x)とは、モデルにおいてどんな意味を持つのでしょうか? まずこのモデルは考えている形式的体系のモデルですから、体系の健全性を仮定すれば、次のような性質を持つモデルが存在します。
「この公理系で証明できる論理式が記述する命題は、このモデルで真である。」
するとAは確定文であり命題Aを記述するものなので、論理式Aが証明できるなら命題Aは真です。同様に論理式T(a)が証明できるなら命題T(a)は真です。以上を記号で表すと次のようになります。
1) |--- 論理式A⇔T(a) ∵T(a)の定義から
2a) |--- A ならば、命題Aは真
2b) |--- T(a) ならば、命題T(a)は真
さらに次のことが言えます。
3) |--- A ならば、|--- T(a) ∵1)と三段論法(推論規則のひとつ)
4) |--- A ならば、命題T(a)は真 ∵3)と2b)からの三段論法
同様な推論から、
5) |--- T(a) ならば、命題Aは真
すなわち命題T(a)とは「命題Aは真である」という意味を持つと解釈できます。さて実は、このような性質を持つ論理式T(x)は存在しない、というのが「タルスキの定義不可能性定理」と呼ばれる定理です。
証明 [Ref-3) p139]
T(x)が存在すると仮定して、以下の推論から矛盾を導く。
1) ある確定文Bが存在してb=~B~とすれば、|--- B⇔¬T(b)
∵ゲーデルの対角化定理
2) T(x)の定義から、|--- B⇔T(b)
3) 矛盾である。
私の言語感覚からすると「定義する」だけなら証明可能性は無関係だと思いたくなるのですが、「タルスキーの定義不可能性定理」の定義の意味には、上記説明の通り「証明可能性」の概念が入っています。実際、論理式T(x)が「ゲーデル数xである論理式は真である」を単に記述するだけなら、真を定義するモデルによっては可能です。例えばゲーデルの定理-2.3-で仮に「ペアノ自然数」と呼んだモデルです。
公理系としてペアノ公理系をとる。
自然数の集合でペアノ公理系から証明可能な命題のみを真と定義する。
真でない命題は偽と定義する。
するとこの形式的体系での論理式Bew(x)「ゲーデル数xである論理式は証明できる」は、まさにこのペアノ自然数モデルにおけるT(x)になります。すなわち、
T(a)「命題Aは真である」という命題はBew(a)に対応する。
¬T(a)「命題Aは偽である」という命題は¬Bew(a)に対応する。
しかし後者の場合はT(a)も¬T(a)も証明できない場合も含みますから、Bew(x)は命題T(a)を表現してはいません。
ところで、そもそも真理式T(x)を定義する命題4.2-2が証明可能性を使っていますが、替わりに次の命題を使うこともできるはずです。
命題4.2-3 すべての確定文(閉論理式)Aについて、命題A⇔T(a)が成り立つ。
この命題を使う場合は、命題A⇔T(a)が成り立つか否かはモデルを特定して、そのモデルについて確認しなければなりません。その代り、公理系をいちいち設定する必要はありません。逆に命題4.2-2を使う場合は、モデルによらず特定の公理系の中だけで話が済みます。ただし「すべての確定文」というのは無限集合ですから、それについて「命題が成り立つ」ことは数学的証明以外の方法では確認できないのが普通です。これでは命題4.2-3は使いずらいですね。
なお上記の「ペアノ自然数」のモデルは、実は、「ペアノ公理系の確定文」という台集合に「証明できる」という1項関係を加えた構造をモデルにしたものとも言えます。すなわち論理式の世界における、論理式の集合そのものをモデルにしたわけです。するとこのモデルでは「証明できる」と「真である」という命題が一致すると考えてよい、というわけです。
タルスキの真理定義の詳細は次回とします。
前回からの続き
【再掲】式4.1-1 A⇔R(a) ただしa=~A~
さてゲーデル文A、すなわち上式を満たすAを使い、次の性質を持つ論理式T(x)を考えてみます。
定義4.2-2 すべての確定文(閉論理式)Aについて、論理式A⇔T(a)が証明できる。
この論理式T(x)が記述している命題T(x)とは、モデルにおいてどんな意味を持つのでしょうか? まずこのモデルは考えている形式的体系のモデルですから、体系の健全性を仮定すれば、次のような性質を持つモデルが存在します。
「この公理系で証明できる論理式が記述する命題は、このモデルで真である。」
するとAは確定文であり命題Aを記述するものなので、論理式Aが証明できるなら命題Aは真です。同様に論理式T(a)が証明できるなら命題T(a)は真です。以上を記号で表すと次のようになります。
1) |--- 論理式A⇔T(a) ∵T(a)の定義から
2a) |--- A ならば、命題Aは真
2b) |--- T(a) ならば、命題T(a)は真
さらに次のことが言えます。
3) |--- A ならば、|--- T(a) ∵1)と三段論法(推論規則のひとつ)
4) |--- A ならば、命題T(a)は真 ∵3)と2b)からの三段論法
同様な推論から、
5) |--- T(a) ならば、命題Aは真
すなわち命題T(a)とは「命題Aは真である」という意味を持つと解釈できます。さて実は、このような性質を持つ論理式T(x)は存在しない、というのが「タルスキの定義不可能性定理」と呼ばれる定理です。
証明 [Ref-3) p139]
T(x)が存在すると仮定して、以下の推論から矛盾を導く。
1) ある確定文Bが存在してb=~B~とすれば、|--- B⇔¬T(b)
∵ゲーデルの対角化定理
2) T(x)の定義から、|--- B⇔T(b)
3) 矛盾である。
私の言語感覚からすると「定義する」だけなら証明可能性は無関係だと思いたくなるのですが、「タルスキーの定義不可能性定理」の定義の意味には、上記説明の通り「証明可能性」の概念が入っています。実際、論理式T(x)が「ゲーデル数xである論理式は真である」を単に記述するだけなら、真を定義するモデルによっては可能です。例えばゲーデルの定理-2.3-で仮に「ペアノ自然数」と呼んだモデルです。
公理系としてペアノ公理系をとる。
自然数の集合でペアノ公理系から証明可能な命題のみを真と定義する。
真でない命題は偽と定義する。
するとこの形式的体系での論理式Bew(x)「ゲーデル数xである論理式は証明できる」は、まさにこのペアノ自然数モデルにおけるT(x)になります。すなわち、
T(a)「命題Aは真である」という命題はBew(a)に対応する。
¬T(a)「命題Aは偽である」という命題は¬Bew(a)に対応する。
しかし後者の場合はT(a)も¬T(a)も証明できない場合も含みますから、Bew(x)は命題T(a)を表現してはいません。
ところで、そもそも真理式T(x)を定義する命題4.2-2が証明可能性を使っていますが、替わりに次の命題を使うこともできるはずです。
命題4.2-3 すべての確定文(閉論理式)Aについて、命題A⇔T(a)が成り立つ。
この命題を使う場合は、命題A⇔T(a)が成り立つか否かはモデルを特定して、そのモデルについて確認しなければなりません。その代り、公理系をいちいち設定する必要はありません。逆に命題4.2-2を使う場合は、モデルによらず特定の公理系の中だけで話が済みます。ただし「すべての確定文」というのは無限集合ですから、それについて「命題が成り立つ」ことは数学的証明以外の方法では確認できないのが普通です。これでは命題4.2-3は使いずらいですね。
なお上記の「ペアノ自然数」のモデルは、実は、「ペアノ公理系の確定文」という台集合に「証明できる」という1項関係を加えた構造をモデルにしたものとも言えます。すなわち論理式の世界における、論理式の集合そのものをモデルにしたわけです。するとこのモデルでは「証明できる」と「真である」という命題が一致すると考えてよい、というわけです。
タルスキの真理定義の詳細は次回とします。
※コメント投稿者のブログIDはブログ作成者のみに通知されます