現在２０２０年１２月２７日７時２０分である。（この投稿は、ほぼ３００５文字）
麻友「昨日は、たっぷり寝た？」
私「２２時頃、疲れ切って寝て、今朝３時２分に、目が覚めたけど、もう一度寝て、５時５０分に起きた」
麻友「８時間睡眠か。無理せず、昼寝してね」
私「うん」
結弦「『片方否定』の説明中だった。これ」
私「一晩寝て、良い考えが浮かんだ」
若菜「寝るだけで、アイディアが生まれるお父さんって、凄い」
私「まず、次のように考える。
『否定除去』
だったろ。この、 として、
を、選ぶ」
一方、一昨日若菜が示したように、
だから、・・・」
若菜「分かった。『 除去』だ。
『片方否定』
は、次のように、示せる」
麻友「一晩寝て、頭がスッキリしただけで、証明できちゃうなんて、うらまやしい」
私「特待生が何を言ってる。でも、これで、古典論理（）の一部と、直観主義論理（
）の一部を、完全に説明し終えた。後は、
と、
の推論図が、残っただけ」
若菜「ちょっと、待って下さい。『片方否定』が、他の８個の推論を組み合わせて、証明できるなら、この推論図は、いらないんじゃないですか？」
私「私も、今、それを、考えていた。本来、 や、
の推論図というときには、最低限必要なものだけを、採用するはずだ。そもそも、直観主義論理（
）では、古典論理 （
） より証明できることが減るはずだから、推論図も、９個から８個へ、減った方が、良いはずだよね」
若菜「お父さんの分かっていないことに、気付いた」
私「やっぱり、麻友さん達に説明していると、緊張感が違うから、普段なら気付かないようなことにも、気付く。直観主義論理では、古典論理の『二重否定』と『片方否定』を、『否定除去』で、置き換える。『準背理法』は、そのまま、温存することとする。NKsummary.pdf は、 に関しては、間違いまくりだなあ」
麻友「それだけ、直観主義論理の理解が、進んだということね」
麻友「今、寝てたの？」
私「うん。９時１１分から１２時２分まで、寝てた」
若菜「じゃあ、再開して下さい」
麻友「今、どこへ行ってたの？」
私「マックで、食べて、その後、上で書いたことを、チェックしていた」
麻友「どういう風に？」
私「若菜が、
『『片方否定』が、他の８個の推論を組み合わせて、証明できるなら、この推論図は、いらないんじゃないですか？』
と言って、私が、
『直観主義論理では、古典論理の『二重否定』と『片方否定』を、『否定除去』で、置き換える』
と言っているが、そんなことが、許されるかどうかの、チェックだよ」
麻友「かなり難航していたみたいだけど」
私「結論を言うと、『片方否定』は、省略できない。他の推論から、証明されたように見えるけど、
『片方否定』
自体が、証明できたわけではないことに、気付いた」
麻友「今日の、１３時２１分３０秒から、『麻友７２』のノートで、４３１１ページから４３１８ページまで、１９時３９分２０秒までかけて、推論を色々試している。これで、『片方否定』は、必要と、判断されたのね」
私「色々な推論を組み合わせて、証明できたというのと、この１カ所で、 と、
とから、
が、導けるというのは、同等でないと、分かったんだ」
麻友「そうすると、どうなるの？」
私「古典論理にしても、直観主義論理にしても、推論の数は、９個のままだ、ということだ」
若菜「８個でいい、というのは、勇み足でしたね」
結弦「結局、古典論理にあった、
『二重否定』
を、
『否定除去』
に、置き換えたものが、直観主義論理なんだね。そして、『二重否定』があれば、証明できる、『排中律』が、『否定除去』では、証明できないんだね。だから、直観主義論理は、古典論理より、弱いというわけだね」
麻友「『弱い』というのは、どういうこと？」
結弦「直観主義論理で、証明できることは、すべて、古典論理で、証明できるけれど、反対の、古典論理で、証明できることの中に、直観主義論理で、証明できないことが、あるということだよ」
麻友「ああ、そういうことか」
若菜「『二重否定』が、あると、
『排中律』
が、証明できることは、明日以降、証明して下さい」
私「もちろん」
麻友「もう、２２時０７分になっている。今日は、ここまでに、しましょう」
私「こんなに、論理学ばっかりやってたのは、久し振りだ」
若菜・結弦「じゃあ、おやすみなさーい」
麻友「おやすみ」
私「おやすみ」
現在２０２０年１２月２７日２２時０９分である。おしまい。
