現在2020年12月24日20時21分である。
私「メリークリスマス。麻友さん」
麻友「メリークリスマス、太郎さん」
私「今日は、ふたりで過ごそうよ。子供達は呼ばずに」
麻友「太郎さん。ひとつ提案があるの。今、新型コロナウイルスの影響で、知らない人と、しゃべることを、極度に制限されているじゃない」
私「確かにそうだけど」
麻友「だから、最初のデートは、オンラインで、やらない?」
私「デート、つまり、date は、日付と時間を決めて会うから、date なんだけど、オンラインでも、会っている気分になるの?」
麻友「私達は、模範的な恋愛をするのよ。コロナ禍で、男女がどうやってデートをするべきか、示せなくて、どうするのよ」
私「そうすると、Skype で、チャットか、Zoom を使うのかな?」
麻友「太郎さん。小林りんさんの、Hatch Edu で、初めて、Zoom 使ったけど、回線が、3G LTE とかで、全然動画にならなかったと、言ってたわね。この間の、『朝物理』は、どうだったの?」
私「一応、動画にはなった。だけど、ちょっと不安定だったけれどもね」
麻友「太郎さん。Zoom のこととか、全然、勉強してないでしょ。自分から、誰かを、Zoom に呼ぶとか、できないんじゃない?」
私「確かにそれは、無理かも」
麻友「『無理かも』じゃなくて、勉強しなさいよ。私とデートするためだったら、本気になるんじゃない?」
私「ちょっと、時間を、1週間ほど、ちょうだい。勉強してみる」
麻友「いつもながら、素直なのは、美徳よね」
私「クリスマスイヴだって、数学進めるよ」
麻友「数学の推論で、『』だけが、まだ推論のパターンを、見つけてなかった」
私「まず、『 導入』とか言わず、私が、『準背理法(じゅんはいりほう)』と呼んでいる、
が、ある。これがほぼ、『』の定義みたいなものだな」
麻友「 が、成り立つならば、矛盾が生じるとき、
は、成り立たないとして良いということね。それ以外にも、『
』 を規定するものが、あるの?」
私「ある。『 除去』とか言わず、私が、『片方否定』と呼んでいる次の推論がある
だ」
麻友「 または、
のどちらかが、成り立っていて、そのうちの、
が、成り立たないことが、分かったら、当然、
のほうが、成り立つでしょうと。あれっ、でも、直観主義論理では、成り立つ、成り立たないでなく、それを、確認する方法を、持ってる、じゃ、なかった?」
私「直観主義論理は、取り敢えず置いといて、古典論理を、究める」
麻友「あらそうなの。じゃあ、真偽表が、使えるのね」
私「厳密には、真偽表は、意味を知るのには分かり易いけど、この一連の推論パターンによって、論理記号の使い方を定めるだけで、真偽表に書かれている真偽と同じようなものが、導かれるようになっている。そういう意味で、形式的な、構文論と、真偽表などで意味を考える、意味論
が、同値であるという論理学の定理が、『現代論理学』においても、証明されている」
安井邦夫(やすい くにお)『現代論理学』(世界思想社)
麻友「太郎さんは、推論のパターンは、13個だと言っていた。『 導入』『
除去』『
除去』『
導入-仮定除去』『
導入』『
除去』まで、昨日やって、今日、『準背理法』と、『片方否定』をやって、8個まで、来た。後の5個は?」
私「残りの5つのうち、4つは、ときどき出てきた、『任意の』という意味の『』と、存在するという意味の『
』という記号の、導入と、除去の推論パターンが、それぞれ1つずつ有って、それで、4つなんだ。だけど、麻友さんはまだ、『
』と『
』を勉強するには、数学の経験が、乏しすぎる。このエニとイグジストの出て来る論理学を、述語論理学というのだけ、今日は覚えていって欲しい」
麻友「今までのは?」
私「命題論理学というんだ」
麻友「命題論理学か。それで、残りの5つの、最後の1個は?」
私「そこが、ハイライトなんだ。まず古典論理では、『』 の最後の性質は、『二重否定』と、私が呼んでいる、
という推論なんだ」
麻友「否定の否定は、肯定ね。当然、否定の記号は、そういう性質を持っていなければね」
私「ところで、私がやっと理解し始めた、直観主義論理では、これは、成り立たない」
麻友「どうするの?」
私「先日、リンク集の中の、NKsummary.pdf に間違いがあったと言ったけど、ここで、修正を宣言しよう。以後、あのファイルは、書き換える」
麻友「どの部分?」
私「最後のところだけど、ちょっと長いよ。もうすでに、少し改訂したけど、
++++++++++++++++++++++++++++++++++
直観主義論理とは
章の冒頭で、否定の否定が、肯定にならないという論理があると、書いた。それが、直観主義論理というものを用いた、構成的数学と呼ばれるものを築くとき、役に立つとも書いた。
本章を読んできて、私達の論理(それは、古典論理と呼ばれる) (エヌケーまたは、ドイツ語式に、エヌカーと呼ばれる)と、直観主義論理
(エヌジェイまたは、ドイツ語式に、エヌヨットと呼ばれる) とは、何が違うのだろうと、知りたい人もあるだろう。
そもそも、なぜ否定の否定が肯定にならないのか?
それは、私達のいう での命題は、真(正しい)か、偽(正しくない)かが、定まるものであったのに対し、直観主義論理では、『Aが正しい』とは、『Aを確認する方法をもっている』ということなのである。
と
での推論図の違いは、二重否定の推論、
*******************************
定義(推論図IX.二重否定)(にじゅうひてい)
否定の否定は、肯定であるということである。
*******************************
を、
*******************************
定義(推論図NJ-IX.否定除去)(ひていじょきょ)
の否定が成り立つ、つまり
が成り立たないことを確認する方法を持っているということは、
がもし成り立つことが証明されるならば、それから矛盾が導けるという推論である。
*******************************
に、置き換えることである。
これは、強い推論のように見えるが、実は、直観主義論理では、『』自体が、『
』 と定義されているので、何も言っていないのと、同じなのである。だから、我が
は
で証明できることを、すべて証明できる。逆に、
で証明できて
で証明できないことは、ある。例えば、二重否定を使って証明した、背理法とか、排中律などである。
二重否定推論自体を、他の12個の推論図を組み合わせて表せない以上、 は、
より弱いのである。本当に弱いのかは、推論図を組み合わせることを、何通りか試せば、分かってくることである。
+++++++++++++++++++++++++++
ここまでのなかで、麻友さん達に、否定の記号の定義に否定の記号を使っていて、循環論法だと、指摘された。
定義(推論図NJ-IX.否定除去)(ひていじょきょ)
の否定が成り立つ、つまり
が成り立たないことを確認する方法を持っているということは、
がもし成り立つことが証明されるならば、それから矛盾が導けるという推論である。
の、ところだ。『』 が、
だと言っている。『
』を使わずに定義しなければならないよね。そこで、考えたんだけど、
という矛盾でなく、任意の、
にしてしまったらってね」
麻友「そうすると、どうなるの?」
定義(推論図NJ-IX.否定除去)(ひていじょきょ)
となる」
麻友「それで、上手く行くの?」
私「今のところ、問題は、見つかってない」
麻友「太郎さん。面白い話だけど、もう23時28分よ。寝た方がいいわ」
私「直観主義論理の話、かなり長くなってるね」
麻友「それじゃ、2人だけのクリスマスイヴだったわね。おやすみ」
私「おやすみ」
現在2020年12月24日23時32分である。おしまい。