前回からの続きです。
「全てのカラスは黒い」という命題を確かめるには、一匹一匹のカラスが黒いか黒くないかを確認して、それを全てのカラスについて行えばよいでしょう。しかしカラスが無限にいたとしたら、証明は原理的に不可能です。もちろん反例が見つかれば否定命題である「黒くないカラスがいる」が証明できますが、「全てのカラスは黒い」という命題が正しい場合には、いつまでたってもこの命題も、その否定も証明できません。帰納法*1の限界というものです。
つまるところゲーデルの第一不完全性定理は、このような限界というものが数学理論においてもあるのだと言っているのです。要点は「自然数の公理系を含む」というところで、つまり無限個の対象を扱っているところです。ゲーデルの証明では全ての論理式にゲーデル数という自然数を１対１対応させることで論理式の集合を自然数の部分集合に対応させてしまいます。論理式の集合もまた可算無限個なのですが、全体を部分に１対１対応させられるという無限集合の特質をいかんなく発揮しているのです。このことにより自己言及的な「それ自身もその否定も証明できない閉論理式」が作り出されるのです。そして実はこの「それ自身もその否定も証明できない閉論理式」の具体的なものが「全てのカラスは黒い」という命題と類似形をしているのです。それを端的に示すのが前原のRef3,p136の定理8.8です。
－－－－－－－－
定理8.8 論理式の集合Ｋが表現可能かつ無矛盾ならば、次の１，２を満たす１変数ｘの論理式Ｒ(ｘ)が存在する。
１． Ｒ(０)、Ｒ(１)、Ｒ(２)、・・・は全て証明できる
２． ∀ｘＲ(ｘ)は証明できない
－－－－－－－－
Ｒ(０)、Ｒ(１)、Ｒ(２)、・・・というのはまさに、ひとつひとつのカラスについての命題の確認です。それが全て真であっても∀ｘＲ(ｘ)「全てのカラスは黒い」という命題は確認することができないのです。
なお定理8.8で「表現可能」とは「モデルでの真偽と形式的体系での証明可能性とが対応している」というような意味です(Ref3,p101-104)。意味論的完全性に似ていますが、表現可能というのは個別の論理式の性質であり*2、意味論的完全性は公理系の性質です。モデルでの真偽の定義の話は・・、また後ほど。
ここで∀ｘＲ(ｘ)が証明できないので、￢∀ｘＲ(ｘ)すなわち∃ｘ￢Ｒ(ｘ)を公理として付け加えても矛盾は生じません。Ｒ(０)、Ｒ(１)、Ｒ(２)、・・・は全て証明できる、にもかかわらず￢∀ｘＲ(ｘ)も証明できる公理系は「ω矛盾している(ω-inconsistent)」と呼ばれます(Ref3,p128-129)。
さて形式的体系について語るときの要点のひとつは閉論理式というところです。閉論理式の正確な意味は後ほど述べますが、大切なことは「特定の理論を表す形式的体系」(例えば自然数の公理系、例えばユークリッド幾何学の公理系)では閉論理式とは「意味のある論理式」(真偽が定まっているはずの命題に対応する論理式)と同じになるということです。そのために「特定の理論を表す形式的体系」においては、「その閉論理式もその否定も共に証明できないものが必ずある」という命題は「モデルにおいて真である命題に対応する論理式の中に、それ自身もその否定も共に証明できないものが必ずある」と言い換えることができるのです。もっともそこで「真であることの定義は何？」という話がすっきりしないと理解もすっきりしないのですが。
ところで例えば幾何学のモデルのように、モデルが違えばある命題の真偽も異なるという認識が現代では普通のように見えます。するとそれらのモデルを表現する形式的体系に真偽の決まらない論理式が存在することはむしろ当然に思えます。いや、真偽の決まらない論理式が多ければ、それだけ多様なモデルを表現できる豊かな体系だとも言えるかも知れません。にもかかわらず自然数の公理系はなぜ完全であるべきだと思われていたのでしょうか？ 単にゲーデル以前の人々の思い込みから来ていただけなのでしょうか？ 細かい考察は長くなりそうですが、実在？の自然数とは異なる別のモデルというものが考えだしにくい(たぶん考え出されていない)という理由はありそうです。
一方でゲーデルの完全性定理は「１階述語論理の体系」について述べているのであり、「特定の理論を表す形式的体系」の話ではありません。こちらは意味論的完全性についてなのでモデルでの真偽を使うのですが、特定のモデルではなくて、どのモデルでも真になる命題を問題にします。述語論理においては「どのモデルでも真になる命題」に対応する論理式を「恒真論理式」といいます。命題論理における恒真は、通常は述語論理での定義とは少し違ってプール代数で真偽を定義するのですが、意味としては同じとも言えます。
ところで「特定の理論を表す形式的体系」は述語論理を土台としており、述語論理は命題論理を土台にしています。この述語論理や命題論理のレベルでも様々な公理系を考えることができますが、これらの公理系は幾何学の公理系のように具体的対象は扱わなず論理だけを表していますので、幾何学や代数の公理系と区別したいときは論理体系と呼ぶことにしましょう。さて考えうる様々な論理体系のなかでゲーデルの完全性定理で意味論的完全性が成り立つと証明された１階述語論理というのは、任意に作れる様々な論理体系の中のたった一つの特定の公理系であり、古典論理と呼ばれる論理体系です。そして数学のいや科学そのものの土台をなす上記の述語論理というのは、まさにこの古典論理です。
古典論理以外の論理体系で(たぶん)無矛盾なもののひとつにブラウワー(Brouwer)の直観主義(Intuitionism)に始まりハイティング(Arend Heyting)が発展させた直観論理(Intuitionistic logic)がありますが、これは排中律を認めないものです。つまりＡ∨￢Ａという論理式の真偽を定めません。言い換えると証明できない論理式を意図的に導入した論理体系、つまり、意図的に統語論的に不完全にした論理体系ということになります。なお直観論理が古典論理と異なるのは命題論理レベルからであることに御注意ください。しかもそもそも真という概念が違ってきますから、健全性とか完全性という概念もそのまま適用してよいかどうかは疑問かも知れません。
なおBrouwerはオランダ人ですが、ブラウワーは英語読みで原語ではブローエルのようです[(Ref-1)p128]。
ではいよいよ次回から、「真であることの定義」の謎解きに立ち向かいたいと思います。
－－－－－－－－
*1) 数学的帰納法ではなくて演繹に対比される帰納。ここでカラスという例を持ち出したのは知る人ぞ知る鴉のパラドックス(Raven paradox)に由来する。カラスの逆説-1-から始まる本ブログのシリーズ記事も参照のこと。
*2) モデルにおける命題ｐを表現する論理式が存在すれば「命題ｐは表現可能」となり、形式的体系での論理式Ｐにより表現できる命題があるモデルに存在すれば「論理式Ｐは表現可能」となる。
「全てのカラスは黒い」という命題を確かめるには、一匹一匹のカラスが黒いか黒くないかを確認して、それを全てのカラスについて行えばよいでしょう。しかしカラスが無限にいたとしたら、証明は原理的に不可能です。もちろん反例が見つかれば否定命題である「黒くないカラスがいる」が証明できますが、「全てのカラスは黒い」という命題が正しい場合には、いつまでたってもこの命題も、その否定も証明できません。帰納法*1の限界というものです。
つまるところゲーデルの第一不完全性定理は、このような限界というものが数学理論においてもあるのだと言っているのです。要点は「自然数の公理系を含む」というところで、つまり無限個の対象を扱っているところです。ゲーデルの証明では全ての論理式にゲーデル数という自然数を１対１対応させることで論理式の集合を自然数の部分集合に対応させてしまいます。論理式の集合もまた可算無限個なのですが、全体を部分に１対１対応させられるという無限集合の特質をいかんなく発揮しているのです。このことにより自己言及的な「それ自身もその否定も証明できない閉論理式」が作り出されるのです。そして実はこの「それ自身もその否定も証明できない閉論理式」の具体的なものが「全てのカラスは黒い」という命題と類似形をしているのです。それを端的に示すのが前原のRef3,p136の定理8.8です。
－－－－－－－－
定理8.8 論理式の集合Ｋが表現可能かつ無矛盾ならば、次の１，２を満たす１変数ｘの論理式Ｒ(ｘ)が存在する。
１． Ｒ(０)、Ｒ(１)、Ｒ(２)、・・・は全て証明できる
２． ∀ｘＲ(ｘ)は証明できない
－－－－－－－－
Ｒ(０)、Ｒ(１)、Ｒ(２)、・・・というのはまさに、ひとつひとつのカラスについての命題の確認です。それが全て真であっても∀ｘＲ(ｘ)「全てのカラスは黒い」という命題は確認することができないのです。
なお定理8.8で「表現可能」とは「モデルでの真偽と形式的体系での証明可能性とが対応している」というような意味です(Ref3,p101-104)。意味論的完全性に似ていますが、表現可能というのは個別の論理式の性質であり*2、意味論的完全性は公理系の性質です。モデルでの真偽の定義の話は・・、また後ほど。
ここで∀ｘＲ(ｘ)が証明できないので、￢∀ｘＲ(ｘ)すなわち∃ｘ￢Ｒ(ｘ)を公理として付け加えても矛盾は生じません。Ｒ(０)、Ｒ(１)、Ｒ(２)、・・・は全て証明できる、にもかかわらず￢∀ｘＲ(ｘ)も証明できる公理系は「ω矛盾している(ω-inconsistent)」と呼ばれます(Ref3,p128-129)。
| ￢∀ｘＲ(ｘ)は証明可能 | ￢∀ｘＲ(ｘ)は証明不可 | |
| ∀ｘＲ(ｘ)は証明可能 | 矛盾 | ω無矛盾、表現可能 |
| ∀ｘＲ(ｘ)は証明不可 | ω矛盾かつ無矛盾 | ω無矛盾、表現不可 |
さて形式的体系について語るときの要点のひとつは閉論理式というところです。閉論理式の正確な意味は後ほど述べますが、大切なことは「特定の理論を表す形式的体系」(例えば自然数の公理系、例えばユークリッド幾何学の公理系)では閉論理式とは「意味のある論理式」(真偽が定まっているはずの命題に対応する論理式)と同じになるということです。そのために「特定の理論を表す形式的体系」においては、「その閉論理式もその否定も共に証明できないものが必ずある」という命題は「モデルにおいて真である命題に対応する論理式の中に、それ自身もその否定も共に証明できないものが必ずある」と言い換えることができるのです。もっともそこで「真であることの定義は何？」という話がすっきりしないと理解もすっきりしないのですが。
ところで例えば幾何学のモデルのように、モデルが違えばある命題の真偽も異なるという認識が現代では普通のように見えます。するとそれらのモデルを表現する形式的体系に真偽の決まらない論理式が存在することはむしろ当然に思えます。いや、真偽の決まらない論理式が多ければ、それだけ多様なモデルを表現できる豊かな体系だとも言えるかも知れません。にもかかわらず自然数の公理系はなぜ完全であるべきだと思われていたのでしょうか？ 単にゲーデル以前の人々の思い込みから来ていただけなのでしょうか？ 細かい考察は長くなりそうですが、実在？の自然数とは異なる別のモデルというものが考えだしにくい(たぶん考え出されていない)という理由はありそうです。
一方でゲーデルの完全性定理は「１階述語論理の体系」について述べているのであり、「特定の理論を表す形式的体系」の話ではありません。こちらは意味論的完全性についてなのでモデルでの真偽を使うのですが、特定のモデルではなくて、どのモデルでも真になる命題を問題にします。述語論理においては「どのモデルでも真になる命題」に対応する論理式を「恒真論理式」といいます。命題論理における恒真は、通常は述語論理での定義とは少し違ってプール代数で真偽を定義するのですが、意味としては同じとも言えます。
ところで「特定の理論を表す形式的体系」は述語論理を土台としており、述語論理は命題論理を土台にしています。この述語論理や命題論理のレベルでも様々な公理系を考えることができますが、これらの公理系は幾何学の公理系のように具体的対象は扱わなず論理だけを表していますので、幾何学や代数の公理系と区別したいときは論理体系と呼ぶことにしましょう。さて考えうる様々な論理体系のなかでゲーデルの完全性定理で意味論的完全性が成り立つと証明された１階述語論理というのは、任意に作れる様々な論理体系の中のたった一つの特定の公理系であり、古典論理と呼ばれる論理体系です。そして数学のいや科学そのものの土台をなす上記の述語論理というのは、まさにこの古典論理です。
古典論理以外の論理体系で(たぶん)無矛盾なもののひとつにブラウワー(Brouwer)の直観主義(Intuitionism)に始まりハイティング(Arend Heyting)が発展させた直観論理(Intuitionistic logic)がありますが、これは排中律を認めないものです。つまりＡ∨￢Ａという論理式の真偽を定めません。言い換えると証明できない論理式を意図的に導入した論理体系、つまり、意図的に統語論的に不完全にした論理体系ということになります。なお直観論理が古典論理と異なるのは命題論理レベルからであることに御注意ください。しかもそもそも真という概念が違ってきますから、健全性とか完全性という概念もそのまま適用してよいかどうかは疑問かも知れません。
なおBrouwerはオランダ人ですが、ブラウワーは英語読みで原語ではブローエルのようです[(Ref-1)p128]。
ではいよいよ次回から、「真であることの定義」の謎解きに立ち向かいたいと思います。
－－－－－－－－
*1) 数学的帰納法ではなくて演繹に対比される帰納。ここでカラスという例を持ち出したのは知る人ぞ知る鴉のパラドックス(Raven paradox)に由来する。カラスの逆説-1-から始まる本ブログのシリーズ記事も参照のこと。
*2) モデルにおける命題ｐを表現する論理式が存在すれば「命題ｐは表現可能」となり、形式的体系での論理式Ｐにより表現できる命題があるモデルに存在すれば「論理式Ｐは表現可能」となる。
