前回からの続き
実は数学基礎論においては、モデルとする集合(構造の領域)についてすべての命題の真偽は定まっているものとみなしています。ただしその真偽を有限回の手順で決定可能とは限りません[Webs-1c)6.3決定性]。つまり人間には有限の時間では確認できないとしても、神様は真偽を知っている！？
具体的には閉論理式∀ｘＲ(ｘ)の真偽は次のように定義します[Ref-3)p101-105, Ref-4)p80-81]。
定義2.2-1. 論理式の真偽
1) モデルでの関係Ｒ(ｔ)(ｔはある元を示す)がすべての元ｔについて成立すれば真
2) さもなければ、偽。つまり関係Ｒ(ｔ)が成立しない元ｔがひとつでもあれば、偽。
モデルが有限集合であればすべての元についてのＲ(ｔ)の真偽は原理的には枚挙法でわかりますが、無限集合の場合は一般には不可能です。それでも、知ることは不可能だとしても定まってはいる、とみなすというわけです。うがった見方をすれば、数学基礎論におけるモデル(特に無限モデル)とは人が触れることができる(観測できる)ものとは限らず、論理式に真理値を与えるために作り出された道具、すべての関係の真偽が定まっているという原理的に観測不能な性質を仮定した創造物、とも言えるでしょう。実際、集合というものは現実のものの集まりの抽象概念であり、抽象概念ゆえに、現実にはないものの集まりも表すことができます。そして集合上のｎ項関係というものが、ｎ個の元のすべての組み合わせについて真偽が定まっているものとして定義されている、というわけです。
さてゲーデルの完全性定理は図１で[公理０＋定理０]の論理式集合に対応する命題集合が[真理０＋真理０']そのものだという主張です。つまり以下の２つを主張します。
健全性 [公理０＋定理０]と対応する命題集合は[真理０＋真理０']に含まれる
完全性 [真理０＋真理０']と対応する論理式集合は[公理０＋定理０]に含まれる
健全性の証明は比較的簡単です。まず定義からして公理０と真理０は一致します。つまり公理０は[真理０＋真理０']に含まれます(恒真式)。次に論理式が恒真であるという性質が、古典述語論理体系での推論の過程で変わらないことが有限の手続きで証明できます。それは推論における手続きの種類が有限なのでひとつひとつ確認できるからです。すると、定理０の論理式は公理０から推論により導かれたものばかりなので、すべて恒真になります。
完全性の証明では次の定理がポイントになります。
定理2.2-1. 無矛盾な公理系はモデルを持つ
これさえ認めれば後は比較的簡単です。図２をご覧ください。公理０から証明できない論理式Ａに対応する命題Ａがモデル１で成り立つ(真である)とします。健全性の対偶から論理式￢Ａも証明できないので、公理０に論理式￢Ａを加えた公理反１を考えます。論理式Ａは公理０から証明できないので、公理系反１は無矛盾です。ゆえに上記定理から、そのモデル反１が存在します。そしてモデル反１もモデル１と同様に公理系０のモデルになります。すると命題Ａは、公理系０のすべてのモデルの共通部分で成立する命題ではありません。つまり、
定理2.2-2a. 公理系０で証明できない論理式は恒真ではない
この対偶により完全性が成立します。
定理2.2-2b. 恒真式ならば公理系０で証明できる
これ以上の詳細はRef-4,5などをご参照ください。
図２
さてこの証明でＡも￢Ａも証明できない、つまり公理系０が統語論的に不完全であることが前提されていることに御注意ください。実際、もし公理系０が統語論的に完全な場合は、論理式Ａが証明できなければ￢Ａの方が証明できて公理系０の定理となるはずです。すると公理系０のモデルであるモデル１では命題Ａは成り立たないはずであり、最初の前提に反します。同じ論法を使えば、統語論的に完全な公理系は意味論的にも完全であるということになります。図１を見ればわかるでしょうが、統語論的に完全な公理系０では[真理０＋真理０']から踏み出すようなモデルは表現できません。実際、「通常,統語論的に完全な理論は,意味論的にも完全である」(Ref5.p10)と言われます。
さてゲーデルの完全性定理は古典述語論理体系が健全かつ意味論的に完全であると述べていますが、これは古典述語論理体系を基とするあらゆる公理系もまた意味論的に完全であることを意味します。それは上記の証明概要でもわかる通りで、公理０としては矛盾さえ生じなければ何の制限もなく任意のもので成り立ちます。つまりゲーデルが統語論的には不完全だと証明した「自然数を含む形式的体系」もまた完全性定理での意味では完全なのです。この点は次回にでもまた詳しく述べましょう。
さて見落としやすいかも知れませんが、統語論的完全性をうんぬんするときは意味を持つ記号が限定されていなくてはなりません。不完全性定理は特定の公理系についての話であり、つまりはこの公理系のモデルとなる構造に限定された話だからです。例えば公理系０に、まだ定義されていなかった定数記号や関数記号や述語記号を持ち込めば、それを使った論理式は明らかに公理系０では証明できません。しかしそれはモデルに新しい元や関数や関係を想定することであり、いわば別の公理系の話になってしまいます。
例えば和という２項関数(演算)が定義された群論の公理系に全く別の積という２項関数を持ち込めば、これは環の公理系になってしまいます。ただし新しい関数積が既知の関数の和によって定義されるものならば、その限りではありません。例えば自然数の公理系では「後者」という関数だけを無定義の関数として持ち込むのが普通ですが、群論の公理系とは異なり、和も積も指数関数も「後者」だけで定義できますから、これらの関数も「後者」だけを持つ公理系で記述できることになります。
では次回から、その自然数を含む形式的体系での具体的な話を話します。
－－－－－－－－－－－－－－－－－－－
References
1) 野崎昭弘『不完全性定理―数学的体系のあゆみ(ちくま学芸文庫)』筑摩書房(2006/05)
2) 日本数学会『岩波数学辞典-第3版』岩波書店(1985/12) [71.記号論理]の項
3) 前原昭二『数学基礎論入門』朝倉書店(1977)
4) 上江洲忠弘『述語論理・入門―基礎からプログラムの理論へ』遊星社(2007/04)
5) 田中一之他『ゲーデルと20世紀の論理学(第2巻)完全性定理とモデル理論』東京大学出版会(2006/10)
6) 田中一之他『ゲーデルと20世紀の論理学(第3巻)2不完全性定理と算術の体系』東京大学出版会(2007/03)
webs
1) 平賀譲[筑波大学・図書館情報メディア研究科・教授]の講義資料
http://www.slis.tsukuba.ac.jp/~hiraga/mathinfo/print.shtml
1a) 命題論理 http://www.slis.tsukuba.ac.jp/~hiraga/mathinfo/docs/prop1.pdf
1b) 述語論理１ http://www.slis.tsukuba.ac.jp/~hiraga/mathinfo/docs/pred1.pdf
1c) 述語論理２ http://www.slis.tsukuba.ac.jp/~hiraga/mathinfo/docs/pred2.pdf
実は数学基礎論においては、モデルとする集合(構造の領域)についてすべての命題の真偽は定まっているものとみなしています。ただしその真偽を有限回の手順で決定可能とは限りません[Webs-1c)6.3決定性]。つまり人間には有限の時間では確認できないとしても、神様は真偽を知っている！？
具体的には閉論理式∀ｘＲ(ｘ)の真偽は次のように定義します[Ref-3)p101-105, Ref-4)p80-81]。
定義2.2-1. 論理式の真偽
1) モデルでの関係Ｒ(ｔ)(ｔはある元を示す)がすべての元ｔについて成立すれば真
2) さもなければ、偽。つまり関係Ｒ(ｔ)が成立しない元ｔがひとつでもあれば、偽。
モデルが有限集合であればすべての元についてのＲ(ｔ)の真偽は原理的には枚挙法でわかりますが、無限集合の場合は一般には不可能です。それでも、知ることは不可能だとしても定まってはいる、とみなすというわけです。うがった見方をすれば、数学基礎論におけるモデル(特に無限モデル)とは人が触れることができる(観測できる)ものとは限らず、論理式に真理値を与えるために作り出された道具、すべての関係の真偽が定まっているという原理的に観測不能な性質を仮定した創造物、とも言えるでしょう。実際、集合というものは現実のものの集まりの抽象概念であり、抽象概念ゆえに、現実にはないものの集まりも表すことができます。そして集合上のｎ項関係というものが、ｎ個の元のすべての組み合わせについて真偽が定まっているものとして定義されている、というわけです。
さてゲーデルの完全性定理は図１で[公理０＋定理０]の論理式集合に対応する命題集合が[真理０＋真理０']そのものだという主張です。つまり以下の２つを主張します。
健全性 [公理０＋定理０]と対応する命題集合は[真理０＋真理０']に含まれる
完全性 [真理０＋真理０']と対応する論理式集合は[公理０＋定理０]に含まれる
健全性の証明は比較的簡単です。まず定義からして公理０と真理０は一致します。つまり公理０は[真理０＋真理０']に含まれます(恒真式)。次に論理式が恒真であるという性質が、古典述語論理体系での推論の過程で変わらないことが有限の手続きで証明できます。それは推論における手続きの種類が有限なのでひとつひとつ確認できるからです。すると、定理０の論理式は公理０から推論により導かれたものばかりなので、すべて恒真になります。
完全性の証明では次の定理がポイントになります。
定理2.2-1. 無矛盾な公理系はモデルを持つ
これさえ認めれば後は比較的簡単です。図２をご覧ください。公理０から証明できない論理式Ａに対応する命題Ａがモデル１で成り立つ(真である)とします。健全性の対偶から論理式￢Ａも証明できないので、公理０に論理式￢Ａを加えた公理反１を考えます。論理式Ａは公理０から証明できないので、公理系反１は無矛盾です。ゆえに上記定理から、そのモデル反１が存在します。そしてモデル反１もモデル１と同様に公理系０のモデルになります。すると命題Ａは、公理系０のすべてのモデルの共通部分で成立する命題ではありません。つまり、
定理2.2-2a. 公理系０で証明できない論理式は恒真ではない
この対偶により完全性が成立します。
定理2.2-2b. 恒真式ならば公理系０で証明できる
これ以上の詳細はRef-4,5などをご参照ください。
図２
さてこの証明でＡも￢Ａも証明できない、つまり公理系０が統語論的に不完全であることが前提されていることに御注意ください。実際、もし公理系０が統語論的に完全な場合は、論理式Ａが証明できなければ￢Ａの方が証明できて公理系０の定理となるはずです。すると公理系０のモデルであるモデル１では命題Ａは成り立たないはずであり、最初の前提に反します。同じ論法を使えば、統語論的に完全な公理系は意味論的にも完全であるということになります。図１を見ればわかるでしょうが、統語論的に完全な公理系０では[真理０＋真理０']から踏み出すようなモデルは表現できません。実際、「通常,統語論的に完全な理論は,意味論的にも完全である」(Ref5.p10)と言われます。
さてゲーデルの完全性定理は古典述語論理体系が健全かつ意味論的に完全であると述べていますが、これは古典述語論理体系を基とするあらゆる公理系もまた意味論的に完全であることを意味します。それは上記の証明概要でもわかる通りで、公理０としては矛盾さえ生じなければ何の制限もなく任意のもので成り立ちます。つまりゲーデルが統語論的には不完全だと証明した「自然数を含む形式的体系」もまた完全性定理での意味では完全なのです。この点は次回にでもまた詳しく述べましょう。
さて見落としやすいかも知れませんが、統語論的完全性をうんぬんするときは意味を持つ記号が限定されていなくてはなりません。不完全性定理は特定の公理系についての話であり、つまりはこの公理系のモデルとなる構造に限定された話だからです。例えば公理系０に、まだ定義されていなかった定数記号や関数記号や述語記号を持ち込めば、それを使った論理式は明らかに公理系０では証明できません。しかしそれはモデルに新しい元や関数や関係を想定することであり、いわば別の公理系の話になってしまいます。
例えば和という２項関数(演算)が定義された群論の公理系に全く別の積という２項関数を持ち込めば、これは環の公理系になってしまいます。ただし新しい関数積が既知の関数の和によって定義されるものならば、その限りではありません。例えば自然数の公理系では「後者」という関数だけを無定義の関数として持ち込むのが普通ですが、群論の公理系とは異なり、和も積も指数関数も「後者」だけで定義できますから、これらの関数も「後者」だけを持つ公理系で記述できることになります。
では次回から、その自然数を含む形式的体系での具体的な話を話します。
－－－－－－－－－－－－－－－－－－－
References
1) 野崎昭弘『不完全性定理―数学的体系のあゆみ(ちくま学芸文庫)』筑摩書房(2006/05)
2) 日本数学会『岩波数学辞典-第3版』岩波書店(1985/12) [71.記号論理]の項
3) 前原昭二『数学基礎論入門』朝倉書店(1977)
4) 上江洲忠弘『述語論理・入門―基礎からプログラムの理論へ』遊星社(2007/04)
5) 田中一之他『ゲーデルと20世紀の論理学(第2巻)完全性定理とモデル理論』東京大学出版会(2006/10)
6) 田中一之他『ゲーデルと20世紀の論理学(第3巻)2不完全性定理と算術の体系』東京大学出版会(2007/03)
webs
1) 平賀譲[筑波大学・図書館情報メディア研究科・教授]の講義資料
http://www.slis.tsukuba.ac.jp/~hiraga/mathinfo/print.shtml
1a) 命題論理 http://www.slis.tsukuba.ac.jp/~hiraga/mathinfo/docs/prop1.pdf
1b) 述語論理１ http://www.slis.tsukuba.ac.jp/~hiraga/mathinfo/docs/pred1.pdf
1c) 述語論理２ http://www.slis.tsukuba.ac.jp/~hiraga/mathinfo/docs/pred2.pdf
