現在2021年1月8日21時35分である。(この投稿は、ほぼ3508文字)
麻友「今日は、時間があったのでは、ないの?」
私「今朝は、12時54分に起きた。マックへ行き、『集合と位相』を、進めた。家へ帰って、ダウンロードできていない、ブルバキの『代数10』の Kindle のことを、問い合わせた。しかし、向こうも困り果てて、調査して、後でメールで報告しますとのことだった」
麻友「まだ、ダウンロードできてないの?」
私「今までダウンロードしたもの、全部クリアして、改めて、ダウンロードすることまでしているのに、駄目なんだ。私が見たところ、フランス語の辞書がダウンロードされていないのが、原因のようなんだけどね」
若菜「返却するというのは?」
私「スマホには、ダウンロードできているから、クーリングオフは、できない」
結弦「困ったね」
麻友「この題は?」
私「去年最終回で、ブルバキの最後の論理の公理S4.を、 で、証明すると言いながら、証明しなかった。さらに、直観主義論理では、二重否定が、使えないから、証明できないと言ったのも、そのままにしてしまった。この積み残しをやろう」
若菜「本格的にやるのですか?」
私「うん。まず、排中律、 は、証明したな。
これは、覚えておく。
さて、
の演繹図で、最後の結論は、ブルバキのS4.そのものだ。そして、すべての仮定が落ちている」
若菜「排中律とあるところは?」
私「本来なら、全部の証明を書いて、完成した演繹図になるが、毎回分かりきったことを書くのは、スペースが無駄だ。だから、排中律の仮定が、全部落ちていることを確認した上で、他の証明に用いることを許すことで、無駄なスペースを減らすことにする」
麻友「ひとつ気になっているのよ。太郎さんは、仮定を置いて、推論を進めていって、先の方で、いくつもある仮定をどんどん落としていく。でも、ここでは、この仮定を落とすべきだ。というのは、どうして分かるの?」
私「それは、聞きたくてうずうずしていただろう。実は、これは、目標の定理を、証明しようと思っていると、結構分かるんだ。慣れることが、大切だけど、そのためには、正しい演繹図を、最低でも3回くらいは、写してみた方が、良い」
結弦「それで、二重否定は?」
私「S4.を証明するのに、排中律を使った。排中律の証明に、二重否定を使った。だから、S4.を証明するには、二重否定が、必要なんだ」
若菜「そうすると、直観主義論理では、ブルバキの論理の公理を、証明できませんね」
私「その通りだ。直観主義論理は、ブルバキより弱い。ブルバキより弱い、直観主義論理で、どこまで行かれるのか、興味もあったけど、もっと、たくさんの美しい花々を、愛でたいと、思う気持ちもある。数学基礎論で、後やり残しているのは、コーエンのフォーシング、ルベーグ可測関数について、ゲーデルの第2不完全性定理、自然数論の無矛盾性、解析学の無矛盾性、BGとZFの集合に関しての同値性、などだが、いつまでも数学基礎論をやっていても、何も始まらないからね」
麻友「太郎さんは、これが難しいというのを、聞くと、知りたくなるのよね。でも、1番やりたいことを、やったらいいと、思うわ」
私「ありがとう。ガロア理論もやりたいことなんだ」
若菜「じゃあ、明日は、ガロア再開してください」
私「分かった」
若菜・結弦「おやすみなさーい」
麻友「おやすみ」
私「おやすみ」
現在2021年1月9日0時38分である。おしまい。