ＮＪについての書き直し

　現在２０２１年１月１１日２１時０４分である。（この投稿は、ほぼ２５２５文字）

麻友「ガロアが、進まないわね」

私「申し訳ない。どうも、調子が良くならない。やっぱり、鬱なのかなあ。一方で、確かに、もの凄くなんでもできそうな、気分になっているときもあるからなあ」

結弦「今、新型コロナウイルスで、社会全体が、低迷している。辛いのは、お父さんだけじゃないよ」

若菜「それで、この題は、何ですか？」

私「リンク集の『ＮＫとＢＧの要約』というリンクの中の、『NKsummary.pdf』というファイルで、１階述語論理の比較的自然な体系（ＮＫ）の説明の最後に、１階述語論理の直観主義論理の体系（ＮＪ）というものの、紹介を書いた。これは、推論図をひとつ、入れ換えるだけだったのだが、麻友さんも、知っているように、否定の記号の定義に、否定の記号を使っていて、不備があることを、去年の暮れに指摘されて、訂正することにした。だが、ただ書きなおすと、前どうだったか分からなくなるので、記録を残すことにした。ちょっと長いが、問題の箇所を取り出す」

＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋

　　　　　　直観主義論理とは

章の冒頭で、否定の否定が、肯定にならないという論理があると、書いた。それが、直観主義論理というものを用いた、構成的数学と呼ばれるものを築くとき、役に立つとも書いた。

本章を読んできて、私達の論理（それは、古典論理と呼ばれる） と、直観主義論理 （エヌジェイと呼ばれる） とは、何が違うのだろうと、知りたい人もあるだろう。

そもそも、なぜ否定の否定が肯定にならないのか？

それは、私達のいう での命題は、真（正しい）か、偽（正しくない）かが、定まるものであったのに対し、直観主義論理では、『Aが正しい』とは、『Aを確認する方法をもっている』ということなのである。つまり、『Aが正しい』とは、Aに至る での演繹図を、持っているということなのである。

と での推論図の違いは、二重否定の推論、

＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

　　　　　定義(推論図IX.二重否定)(にじゅうひてい)

否定の否定は、肯定であるということである。

＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

を、

＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

　　　　定義(推論図NJ-IX.否定除去)(ひていじょきょ)

の否定が成り立つ、つまりが成り立たないことを確認する方法を持っているということは、がもし成り立つことが証明されるならば、それから矛盾が導けるという推論である。

＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

に、置き換えることである。

これは、強い推論のように見えるが、実は、直観主義論理では、『』自体が、『』 と定義されているので、何も言っていないのと、同じなのである。だから、我が は で証明できることを、すべて証明できる。逆に、 で証明できて で証明できないことは、ある。例えば、二重否定を使って証明した、背理法とか、排中律などである。

二重否定推論自体を、他の12個の推論図を組み合わせて表せない以上、 は、 より弱いのである。本当に弱いのかは、推論図を組み合わせることを、何通りか試せば、分かってくることである。

＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋＋

　いくつか、意味を、取り違えてしまっている部分があるが、今後の私達の数学を築いていく上で、いくつか方針変更をしよう。

　まず、以前も紹介した、

久馬栄道（きゅうま　えいどう）『Ｑ＆Ａ数学基礎論入門』（共立出版）

Q&A 数学基礎論入門

という本で、なぜ直観主義論理を、ＮＪというかについて、書かれている。本来直観主義論理は、”intuitionistic logic" である。ドイツ人のゲンツェンも、論文で、ＮＩとしていたようなのだが、ドイツ語の花文字で、Ｉは、『』、で、Ｊは、『』なので、ほとんど区別がつかないため、英語に翻訳されるときに、ＩがＪに化けたそうである。

　ＮＪは、ドイツ人のゲンツェンに敬意を表し、ドイツ語式に『エヌ・ヨット』と呼ぶそうである。

　私達も、『エヌ・ヨット』を、今後採用しよう。

　同様に、以後、ＮＫは、『エヌ・カー』に切り換えていこう。

　さて、上の切り出した部分をどう切り換えるかだが、もう、２２時５０分になってしまったので、先に延ばそう」

麻友「研究は、してるんだ」

私「少しずつはね」

若菜・結弦「じゃあ、おやすみなさーい」

麻友「おやすみ」

私「おやすみ」

　現在２０２１年１月１１日２２時５７分である。おしまい。