現在2020年5月15日19時04分である。
麻友「ちょっと、ショッキングな題じゃない?」
私「完全にいらない、というのは、言いすぎかも知れないけど、ブルバキよりもっと良いものが、出来つつある」
若菜「どういうことですか?」
私「Mathematica を作っている、ウルフラムからメールが来て、Mathematicaの12.1 バージョンを、発表したという」
Mathematicaの12.1の新機能のまとめreference.wolfram.com
結弦「お父さん、そういうメーリングリストに、登録してあるんだ」
私「前回買ったときから、メールアドレスは登録してあるから、営業としては、送ってくる。ただ、AOLからGmailに乗り換えたとき、ちゃんと申請したからでもある」
若菜「その Mathematicaの12.1 が、良かったのですか?」
私「わざと字を間違えたんじゃないか? と思う項目があった」
・一階術後論理をサポートするように拡張された
麻友「えっ、一階述語論理よね」
若菜「お父さんは、いつもそう言ってる」
結弦「お父さんの目を釘付けにしようと、仕組んだかな? って、お父さんの妄想癖が、伝染っちゃった」
麻友「とにかく、太郎さんは、その項目を、丁寧に読んだのね」
私「うん。読んでみると、私が、『1から始める数学』というブログでやろうとしていた、14個の推論規則と24個の公理だけで、全部導く、というようなことを、『今回はこの公理から証明できるか、やってみて』というように、Mathematica に入力すると、証明できる場合、証明の全ステップを、書き上げてくれるところまで、進歩したようだ」
若菜「えっ、じゃあ、人間がやること、なくなっちゃったじゃないですか」
私「それは、早合点で、一般的な述語算(一階の述語論理は、そのひとつ)は、決定可能ではない(有限の時間で、正しいか正しくないか、決定できない問題があり、決定できない)という定理があり、Mathematica も、もちろんそれから、免れられない」
結弦「とんでもない、定理があるんだねえ。どこで、読んだの?」
私「いつもの、安井邦夫『現代論理学』(世界思想社)
の、最後の定理なんだ」
麻友「この本で、証明が完全でない定理は、第二不完全性定理と、チャーチのテーゼだけ。このふたつとの関係は?」
私「両方、利用している」
麻友「将来、覆る可能性も?」
私「それは、ないでしょう。さすがに。ただ、CPUが、桁外れに速くなってるし、メモリも大きくなってるから、大抵の問題なら、証明できる(この場合、正しい)か、こんなにやっても証明できない(限りなく、正しくなさそう)という判定が、できるようになるだろうね」
結弦「そうか。公理を入れ換えるたびに、ブルバキ、書き換えていたら、やってられないけど、『この公理で』って、その場で、指定できるのか。恐ろしい~」
若菜「ブルバキの新しい訳本が出ないのは、こういうことを、踏まえていたのかも知れませんね」
私「ブルバキのメンバーのひとりが、『戦いは終わったのです』と言っていたが、もう、ブルバキを、コンピューターが、越えたんだな。その人は、コンピューターに負けたことを、言ったのではなかったけど」
麻友「その言葉は、どこで読んだの?」
私「次の本に書いてあった」
モーリス・マシャル『ブルバキ──数学者達の秘密結社』(丸善)
結弦「どうりで、ブルバキに詳しいわけだね」
私「そういうわけで、このブログも、目標を少し変えようと思う」
若菜「どこかで、『1から始める数学』って、言ってましたけど、どこを起点にしても、理論展開できる数学に、脱皮させる必要がありますね」
私「おいおい。お前達に、そんな、難題を、押しつける気は、ないぞ」
若菜「でも、少なくとも、お父さんは、圏論を使うのか、Mathematica を使うのか、は、知りませんけど、やろうとしているのでしょう?」
私「まず、ブルバキ流の古い集合論は、飛ばして、代数に入ろうかと考え始めている」
結弦「今までのは、無駄?」
私「そんなことないよ。ブルバキというものが、どんな風に始まるかも、見せたし、他で見られない、序文の訳文を、スキャンした。助かった人も多いと、期待している(『数学原論(その15)』の記事参照)」
麻友「その代数というのも、論理で、ギチギチ書いてあるの?」
私「そうなんだろうなと、私も今日まで思っていたんだけど、読んでみると、確かに論理的に不備な記述はないけど、厳密すぎるというほどではない。訳者が頑張ったのかも知れないけど、数学の普通の本だ」
結弦「じゃあ、僕たちも、読めない?」
麻友「しまった。先に言われてしまった」
若菜「お母さん、証明は、嫌だったんですよね」
私「まあ、ほとんど完全に、フランス語で読んでいるみたいに、違う遊星に紛れ込んだみたいに、なるだろうけど、大学の理学部の数学科って、こんななのね、と、ちょっと触れるのも、悪くはないだろう」
麻友「太郎さん、その難しい本の読み方、数学の動画で、リアルで、見せられない?」
私「絵の先生で、普通の画家は、奥義を盗まれちゃうから、完全な描き方まで見せてくれないんだけど、その先生は、絵の具の溶き方から何から全部見せてくれるらしくて、母が喜んでいた。私は、そこまで出来るかどうか、分からないけど、技を盗まれるのは、全然恐くない。やりましょう」
麻友「明日は、新聞買いに行くんでしょ。もう寝たら?」
私「じゃあ、若菜、結弦も、代数からにしちゃって、いいな?」
若菜「集合論1、集合論2、集合論3、と、3冊抜き去り。特急ね」
結弦「集合論 要約 っていうのも、飛ばすんだよ。超特急だ」
私「じゃあ、解散」
若菜・結弦「おやすみなさーい」
麻友「おやすみ」
私「おやすみ」
現在2020年5月15日22時00分である。おしまい。