集合論言語とZFC公理系による数学の哲学のおはなし
こんにちは。気が付けば2023年も終わりを迎えようとしており、時の流れを感じております。
今日も懲りずに数学のお話を書くのですが、いつもの堅苦しい解説風の文体ではなく、ちょっとばかり柔らかい文体で書くことにしました。
今日書きたいのは「現代数学の議論ってなんだ？」ということです。
こんにち私たちは数学の議論を展開する際、自然言語で誰が見ても一意な解釈のできる定義と定理、そして証明を与えるということをしています。
しかし、数学を突き詰めていくと、例えば「数ってなんだ？」という素朴な疑問に繋がっていき、挙句、「集合ってなんだ？」「定理ってなんだ？」「証明ってなんだ？」という極めて基本的な、それでいて回答に困るような疑問に突き当たるわけです。
今日はそういった数学の哲学のお話をしたいと思います。
予め宣言しておきますが、いくつか参考にした教科書があり、それらを読んだ上で数学の哲学を述べていますが、如何せん私にはやや難しいお話ですから、理解が曖昧で、もしかすると誤り等あるかもしれません。若し内容が出鱈目書いていると思う場合は、ここに書いてあることはあくまで私の独り言だと思ってくだされば幸いです。
長々と前座を語っていても仕様がありませんので、早速本題に移ることとします。
目次
自然言語の証明は集合論言語による形式的な証明に書き下せないの？
以前こんな記事を投稿しました。
ここを見てもらえればわかりますが、殆どの内容は集合論言語とその上の1階述語論理体系のお話をしています。
後半から本題である公理的集合論のお話に移っていくのですが、その議論形式は非形式的に行われています。
例えば、定理1.15では包含に関する基本性質を述べ、それを証明していますが、この議論は前半の集合論言語の節で紹介したような形式的な議論で展開していません。
勿論、形式的な証明も可能ですが、それをしようとすると証明は幾分冗長になりますし、何よりややこしくなってしまいます。
今後、いわゆるZFC公理系を紹介していき、そこからペアノの公理を満たす自然数のシステムを構成し、さらに整数、有理数、実数、複素数の順に構成していきます。さらには順序数を定義し、そこから選択公理を仮定して基数、つまり集合の濃度を定義することを目標とします。
そうしたとき、目標となる数学概念を定義するには一体どの程度の証明が必要になるでしょうか。しかも、あくまでそれは「数学の基礎」に過ぎません。「基礎」を学んだら、そこから代数学、解析学、幾何学、その他数学分野に議論を発展させ、「いつもの数学」を議論していかねばなりません。
こうしたことから、すべての数学を「形式的」に証明できるでしょうか…？
答えは限りなく「ノー」に近いでしょう。話を進めれば進めるほど、数学は複雑になっていきます。それらをすべて形式的に証明したり、定義したりするなんて、人間の手作業では到底不可能に近い訳です。できたとしても、それで得られるものは何でしょうか？
きっと、絶対的な安心は得られることでしょう。でも、それに対する労力は果たして数学の発展に対して見合うものかと言われれば、きっとそうではないはずです。
そこで、私たちは通常の、自然言語による非形式的な証明は、すべて集合論言語による形式的な証明によって表現できると信じて議論を進めます。これは殆どの現代数学者の暗黙の了解です。
とはいえ、集合論言語とその上の1階述語論理体系を見せられてしまった人からすると、「いや！私は形式的証明しか認めたくないんだ！！！」…な～んて人が出てくるかもしれません。一応、そういう形式的な議論で書き下した教科書もこの世の中にはあるようです（例えば、Introduction to Axiomatic Set Theoryを参照）。
しかし、この世の中の定理の証明には形式的証明で書き下すにはあまりにも技巧的な非形式的な証明も多くあるでしょう。
わかりやすい例で言えば、集合論に近い分野である位相空間論でさえ、選択公理を用いて元をとってくる過程は具体的に書き下されることは少ないように思えます。実際に教科書や論文を読めばその選択関数をとる過程の「適当」さは確認できるでしょう。
試しに、位相空間論におけるチコノフの定理「コンパクトな位相空間の族の直積空間はコンパクトである」を形式的な証明で書き下そうとしてみるといいでしょう。きっと骨が折れる作業に違いありません。私なら絶対やりたくありませんし。
こうした、非形式的な証明を形式的に書き下すことはかなりの労力を費やすことになりますし、何よりその証明においてこの作業は本質的ではないと考えられます。
以上の理由から、私たちは自然言語による非形式的な証明は集合論言語による形式的な証明で書き下せると認めるのです。すべての数学は形式的なZFC公理系の集合論で表現できると考えるのです。
集合論言語と集合論におけるモデル理論は循環している？
上でおはなししたように、自然言語で書かれた数学は、すべて集合論言語で書かれた数学に埋め込まれます。
ところで、少し詳しい方であれば、モデル理論と証明論というものを学んでいることでしょう。いずれも、それぞれ意味論的に、構文論的にある言語上の1階述語論理体系を構築し、定理の正しさを厳密に解釈しようと試みます。
当然、集合論にも言語が考えられます。それが集合論言語を言語にもち、ZFC公理系を公理系にもつ1階述語論理体系です。
このときの集合論のモデルは構造であり、集合論言語の文
が意味論的帰結であることを
と表します。
が公理系
の定理であることを
と表します。特に,
をとれば、
は通常の数学における
の証明になります。
以上により、集合論をモデル理論と証明論で理解することができるようになりました。
…でもちょっと待ってください。集合論言語上の1階述語論理体系って、集合を使ってモデル理論や証明論を定義する前に定義していましたよね？集合論言語の上でZFC公理系を考えて、再度形式的な証明をする為に集合論言語を定義して…って、これって定義が循環しているように見えますよね？
この循環は、集合論を考える前の集合論言語と、集合論を考えている中の集合論言語を同一のものと考えていることに問題があります。この2つは鶏が先か、卵が先かというお話にしてしまっているのです。
実際には、集合論を考える前の集合論言語はメタ理論と呼ばれており、この議論の下でZFC公理系を導入し、その中でモデル理論における集合論言語を考えます。メタ理論については私の知識不足により詳しく存じ上げられないのですが、おおまかに説明すると、「有限集合に限定した推論を行い、議論すること」をいいます。
メタ理論において正しいといえる事実は論理的に帰結される有限的な推論だけです。このように考えれば、たとえメタ理論でどのような議論をしようとも、その議論は有限的な推論しかしていないのですから、誰がどう見ても異論の余地はなくなるでしょう。
この考え方の下で、形式的に述語記号や論理記号
、変数
といった記号を導入し、集合論言語を構成します。こうして集合論言語における変数を集合ということにし、議論のルールであるZFC公理系を導入することで、実際に数学を展開していくのです。ZFCの中では無限の概念が現れるのですが、そこでモデル理論と証明論により形式的な議論を焼き直すことになります。こうして無限の概念を取り扱うことができるようになるのです。
以上より、集合論言語をメタ理論により定義し、ZFC公理系を導入した後、その中でモデル理論により集合論言語を再度定義するので、集合論言語と集合論におけるモデル理論との間には議論の循環は起きていないことがわかります。
集合論は矛盾していない？
ここまで、集合論における議論とは何かについて述べてきました。要するに、集合論とはメタ理論で定義された集合という概念を、その中で形式的に議論する理論をいいます。その際、大抵の場合、証明は暗黙のうちに、自然言語による非形式的な議論は集合論言語による形式的な議論に書き換えられることを認めているのです。
こうして集合論の下で現代数学の議論が正当化されるのでした、めでたしめでたし…となるのですが、もう一つ問題が残っています。それは集合論の無矛盾性です。
私たちは集合論の公理系としてZFC公理系を採用することが多く、現代数学はその中で議論できることを認めています。しかし、肝心のZFC公理系が矛盾していては、その議論には何ら意味をなさなくなってしまいます。
なぜならば、矛盾する理論からは何でも導けてしまうからです。モデル理論において、偽の仮定からは結論の真偽に関わらず「ならば」の命題は真になることはよく知っている通りです。或いは、証明論においても、文と
をもつ公理系からはどのような文も証明できてしまうことがわかります。
こうした事実から、ZFC公理系は矛盾しない理論である、即ち無矛盾であることが保証されなければ、求めている数学の理論としては致命的です。果たして、ZFC公理系は無矛盾なのでしょうか？
答えは「ZFC公理系の下では『ZFC公理系が無矛盾である』ことは証明も反証もできない」のです。
若しZFC公理系が無矛盾で、さらにZFC公理系から「ZFC公理系が無矛盾である」ことが証明できてしまったら、ゲーデルの第二不完全性定理より、ZFC公理系は矛盾していることになってしまうのです。これは「ZFC公理系が無矛盾である」ことと「ZFC公理系は矛盾している」ことが両立しており、支離滅裂なことになります。従って、ZFC公理系が無矛盾なら、ZFC公理系から「ZFC公理系は無矛盾である」ことは証明できないことがわかりました。
一方で、ZFC公理系が無矛盾なら、ZFC公理系から「ZFC公理系は矛盾している」ことも証明できません。
故に、ZFC公理系の下、ZFC公理系が無矛盾であれば、ZFC公理系から「ZFC公理系は無矛盾である」ことも、「ZFC公理系は矛盾している」ことも証明できないことがわかりました。こういう命題を独立命題や、決定不能命題といいます。
ZFC公理系に矛盾があれば話は別ですが、現代の数学では、ZFC公理系は無矛盾であると暗黙の了解を置いて議論を展開することが殆どです。これは、ZFC公理系はカントールの素朴集合論から導かれた矛盾を、集合を厳密に定義することで解消することに成功しており、今に至るまでにZFC公理系から矛盾が導かれていないことに起因します。
以上より、ZFC公理系は無矛盾であることを証明も反証もできないので、経験則からZFC公理系は無矛盾であることを仮定することがわかりました。
おわりに
最後に本稿で述べたいことをまとめておきます。
集合論言語とその上の1階述語論理体系はメタ理論によって展開されており、集合論のモデル理論はZFC公理系の中で展開されるので循環しない議論である。
ZFC公理系が無矛盾ならば、ZFC公理系から「ZFC公理系が無矛盾であること」は証明も反証もできないので、慣例的にZFC公理系は無矛盾であることを仮定する。
以上の哲学的なお話は主に参考文献を読んで自分なりにまとめたものです。より細かいお話はそこに載っていますので、気になる方は是非読んでみてください。
