現在２０２０年１１月２５日６時１７分である。（この投稿は、ほぼ５３６１文字）
麻友「昨日の投稿は、何？ ほとんど、数学と関係ないじゃない」
私「もっと、書くつもりだったんだ。でも、眠くなっちゃって、寝るしかなかったんだ」
若菜「よく眠れたんですか？」
私「２２時４０分頃から、５時９分まで、グッスリ眠った」
結弦「お父さんに取って、あそこまで、スカッと書くと、発散できるのかもな」
麻友「数学始めなさいよ」
私「昨日、『リンク集の中の『ＮＫとＢＧの要約』の中の、NKsummary.PDF の中に書いてあったことに、間違いがあったことに気付いたんだ』と、書いた。私が、間違っていたのだが、あのＮＫの要約で、ＮＫ（古典論理）の説明は、間違っていないことに、今朝気付いた。間違っていたのは、私が最後に書いた、ＮＪ（直観主義論理）の概略の説明だった」
若菜「ＮＫとか、ＮＪと、言われても・・・」
私「そう言うだろうと思って、今朝、５時半頃から、バナナ１本食べただけで、この記事書き始めた。今日は、とことん書くぞ。ちゃんと、付いて来いよ」
結弦「本当に、ＮＫとＮＪ、説明する気？」
私「ああ、そうだとも」
麻友「太郎さん。その熱意は有り難いけど、朝食は、食べた方がいいわ。何か、冷蔵庫にないの？」
私「冷凍庫に、冷凍の『揚げなすの入った牛挽肉のボロネーゼ』って、ある」
麻友「６分くらいで、食べられるんでしょ。レンジでチンしなさいよ」
私「分かった。じゃあ、６分３０秒レンジにかけてみる」
麻友「本当に、無理するんだから」
私「ありがとう。未来のお嫁さん」
若菜「それで、直観主義論理は？」
私「まず、『数学を悟ってみて（その２）』で、一応、直観主義論理での、 は、定義してあった。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
は、『
を確認する方法が与えられたときに、その方法をもとにして、
を確認する方法を作る方法を持っている』と、定義される。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
（『数学を悟ってみて（その２）』より）
とある。そこで、これを利用して、説明しようとして、
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
麻友「竹内さんの『直観主義的集合論』には、どう書いてあるの？」
私「これには、
竹内外史（たけうち がいし）『直観主義的集合論』（紀伊國屋書店）
- 作者:竹内 外史
- メディア: 単行本
『 で矛盾を表わすことにして
は
の略と考えることにします．即ち
は“
を確認する方法があたえられればその方法をもとにして矛盾を導く方法をもっている”ということになります．』
と、p. vi に、書いてある」
麻友「ということは、矛盾という記号を、新しく、加えなければ、ならないんじゃない？」
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
（『数学を悟ってみて（その２）』より
という迷路に、迷い込んだ」
若菜「迷路だったんですか？」
私「竹内外史さんが、矛盾、矛盾と、言ってるけど、矛盾の定義って何だ？」
結弦「だって、『これとこれは、矛盾する』って、日常用語じゃない」
私「それでは、論理学で、矛盾を定義できてない」
若菜「そうすると、あのとき、お父さんが持ち出した、 みたいに、ある命題と、その命題の否定が、どちらも、導けたとき、『矛盾が生じた』と言うのですか？」
私「おお、いい線いってる。少なくとも、古典論理では、それで、良かった」
麻友「まだ、ある？」
私「古典論理では、 は、真偽表で、定義されていたから、問題なかった。ところが、直観主義論理では、
『 は、『
を確認する方法が与えられれば、その方法をもとにして、矛盾を導く方法を持っている』
となるのだ」
結弦「どうして？」
私「直観主義論理では、真と、偽の他に、まだ分からない、みたいなものもあるから、真偽表が使えないんだ」
結弦「あっ、そうか。真偽表が使えないのに、どうやって数学やるの？」
私「だから、本質的に、新しい数学なんだよ。直観主義的集合論というのは」
麻友「でも、どうして、普通の数学も、ろくに知らない私達に、そんな新しい数学なんて、説明してみようと、思ったの？」
私「それは、今、目の前にある、数学だけ見ていても、分からなかったのが、一旦外国旅行でもして、全く違う数学に出会ったら、『あれっ、別の視点から見たら、これは、当たり前だ』ということが、あり得るからなんだよ」
麻友「そうすると、どういうものなの？ 直観主義論理って」
私「もう、手加減しない。『ＮＫとＢＧの要約』説明する。ＮＫでは、証明のための、推論のパターンを１３種類用意して、これ以外の証明法は、認めないとするんだ」
若菜「１３個か。結構少ない」
私「古典論理では、 という命題が真で、
という命題が真のとき、とにかく、
と、
を、書いちゃう。下の絵の上の段のように。そうして、『これに対して推論しますよ』という意味で、線を引く。そして、
が真で、
も真なら、
も、真だろうと、この推論の結論を、線の下に書く。これで、推論のパターンいっちょあがりだ」
結弦「他のは？」
「 という命題が真で、
という命題が真のとき、推論を進めて、
という命題も真だろうと、推論する」
麻友「なんか、分かってきた。だったら、こういうのどう？」
私「それ、どういう意味？」
麻友「 が、真だったら、
単独でも、真だろうと」
私「麻友さんが、特待生だと、認めたのは、間違いではなかった。それ、正しい」
結弦「えっ、だったら、こういうのもある？」
私「それどういう意味？」
結弦「 が、真だったら、
の方だって、単独で、真だろうと」
私「もう『 除去』まで、征服された」
結弦「かつ、じょきょって？」
私「ひとつひとつ、推論のパターンに、名前が付いているんだ」
麻友「じゃ、私のは？」
私「麻友さんのも、『 除去』だよ。やっていることは、『かつ』の記号『
』を、なくすことだからね」
若菜「じゃあ、ひとつ上のは、『 除去』（ ならば、じょきょ）ですか？」
私「その通り。良く分かった」
結弦「一番上のは、『』が、増えてるだけで、何も、減ってないけど」
私「そうだな。だから、『 導入』（かつ、どうにゅう）と呼ぶ」
麻友「そうすると、導入と除去が、ペアになってるのね。じゃあ、『 導入』も、あるはず」
私「そこへ、行く？」
麻友「いけない？」
私「『 導入』（ならば、どうにゅう）は、難しいんだよ。実は、『
導入-仮定除去』（ならば、どうにゅう、かてい、じょきょ）というものになるんだ」
麻友・若菜・結弦「仮定除去？」
私「仕方ない。やってみせよう」
私「まず、 を仮定して、推論していったとする。推論とは、あくまでも、上の『
導入』や『
除去』などを使うということだ」
私「そして、例えば、
と、推論したとすると、このとき、仮定として、 と
が、生きているというんだ。つまり、仮定として、
と
が真でないと、結論の
が、導けないんだ」
私「それで、ここが、一番難しいんだけど、この推論の下に、さらに線を引き、
次に、他のところと区別するために、番号を振って、例えば、 とかで、
さらに、例えば、 （『
ならば 『
かつ
』』） と、『
導入』するのであれば、
の中に、すでに、
を仮定するという意味が入っているので、この推論図の集まり、それを演繹図というのだけど、そこで、仮定の、
は、落ちたとして、次のように、除去するんだ」
私「さらに、どの推論で、この仮定を落としたかが、分かるように、今の場合、 を、落とした仮定の右肩に、括弧閉じを伴わせて、次のように、書くんだ」
私「これが、『 導入-仮定除去』（ならば、どうにゅう、かてい、じょきょ）という推論で、なぜ、
の中に、すでに、
を仮定するという意味が入っているので、仮定から落として良いのか、私は大学２回生のとき、なかなかなじめなかった」
麻友「私も、疑問だわ。どうして、そうしていいの？」
私「 を導くのには、
が、必要だけど、
を、導くのには、
は、必要ないということなんだよね。これは、これだけ考えていても、多分分からない。数学の命題を、もっと証明してみて、・・・」
若菜「数学の命題って？」
私「例えば、 でも、『正三角形なら、二等辺三角形』でも、色々あるでしょ。それを、証明しているうちに、『これは、最後の結論のための仮定として、残しておく必要ないな』と、分かるようになる」
麻友「もう、１３時３０分なのに、お昼も食べてないんでしょ。マックへでも、行ってらっしゃい」
私「じゃあ、未来のお嫁さんの忠告に従うよ。バイバイ」
若菜・結弦「バイバイ」
麻友「気を付けてね」
現在２０２０年１１月２５日１３時３３分である。おしまい。
