現在２０２１年４月１８日１９時４０分である。（この投稿は、ほぼ２４１３文字）
麻友「また、古い話を」
私「機会を逸して、書けずにいたんだ」
若菜「ＮＪ（エヌ・ヨット）でしたね。覚えていますよ」
私「このＪとかＩとか、ＮＫとかＬＫなんだけどもね、ずっと、
ＮＫは、ドイツ語の natürlicher Kalkül の頭文字で、
ＬＫは、ドイツ語の logistischer Kalkül の頭文字だと、信じ込んでいたんだ。
ところが、研究が進んで、とうとう『証明論』に、手を出した」
結弦「お父さんの蔵書に、『証明論』なんていう本は、ないよ」
G. Takeuti : Proof Theory
Proof Theory: Second Edition (Dover Books on Mathematics)
- 作者:Takeuti, Gaisi
- 発売日: 2013/02/20
- メディア: ペーパーバック
私「これだよ」
若菜「それは、かなりレヴェルが高いのでは？」
私「それは、分かっている。でも、高階論理におけるカット消去定理を示し、結果として実数論（解析学）の無矛盾性を導いている本は、なかなか見つからないんだ」
麻友「いつ、それを読もうと、考えているの？」
私「これは、完全にヲタクの世界だから、ブルバキが終わってからで、良いのではないかと、思ってる」
結弦「ブルバキだって、ヲタクみたいだけどな」
私「それは、読んでからのお楽しみだ」
若菜「『ＮＪについての書き直し』の５回目なんですから、終わらせましょう」
私「前回、
(1)以下の つの論理式は、
の定理である(つまり、仮定のすべてが落ちている、演繹図の結論になっている)ことを、証明する。
の つのうちの、
と、
を証明した」
結弦「じゃあ、 を証明して」
私「
と、が証明できた」
麻友「あー、ちゃんと、証明できるんだ」
私「本当は、『現代論理学』の２５ページから、否定の記号（『～』から、『』）とならばの記号（『
』 から、『
』）の書き換えをしただけで、丸写ししたんだ」
麻友「太郎さんでも、その程度か」
若菜「今日の最初に、ＮＫやＬＫが、何の略かという話が、ありましたが」
私「それがね、Proof Theory の第１ページを開いたら、
ＬＫ（ logistischer klassischer Kalkül ）
ＬＪ（ logistischer intuitionistischer Kalkül ）
と、書いてあるんだ。これを、受け入れると、ＬＫのＫも、ＮＫのＫも、Kalkül の頭文字じゃなくて、klassischer （古典）の頭文字だということになる。intuitionistischer (直観主義）は、花文字のＬＩが、ＬＪに化けたという話は、前したね」
若菜「そうすると、ＮＫとＮＪは？」
私「
ＮＫ（ natürlicher klassischer Kalkül ）
ＮＪ（ natürlicher intuitionistischer Kalkül ）
で、natürlicher は、比較的自然なという意味なんだ。ナチュラルということだよ」
麻友「太郎さんも、日々前進してるのね。それで、証明は全部終わったけど、纏めてくれない？」
私「そのつもりだったけど、もう、２１時３０分だ。しかも、明日通院だ。まとめは、次回にするよ」
若菜・結弦「じゃあ、おやすみ」
麻友「おやすみ」
私「おやすみ」
現在２０２１年４月１８日２１時３２分である。おしまい。
