共通参考文献はこちら
前回からの続き
アルフレト・タルスキ(Alfred Tarski)という数学者は、「球を分割再構成して2倍にできる」(あまり正確じゃないかな)というパラドックス的な「バナッハ=タルスキの定理」で有名です。リンク先のwikiの記事の通り、彼はゲーデルと交流がありました。そして[Ref-6)p19]によれば、「不完全性定理の初期のバージョンは、タルスキの真理定義不可能性定理とほとんど同じだったといえる。」とのことです。
すわ先取権争いか? ですが、数学基礎論三つの神話(林普)によれば、やや複雑な事情があったようです。ゲーデル論文の発表は1931年で、その少し前にタルスキのポーランド語の論文で「n+1階の算術で,n階の算術の真理概念の定義ができる」ことが発表されていますが、後に(ゲーデル論文を知った後)改めて出版する際に「定義不可能性定理とその証明」を付け加えたとのことです。
さて[Ref-6) p218]によれば、タルスキーによる「真であることの定義」とは次のようなものです。
命題4.2-4 xが真であるのはpのときそのときに限る
x : 形式言語L中の式Xの名前
p : メタ言語の中でのXの翻訳文
メタ言語というのは形式言語L自体について色々と議論している言語、普通は数学者が使う自然言語です。よってXの翻訳文というのは、大抵はなんらかのモデルについての言明と言えるでしょう。さもなくば「pのとき」であるのか否かが判断できないはずです。つまり命題4.2-4は「何らかのモデルの真偽により式Xの真偽を判定する」と言っているように、私には見えます。
そしてメタ言語の中で命題4.2-4のようにキチンと表記された命題は、形式言語の中の対応する論理式を構成しやすくなります。つまり「xが真である」という命題に対応する論理式をT(x)とすれば、「pのとき」という命題に対応する論理式はXだったので、命題4.2-4に対応する論理式は次の式4.2-1になります。まさに前回にゲーデル文を使って定義したT(x)そのものです。
式4.2-1 T(x)⇔X
このようなT(x)が構成できるか否かは「真である論理式の集合」を決定するモデルに依存しますが、たとえ構成できたとしても、構成されたT(x)の「真理論理式である必要十分条件」と言える「式4.2-1が全ての閉論理式Xについて成り立つ」ということは、形式言語Lで書かれた公理系の中では証明できません。それがタルスキの真理定義不可能性定理です。
要するにタルスキの真理定義不可能性定理は「真である論理式の集合」をどのように決定しようが成立します。それを反映して、スマリヤンは[Ref-s3]で「真である論理式の集合」「証明可能な論理式の集合」「反証可能な論理式の集合」を無定義で導入するところから議論を始めています。すなわち次のような論理式の集合を導入して、ゲーデルやタルスキーの定理をより一般的な形で証明しようとしています。
S : 確定文(閉論理式)S全ての集合
P : 証明可能な確定文P全ての集合
R : 反証可能な確定文R全ての集合。¬Rが証明可能。
T : 真なる確定文T全ての集合。
Pcp=S-P : 証明できない確定文の集合
Tcp=S-T : 真ではない(偽なる)確定文の集合
なお、補集合を示すPcpのような記号などは原文とは変えています。無定義とはいってもここで各集合には次のような性質は必要でしょう。
・すべての論理式A∈Sについて、A∈Tと¬A∈Tcpとは同値。 [真偽についての無矛盾性]
・PとRとの共通部分はない。 [証明可能性についての無矛盾性]
このような無定義での導入により、「真である論理式の集合」「証明可能な論理式の集合」を具体的に決めなくても、この2つの集合の間に特定の関係が成立すれば、ゲーデルの不完全性定理やタルスキの真理定義不可能性定理がメタ数学的に証明されます。その特定の関係とは例えば健全性に該当する、「正確である」という性質です。
定義 P⊂Tであるとき、この体系は正確であるという。
つまり体系が正確であるとは、「すべての証明可能な論理式は真である」ことです。そして体系が正確であるという条件の下でゲーデルの不完全性定理が成立することが示せます[Ref-s3]。前原[Ref-3]が書いているようなゲーデル自身の証明ではω無矛盾であるという条件の下で不完全性定理の成立が示されていますが、この条件を使うには上記の無定義の真理集合などを導入した体系に、さらにω無矛盾というものを定義していかなくてはなりません。またロッサー(J.B.Rosser)はゲーデルよりも一歩進んで単に無矛盾であるという条件の下で、Uも¬Uも証明できない確定文Uを作り出しました。
次回は対角化定理の証明に入ります。
前回からの続き
アルフレト・タルスキ(Alfred Tarski)という数学者は、「球を分割再構成して2倍にできる」(あまり正確じゃないかな)というパラドックス的な「バナッハ=タルスキの定理」で有名です。リンク先のwikiの記事の通り、彼はゲーデルと交流がありました。そして[Ref-6)p19]によれば、「不完全性定理の初期のバージョンは、タルスキの真理定義不可能性定理とほとんど同じだったといえる。」とのことです。
すわ先取権争いか? ですが、数学基礎論三つの神話(林普)によれば、やや複雑な事情があったようです。ゲーデル論文の発表は1931年で、その少し前にタルスキのポーランド語の論文で「n+1階の算術で,n階の算術の真理概念の定義ができる」ことが発表されていますが、後に(ゲーデル論文を知った後)改めて出版する際に「定義不可能性定理とその証明」を付け加えたとのことです。
さて[Ref-6) p218]によれば、タルスキーによる「真であることの定義」とは次のようなものです。
命題4.2-4 xが真であるのはpのときそのときに限る
x : 形式言語L中の式Xの名前
p : メタ言語の中でのXの翻訳文
メタ言語というのは形式言語L自体について色々と議論している言語、普通は数学者が使う自然言語です。よってXの翻訳文というのは、大抵はなんらかのモデルについての言明と言えるでしょう。さもなくば「pのとき」であるのか否かが判断できないはずです。つまり命題4.2-4は「何らかのモデルの真偽により式Xの真偽を判定する」と言っているように、私には見えます。
そしてメタ言語の中で命題4.2-4のようにキチンと表記された命題は、形式言語の中の対応する論理式を構成しやすくなります。つまり「xが真である」という命題に対応する論理式をT(x)とすれば、「pのとき」という命題に対応する論理式はXだったので、命題4.2-4に対応する論理式は次の式4.2-1になります。まさに前回にゲーデル文を使って定義したT(x)そのものです。
式4.2-1 T(x)⇔X
このようなT(x)が構成できるか否かは「真である論理式の集合」を決定するモデルに依存しますが、たとえ構成できたとしても、構成されたT(x)の「真理論理式である必要十分条件」と言える「式4.2-1が全ての閉論理式Xについて成り立つ」ということは、形式言語Lで書かれた公理系の中では証明できません。それがタルスキの真理定義不可能性定理です。
要するにタルスキの真理定義不可能性定理は「真である論理式の集合」をどのように決定しようが成立します。それを反映して、スマリヤンは[Ref-s3]で「真である論理式の集合」「証明可能な論理式の集合」「反証可能な論理式の集合」を無定義で導入するところから議論を始めています。すなわち次のような論理式の集合を導入して、ゲーデルやタルスキーの定理をより一般的な形で証明しようとしています。
S : 確定文(閉論理式)S全ての集合
P : 証明可能な確定文P全ての集合
R : 反証可能な確定文R全ての集合。¬Rが証明可能。
T : 真なる確定文T全ての集合。
Pcp=S-P : 証明できない確定文の集合
Tcp=S-T : 真ではない(偽なる)確定文の集合
なお、補集合を示すPcpのような記号などは原文とは変えています。無定義とはいってもここで各集合には次のような性質は必要でしょう。
・すべての論理式A∈Sについて、A∈Tと¬A∈Tcpとは同値。 [真偽についての無矛盾性]
・PとRとの共通部分はない。 [証明可能性についての無矛盾性]
このような無定義での導入により、「真である論理式の集合」「証明可能な論理式の集合」を具体的に決めなくても、この2つの集合の間に特定の関係が成立すれば、ゲーデルの不完全性定理やタルスキの真理定義不可能性定理がメタ数学的に証明されます。その特定の関係とは例えば健全性に該当する、「正確である」という性質です。
定義 P⊂Tであるとき、この体系は正確であるという。
つまり体系が正確であるとは、「すべての証明可能な論理式は真である」ことです。そして体系が正確であるという条件の下でゲーデルの不完全性定理が成立することが示せます[Ref-s3]。前原[Ref-3]が書いているようなゲーデル自身の証明ではω無矛盾であるという条件の下で不完全性定理の成立が示されていますが、この条件を使うには上記の無定義の真理集合などを導入した体系に、さらにω無矛盾というものを定義していかなくてはなりません。またロッサー(J.B.Rosser)はゲーデルよりも一歩進んで単に無矛盾であるという条件の下で、Uも¬Uも証明できない確定文Uを作り出しました。
次回は対角化定理の証明に入ります。
※コメント投稿者のブログIDはブログ作成者のみに通知されます