ロックバンドZFC48を構想する！

　先日、千葉大学の数理論理学者の古森雄一先生からメールをいただいた。『現代数理論理学序説』(日本評論社)などの著作のある、論文業績もりっぱな専門家のかただ。
内容は、このブログの以前のエントリー(バンド不完全性定理を構想する。 - hiroyukikojimaの日記)に関する感想と質問と提案だった。古森さんのメールのタイトルが``「バンド不完全性定理を構想する」について''、だったので、正直ぶったまげた。まさか、バンドにベーシストかなんかで応募してんじゃないだろうな、などと一瞬頭をよぎったが、もちろんそうではなかった。(あたりまえだ)。古森さんからいただいた話はかなり高度になるので、後回しにして、せっかくの機会だから、今書きたいバンドの話を先に書こうと思う。
　(バンド不完全性定理を構想する。 - hiroyukikojimaの日記)のエントリーでは、自分がゼミ生とバンドを組むので、その構想を述べた。それは、実在のバンド相対性理論の向こうをはって、バンド不完全性定理にしようか、という話だった。詳しくは、そのエントリーを読んで欲しいが、要は、ボーカロイドで作ったような曲を実際の人間の女子が歌う、という構想だった。ゼミ生とのライブは、昨年の11月に実現されたのだが(今年のマイ・イベントが全部終了した。 - hiroyukikojimaの日記参照)、それはコピーバンドだったので、オリジナルバンドの構想はまだ残されている。だから、今年こそと、思っていた。
しかし、この構想は、すでに、あるアーティストに実行されてしまっていたのだ。それは、あの、柴咲コウだった。柴咲さんは、最新のアルバム「Circle Cycle」で、DECO*27という人とコラボしている。DECO*27さんは、DECO*27 - Wikipediaによると、ボーカロイド初音ミクで楽曲を作り、それをニコ動にアップして有名になった人らしい。そして、柴咲さんのオファーでユニットを組んだのである。
とにかく「Circle Cycle」は、あまりにすごいアルバムだ。とりわけ、DECO*27さんと作った「無形スピリット」は、ここ一年に作られた中で、最も斬新な曲だと言えると思う(当社比)。ウソだと思ったら、youtubeで、「無形スピリット　studio live」検索して、観てみそ。びっくらすっからさ。そんで、すぐさま、「Circle Cycle」の武道館ライブDVDも観てみた。あまりにすばらしかった。「wish」という曲の最初のMCでは、泣きそうになった。感動のライブだった。このとき会場にいれればな、と思った。
木村カエラの結婚と同時に、彼女の曲(全部持ってた)をすべてipodから削除したぼくなので(笑い、もちろんCDは捨ててないすよ)、柴咲さんという新しい追っかけ対象を見つけたことはありがたいことだった。しばらくは、これで、楽しく暮らすことができる。(学生たちには、YUIが結婚したら木村カエラの比ではない、一週間休講になるからね、と予告してある。笑い)。
まあ、いずれにしても、柴咲さんに構想を先取りされてしまったので(って、そもそも競争になってないさね)、バンド不完全性定理の構想は捨てることになった。さて、そこで古森先生からのメールの話につながる。
古森先生からは、二つのコメントがあった。一つは、ぼくが(バンド不完全性定理を構想する。 - hiroyukikojimaの日記)に書いたある補助定理について、その表記の仕方についての質問だった。さすが、業績のある専門家は余裕が違うね。基本的にぼくの言いたいことは合ってるだろう、という前提で考えていてくださっていた。(他のページを読んで、そう思ったのなら嬉しいことだ)。そして、ぼくが正しいことを言おうとしているにもかかわらず、表現に失敗している、と考えてくださったようだ。そこで、少し専門的なやりとりをして、ぼくの言おうとしていることはその表現で間違っていないことを理解していただいた。くどいようだが、非専門家に対するこういう余裕のある建設的な態度こそが、高い業績を持つりっぱな専門家のありかただろうと思う(当社比)。
さて、古森先生のもう一つのコメントが、今回の話題だ。それは、ZFC（ツェルメロ・フレンケル集合論 + 選択公理）のことだ。ぼくが、(バンド不完全性定理を構想する。 - hiroyukikojimaの日記)に、基礎論のメタ証明(ある公理系の証明能力などについて何かを主張するメタ定理の証明、つまり、外側の証明)について、

