現在２０２０年１１月２０日２０時３２分である。
麻友「何か、不可能だったものが、可能になったの？」
私「いや、私が、可能にしたんじゃないんだ」
若菜「いつもの再発見ですか？」
私「いや、私は、何も発見してなくて、他の数学者達が、頑張った。という話なんだ」
結弦「どういうこと？」
私「説明するより、見せた方がいい。インターネットを『マセマティカで１階の述語論理』とググると、『機械による数学-researchmap』というのが、６番目にヒットする。ＰＤＦファイルをダウンロードすると、１ページ目は、これ。分からないだろうから、取り敢えず飛ばして、４ページを見る。
という図がある。原文を見たい人は、インターネット上にもあるし、私の文献フォルダにも、新井紀子著機械による数学というフォルダを作った」
麻友「それで、何が分かったの？」
私「『モーツァルト交響曲第３７番（その２）』の投稿で、次のようなやり取りを、したじゃない」
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
麻友「どんなこと？」
私「これ、『麻友』ノートに書けば、良かったな」
麻友「なんて書いてあるの？」
私「
２０１９．１０．３ ２１：５２
ブルバキを、 で。
って、書いてあるんだ。ミニストップのレシートの裏」
麻友「どういう意味なの？」
私「この間、『論理学をつくる』っていう本のレビューで、『自然演繹が標準的なGentzenの形でないのがとてもとても残念』というのがある、っていう話、したじゃない」
麻友「読んだ気がする」
私「あそこで言ってる、『標準的なGentzenの形』というのが、私が、リンク集の『ＮＫとＢＧの要約』にまとめた、ＮＫの方なんだ」
麻友「じゃあ、ＢＧの方が、残念な方？」
私「そうじゃなくてＢＧというのは、ＮＫを使って書いた、集合論の公理なんだ。ＢＧ（ベルナイス・ゲーデル）の集合論ね。ＮＫは、論理学の使い方のうち、１階述語論理の比較的自然な体系ＮＫ（natürlicher Kalkül)というものの頭文字なんだ。ドイツ語だから、エヌ・カーと読むのが正式と、次の本の１４３ページに書いてあったりする。でも、私は、普通に、エヌ・ケーと読んでいる」
- 作者:栄道, 久馬
- 発売日: 1995/09/25
- メディア: 単行本
麻友「それで、『ブルバキを、 で』というのは、何なの？」
私「ブルバキでは、証明を、フランス語で書いている。もちろん、訳本では、日本語で、書いてある。でも、これでは、ゲームを作るコンピューターに伝わらない。だけど、ＮＫだと使う記号は決まっていて、証明も機械的だから、数式をＮＫにまで、持ってくれば、コンピューターに、理解させられる。その橋渡しをすれば、後は、ゲームのデザインやストーリーに凝るだけだな、と思ったということなんだ」
麻友「太郎さん。この前教えてくれた、ウルフラムアルファって、日本語理解できるのよ」
私「えっ、そんなに、Ｍａｔｈｅｍａｔｉｃａ、進んでるの？ カチャカチャ」
麻友「太郎さんが、プログラミング言語を、学ばなかったから、時代遅れになっちゃったのよ」
私「ああ、小林りんさんに伝えたこと、全部実現してるんだ。今日、インドのルピーが、日本円でいくらに為替レートでなっているかまで、インターネットで検索して、教えてくれるんだ」
麻友「太郎さん。『数学』っていうゲーム、必要なのかしら？」
私「Ｍａｔｈｅｍａｔｉｃａの家庭バージョンが、４５，０００円なんだ。これを使って、ゲームをするのは、数学を味わうという意味では、面白いと思う。ただ、ある程度勉強した上で、Ｗｏｌｆｒａｍという言語で、何かが正しいということを、どうやって判定しているかは、チェックする必要があるよね」
麻友「計算機が、ウソをつくかも知れないというの？」
私「ウソっていうか、これ以上計算できないとなったとき、『分かりません』と答えた場合は、まあ良いとして、適当にそれっぽそうな数値を答えるようにプログラミングされてたりしたら、Ｍａｔｈｅｍａｔｉｃａ使う意味なくなっちゃうよね」
麻友「やっぱり『数学』っていうゲーム、作るの？」
私「そんなに、悲観することないよ。数学を、整然と書いてある冷たそうな本にだって、胸を打つ華麗な証明が書いてあることもある。数学が、勉強のしようによっては、すっごく楽しめるようなものになるのは、確かなんだ」
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
（『モーツァルト交響曲第３７番（その２）』より）
麻友「ああ、覚えている。でも、よく読むと、新井紀子さん、『仮説』って書いてる」
若菜「それに、お父さんの言う、ＢＧじゃないですし」
結弦「でも、ＺＦとＢＧは、集合論に関して、同じとか」
私「私が、一番ビックリしたのは、『ブルバキでは、証明を、フランス語で書いている。もちろん、訳本では、日本語で、書いてある。でも、これでは、ゲームを作るコンピューターに伝わらない。だけど、ＮＫだと使う記号は決まっていて、証明も機械的だから、数式をＮＫにまで、持ってくれば、コンピューターに、理解させられる。その橋渡しをすれば、後は、ゲームのデザインやストーリーに凝るだけだな、と思った』というところの、橋渡しが難しいだろうなと思っていたのが、もうほぼ完全にできているということなんだよ」
麻友「つまり、数学が、相当難しくても、電卓たたくように、機械的に解けちゃうのね？」
私「そういうことだよ」
若菜「そうだとすると、確かにお父さんが、『不可能を可能とする』というのは、達成されたのですね」
私「ただ、実は、『不可能を可能とする』は、『数Ⅲ方式ガロアの理論』の第１８章の、ルフィニが不完全な証明を発表した章の題名なんだ」
結弦「そして、第２０章、『不可能の証明を完成する』で、アーベルが、解く」
若菜「さらに、第２１章は、『方程式は生きている』ですものね。数学は、今も生きているんですよね」
麻友「太郎さん、眠そう。もう寝たら？」
私「おやすみ」
麻友・若菜・結弦「おやすみ」
現在２０２０年１１月２０日２２時１４分である。おしまい。
