現在2020年12月26日19時53分である。(この投稿は、ほぼ2916文字)
麻友「とうとう、本年200個目の投稿ね」
私「今日は、新聞買いに言ったのと、母に新聞届けた以外、ほとんど数学やってた」
若菜「何時に起きたんですか?」
私「4時21分に起きて、眠れないので、昨日のブルバキの最後のS4.を、証明しようとしていた」
麻友「早く起きすぎじゃない?」
私「8時頃から、眠くなりだして、8時49分から11時34分まで、昼寝した」
結弦「3時間寝れば、確かに十分だね。昨日23時頃から4時21分まで、5時間寝ているのだものね」
私「8時間睡眠は、私に取っては、必ずしも十分ではない。だが、今日は、比較的、時間を、有効に生かせた」
麻友「昨日、直観主義論理の話が、ちょっと出てきたけど、どうして『二重否定』推論が、使えないのか、いつもの太郎さんの冴えた講義を、聞きたいわ」
私「ちょっと、振り返ってみよう。古典論理で、『 は正しい』と言ってた部分を、『 を確認する方法を持っている』と、したのだったね」
若菜「それで、『』は、『 を確認する方法と、 を確認する方法を、両方持っている』とした」
結弦「一方、『』は、『 を確認する方法と、 を確認する方法の、少なくとも一方を持っている』とした」
麻友「そして、『』は、『 を確認する方法が与えられたときに、その方法をもとにして、 を確認する方法を作る方法を持っている』とした。そして、残ったのが、『』だった」
私「『』に関し、『』は、『 を確認する方法が与えられれば、その方法をもとにして矛盾を導く方法を持っている』と、『直観主義的集合論』には、書いてある。でも、矛盾とは、ある命題と、その否定の命題の、どちらもが、導かれることであり、そもそも、否定の命題というものの定義をしようとしているのに、その定義に、否定というものが、顔を出し、循環論法だと、困った。その迷路から脱するため、私は、『』は、『 を確認する方法が与えられれば、その方法をもとにしてあらゆることを導く方法を作る方法を持っている』と、定義すべきだと考えた」
麻友「少し、進歩してるわね」
私「伊達に、ノート、消費しているわけではない」
若菜「問題の、『』のところを、重点的に、説明お願いします」
私「まず、直観主義論理での、『』の定義を表す、『否定除去』という推論、
が、新たに加わる。一方、古典論理で使われていた、『二重否定』は、使えなくなる」
結弦「どうして?」
私「これは、ちょっと、準備が必要。まず、『二重否定』が、使えると、後で証明するように、『排中律』が、証明できる。式で書くと、
『二重否定』
が、あると、『排中律』、
が、証明できてしまう」
結弦「証明できたって、いいじゃん」
私「直観主義論理での、
って、どういうことだった?」
若菜「『 を確認する方法と、 を確認する方法の、少なくとも一方を持っている』でした」
私「『』は、なんだった?」
若菜「『 を確認する方法が与えられれば、その方法をもとにしてあらゆることを導く方法を作る方法を持っている』でした。そうすると、結局、『 でない』という場合のことが、よく分かりませんね。 は、 の場合のことしか、言ってませんから」
私「そうなんだ。 というものが、良く分からない。だが、こういう場合、意味を考えず、式の形で、推論する、構文論の立場というものがある。これを、用いて、 のことを、
『否定除去』
と、定義するのだった。 を、定義で定めるものに、使っていないことに、注意して欲しい」
麻友「太郎さん。推論図を並べる順番に、頭を使っているのね」
私「そうだよ。そして、こう定義された、 について、『準背理法(じゅんはいりほう)』と呼んでいる、
『準背理法』
が、ある」
若菜「 を確認する方法が与えられたときに、その方法をもとにして を確認する方法を持っている、ですが、 ということは、まず、 が確認できてますし、 ということは、(否定除去推論より、好きな について でしたから)好きな について、 が、成り立つということです。だから、 を確認する方法が与えられたときに、その方法をもとにして、なんでも確認できる。これは、まさに、 そのものですね」
結弦「最後は、『片方否定』だけど」
『片方否定』
私「今日は、疲れた。もう寝る前の薬も飲んだ。『二重否定』から、『排中律』が証明できること。『片方否定』が、直観主義論理でも、妥当な推論であることは、明日以降に、伸ばさせてくれ」
若菜「今日の話は、結構お父さんの本音が聞けて、面白かったです」
麻友「そういう本音を聞きたいのよね」
結弦「じゃあ、おやすみ」
若菜「おやすみ」
麻友「おやすみ」
私「おやすみ」
現在2020年12月26日21時53分である。おしまい。