いわば「人間の理性」が数学者のコンセンサスであるところの「証明」を自由奔放に振り回す世界

と書いたことについて、重要なコメントをいただいた。古森先生によると、実際のところ基礎論の専門家のほとんどは、メタ証明(外側の証明)は、ZFC（ツェルメロ・フレンケル集合論 + 選択公理）で十分と考えているので、そのことを書き加えて欲しい、というご要望をいただいたのである。なぜ、そんなに読者が多いわけではないぼくのブログで、わざわざ、基礎論の専門家のコンセンサスをアナウンスして欲しいとおっしゃるのか、その真意はわからないけれど、とても光栄なことだし、ぼくもよく知らないことだったので、追加することにした。(バンド不完全性定理を構想する。 - hiroyukikojimaの日記に赤い字で書き加えてある)。
ツェルメロ・フレンケル集合論というのは、カントールの作り出した集合論が多くの数学的素材を実現することができる一方で、深刻な矛盾も生み出してしまうこと(拙著『無限を読みとく数学入門』角川ソフィア文庫参照)に対して、なんとかその矛盾(パラドクス)を回避するために作り出した、集合の扱いについての公理系である。[外延公理][対公理][和集合公理][べき集合公理][空集合公理][無限公理][置換公理図式][正則性公理]から成る。集合を規定したり、構成したり、操作したり、空集合や無限集合の存在を述べたりするルールだと思えばいい。これに、選択公理(無限個の集合から1個ずつ要素を取り出せる)を加えたものがZFCとなる。
古森先生に教えていただいたことによれば、数学基礎論の進歩によって、「現存するすべての数学の定理の証明は、ZFCで形式化できる」と考えられているのだそうだ。例えば、ジョルダンの曲線定理(拙著『文系のための数学教室』講談社現代新書を参照のこと)の証明などは、ZFCで形式化できることがわかっているとのこと。つまり、メタ定理を証明する際には、(たぶん)ZFCで形式化可能な証明だけを考えれば十分、ということなのである。「自由奔放」には、そういう上限を定めても問題ない、ということなのだ。まとめてみよう。

１.数学の(基礎論に限らず)すべての証明は、ZFCで形式化できる(と信じられている)。
２．有利な証拠として、例えば、ジョルダンの曲線定理などは、実際にZFCで形式化されている。(確認は大変だったそうだ）
３．不利な証拠は、今のところ、一つも見つかっていない。
４。証明をZFCで形式化すれば、あとになって証明に間違いがみつかる、という悲惨なことがなくなる。

ぼく自身は、ZFCがたぶん無矛盾な(=矛盾を孕まない)公理系であろうこと、集合論を展開する際に十分リッチな公理系であることまでは知っていた。でも、すべての数学の証明を記述できる(形式化できる)ようなリッチさだとまでは知らなかった。基礎論がそこまで発展していたとは、驚きである。(もちろん、まだ完全に確認されたわけではない。あくまでコンセンサスの段階)。もし、これが正しければ、数学の研究に抜本的な変革がもたらされるに違いない。
実は、ある数学者Xさんから聞いた話だが、数学者たちが集まった席でとある数学者Yさんが、上記のこと(ZFCですべての数学が形式化できること)を言ったら、そこにいた数人の数学者たちが「そんなことはどうでもいい」と猛然と怒り出したという。この話を聞かせてくれたXさん自身も、「どうでもいい」派の一人だと言っていた。まあ、数学の形式化ということに、どのくらいの数学的な重要度をみているか、あるいは、それがもたらす実益(例えば、自動証明とか、人工知能とか、暗号解読とか、認識論とか)にどのくらいの興味を持っているかで、反応にだいぶ温度差があるだろうな、と思う。ぼく自身は、そもそもゲーム理論を研究対象の一つとしているので、上記のことは、スゴイことだと思うし、大いに興味がある。
さて、またバンドの話に戻ろう。バンド不完全性定理の構想は、もろくも崩れ去った。というわけで、今度は、もっとスゴイ構想、バンドZFCを構想してみたいと思う。これは、すべての音楽ジャンルを飲み込むものだ。流行に乗って48をつけ、バンドZFC48にしたらいいかな、などとも思う(完全ばか）。ついでにいうと、総選挙で1位になるのは、意外にも大島さんではなく、まゆゆあたりだったりして、などと妄想している。(ちなみに自分は、コジハルのファン)。