現在2021年1月13日18時41分である。(この投稿は、ほぼ5451文字)
麻友「太郎さんは、私が優しくしてあげないから、お母様や妹さんが、お誕生日を祝ってくれたのね」
若菜「どんな、誕生日プレゼントだったのですか?」
結弦「なんか、相当値が張ったみたいだな」
私「これなんだ」
若菜「えっ、お母さんの、Quoカード?」
麻友「違うでしょ。あっ、この手帳」
私「2段目の写真で分かるように、診断書などの、A4の紙を、折らずに入れられる、A5サイズの手帳なんだ」
麻友「こういう手帳か。そういえば、太郎さん。手帳、頻繁に使ってたわね。どうして、新しいものが、欲しかったの?」
私「今、出納帳、遡ったら、1999年度に妹が、ヤザキでもらった手帳を、ずっと使ってた。だけど、留め具が、切れてしまったので、2007年3月7日に、18,900円で、今まで使っていた、この手帳を、自分で買った」
若菜「お父さん、その手帳も、随分高い。それが、欲しい理由もあったの?」
私「この古い方ね。ほとんど、非の打ち所のない手帳なんだよ。閉じるためのチャックが壊れなければ、今でも、使っていたいくらい」
麻友「太郎さんが、それを修理するのではなく、新しい手帳を、欲しがったのは、理由があったんでしょう」
私「これが、壊れちゃったのは、麻友さんに会う、4年くらい前、とらいむに行っていた、2011年頃、だったと思う。チャックが、スムーズに動かないので、CRC KURE5ー56 という潤滑油を注したら、チャックが完全に、バラバラになってしまって、閉じなくなっちゃったんだ。チャックには、油を注してはいけないのだと、そのとき知った。さて、修理するか、新しいのにするかと、有隣堂、ロフト、東急ハンズ、を、見ていたとき、A5サイズの手帳を開いたとき、『ここに、A4の紙を、折らずに入れられます』と書いてある手帳を、見つけたんだ」
KURE(呉工業) 5-56 (320ml) 多用途・多機能防錆・潤滑剤 [ 品番 ] 1004
- メディア: Automotive
麻友「若菜。試験とかのプリント、折るの抵抗ある?」
若菜「毎日たくさんもらうから、当然折りますよね」
結弦「今、お父さんのお母さん。つまり、お婆ちゃんに聞いてきた。お父さんが、小学校5年生のとき、プリントを折らずに済む、プラスチックの2重の下敷きを、買ってあげると言ったら、妹さんは、B5の紙が入る、普通の下敷きを、買ったのに、お父さんは、B4の紙も、折らずに入れられる、おっきな下敷きを欲しがって、ランドセルにも入らないのに、その二重の下敷き、ずっと学校へ持って行ってたんだって。でも、それで、プリントを運んだことは、なかったと、お婆ちゃんが言ってた」
麻友「あっ、はっ、はっ、そうなのよ。それが、太郎さんなのよ。私の卒業コンサートにも、今後私に会えなくなるファンが、ひとりでも多く、私の姿が観られるように、と言って、チケット取らなかったり、私と結婚したら、2重になるからと、『Best Regards! 』のソロアルバム、買わなかったりと、考えすぎなのよね。本当に、そのA4のための袋、使うかどうか、見てましょ」
若菜「これ、中身だけで、1,200円ということですかね」
麻友「えっ、太郎さん。今までは、いくらだったの?」
私「毎年変わるんだけど、去年は、B6のは、税抜き800円だった」
麻友「それで、手帳自体は、幾らだったのかしら?」
私「税抜き16,500円。税込み18,150円だよ」
若菜「プレゼントあげる方も、大変ですね」
麻友「太郎さんのお母様や、妹さんは、私がどう出るか、待ってたんだと思う」
若菜「お母さんが、誕生日プレゼントあげるんじゃないかって?」
麻友「でも、私は、何もあげなかった。クリスマスにも」
結弦「お母さん、引退してから、7カ月経ったね。あくまでも、自然淘汰で、ひとりになるのを、待っているの?」
麻友「私は、太郎さんが、お金を稼げるようになるか、或いは、本当にお金というもののない、社会にしてくれるのを、待っているのよ」
若菜「本当ですか? 確かに、AIは、どんどん普及しますし、人間の仕事は、どんどん減って、6年後までには、あっ、いや、もう5年後ですが、5年後には、人間は全員、労働から、解放されます。でも、そうなっちゃったら、お母さん、お父さんじゃなくても良くなるんじゃ、ないですか?」
私「麻友さんを、少しビックリさせた方が、良いのかな? 今日の題の、NJ(直観主義論理)の書き直しの話をしよう」
麻友「どう書きなおすの?」
私「思いの外、苦労した」
麻友「どこで?」
私「古典論理でも、
が、成り立つことの証明で」
麻友「聞いてみたいわね」
私「じゃあ、もう21時14分だから、眠くなったところで、おしまいと言うことで、書き直し、進めていってみよう」
直観主義論理とは
章の冒頭で、否定の否定が、肯定にならないという論理があると、書いた。それが、直観主義論理というものを用いた、構成的数学と呼ばれるものを築くとき、役に立つとも書いた。
本章を読んできて、私達の論理(それは、古典論理と呼ばれる) と、直観主義論理 (エヌジェイまたは、エヌヨットと呼ばれる) とは、何が違うのだろうと、知りたい人もあるだろう。
そもそも、なぜ否定の否定が肯定にならないのか?
それは、私達のいう での命題は、真(正しい)か、偽(正しくない)かが、定まるものであったのに対し、直観主義論理では、『が正しい』とは、『を確認する方法をもっている』ということなのである。つまり、『 が正しい』とは、に至る での演繹図を、持っているということなのである。
と での推論図の違いは、二重否定の推論、
*******************************
定義(推論図IX.二重否定)(にじゅうひてい)
否定の否定は、肯定であるということである。
*******************************
を、
*******************************
定義(推論図NJ-IX.否定除去)(ひていじょきょ)
の否定が成り立つ、つまり が成り立たないことを確認する方法を持っているということは、 がもし成り立つことが確認されるならば、直ちに矛盾が生じ、それからあらゆる命題が導けるという推論である。
*******************************
に、置き換えることである。
これは、強い推論のように見えるが、実は、直観主義論理では、『』自体が、『 が確認されるならば、矛盾が導かれる』 と定義されているので、何も言っていないのと、同じなのである。そして、この推論図は、 で証明できる。だから、我が は で証明できることを、すべて証明できる。逆に、 で証明できて で証明できないことは、ある。例えば、二重否定を使って証明した、背理法とか、排中律などである。
二重否定推論自体を、他の 個の推論図を組み合わせて表せない以上、 は、 より弱いのである。本当に弱いのかは、推論図を組み合わせることを、何通りか試せば、分かってくることである。
ところで、
が、 で、証明できることの証明は、それほど易しくないので、以下に証明しておこう。
まず、方針を示す。
(1)以下の つの論理式は、 の定理である(つまり、仮定のすべてが落ちている、演繹図の結論になっている)ことを、証明する。
(2)次に、そのことを仮定した上で、以下の論理式、
が、 の定理であることを、証明する。
(3)最後に、 の定理となった、 を用いて、
の定理
と、なるので、 の定理は、仮定がすべて落ちている演繹図の結論であるから、
が、証明されたことになる。
以上の方針の元に、(1)から、始めるが、今晩は、(1)、(2)、は、証明を諦めよう。
ただ、どうして、(1)、(2)、を、思い付いたか、書いておこう。
私は、最初、古典論理で、
が、成り立つことを証明するのは、簡単だろうと思っていた。だが、無駄な試みを、5分ほどした後、これは、無理だと気付いた。そこで、いつもの『現代論理学』を、開いた。
を、証明しているところはないか?
あった!
32ページに、
③
というのが、あった。本当は、テキストでは、
③
となっていたが、私の記法に読み替えると、上のようになる。 は、証明できるという記号である。
ここに出ていた証明で、 と、 を用いて、
を、証明できたのである。
眠くなってきたので、ここまでにしようか?」
麻友「太郎さん、文献、やっぱり必要なのね」
私「100冊くらいは持っていないと、研究にならない。実際には私は、300冊くらいは、持っている」
若菜「良い夢を見てください」
私「そうだね」
若菜・結弦「おやすみなさーい」
麻友「おやすみ」
私「おやすみ」
現在2021年1月13日22時38分である。おしまい。