数学を悟ってみて（その２７） - 相対性理論を学びたい人のために

　現在２０２０年１２月２４日２０時２１分である。

私「メリークリスマス。麻友さん」

麻友「メリークリスマス、太郎さん」

私「今日は、ふたりで過ごそうよ。子供達は呼ばずに」

麻友「太郎さん。ひとつ提案があるの。今、新型コロナウイルスの影響で、知らない人と、しゃべることを、極度に制限されているじゃない」

私「確かにそうだけど」

麻友「だから、最初のデートは、オンラインで、やらない？」

私「デート、つまり、date は、日付と時間を決めて会うから、date なんだけど、オンラインでも、会っている気分になるの？」

麻友「私達は、模範的な恋愛をするのよ。コロナ禍で、男女がどうやってデートをするべきか、示せなくて、どうするのよ」

私「そうすると、Skype で、チャットか、Zoom を使うのかな？」

麻友「太郎さん。小林りんさんの、Hatch Edu で、初めて、Zoom 使ったけど、回線が、３G LTE とかで、全然動画にならなかったと、言ってたわね。この間の、『朝物理』は、どうだったの？」

私「一応、動画にはなった。だけど、ちょっと不安定だったけれどもね」

麻友「太郎さん。Zoom のこととか、全然、勉強してないでしょ。自分から、誰かを、Zoom に呼ぶとか、できないんじゃない？」

私「確かにそれは、無理かも」

麻友「『無理かも』じゃなくて、勉強しなさいよ。私とデートするためだったら、本気になるんじゃない？」

私「ちょっと、時間を、１週間ほど、ちょうだい。勉強してみる」

麻友「いつもながら、素直なのは、美徳よね」

私「クリスマスイヴだって、数学進めるよ」

麻友「数学の推論で、『 ${\neg}$ 』だけが、まだ推論のパターンを、見つけてなかった」

私「まず、『 ${\neg}$ 導入』とか言わず、私が、『準背理法（じゅんはいりほう）』と呼んでいる、

${A \Rightarrow ( B \wedge \neg B )\\ \rule{4.0cm}{0.3mm} \\ ~~~~~~\neg A\\ }$

が、ある。これがほぼ、『 ${\neg}$ 』の定義みたいなものだな」

麻友「 ${A}$ が、成り立つならば、矛盾が生じるとき、 ${A}$ は、成り立たないとして良いということね。それ以外にも、『 ${\neg}$ 』を規定するものが、あるの？」

私「ある。『 ${\neg}$ 除去』とか言わず、私が、『片方否定』と呼んでいる次の推論がある

${~~A \vee B ~~~~~~~\neg B \\ \rule{3.0cm}{0.3mm} \\ ~~~~~~~~~~~~~~A \\ }$

だ」

麻友「 ${A}$ または、 ${B}$ のどちらかが、成り立っていて、そのうちの、 ${B}$ が、成り立たないことが、分かったら、当然、 ${A}$ のほうが、成り立つでしょうと。あれっ、でも、直観主義論理では、成り立つ、成り立たないでなく、それを、確認する方法を、持ってる、じゃ、なかった？」

私「直観主義論理は、取り敢えず置いといて、古典論理を、究める」

麻友「あらそうなの。じゃあ、真偽表が、使えるのね」

私「厳密には、真偽表は、意味を知るのには分かり易いけど、この一連の推論パターンによって、論理記号の使い方を定めるだけで、真偽表に書かれている真偽と同じようなものが、導かれるようになっている。そういう意味で、形式的な、構文論 ${\mathrm{(syntax)}}$ と、真偽表などで意味を考える、意味論 ${(\mathrm{semantics})}$ が、同値であるという論理学の定理が、『現代論理学』においても、証明されている」

安井邦夫（やすい　くにお）『現代論理学』（世界思想社）

現代論理学

作者:邦夫, 安井
世界思想社

Amazon

麻友「太郎さんは、推論のパターンは、１３個だと言っていた。『 ${\wedge}$ 導入』『 ${\wedge}$ 除去』『 ${\Rightarrow}$ 除去』『 ${\Rightarrow}$ 導入-仮定除去』『 ${\vee}$ 導入』『 ${\vee}$ 除去』まで、昨日やって、今日、『準背理法』と、『片方否定』をやって、８個まで、来た。後の５個は？」

私「残りの５つのうち、４つは、ときどき出てきた、『任意の』という意味の『 ${\forall}$ 』と、存在するという意味の『 ${\exists}$ 』という記号の、導入と、除去の推論パターンが、それぞれ１つずつ有って、それで、４つなんだ。だけど、麻友さんはまだ、『 ${\forall}$ 』と『 ${\exists}$ 』を勉強するには、数学の経験が、乏しすぎる。このエニとイグジストの出て来る論理学を、述語論理学というのだけ、今日は覚えていって欲しい」

麻友「今までのは？」

私「命題論理学というんだ」

麻友「命題論理学か。それで、残りの５つの、最後の１個は？」

私「そこが、ハイライトなんだ。まず古典論理では、『 ${\neg}$ 』の最後の性質は、『二重否定』と、私が呼んでいる、

${~~~~~~~\neg (\neg A) \\ \rule{3.0cm}{0.3mm} \\ ~~~~~~~~~~~~~~A \\ }$

という推論なんだ」

麻友「否定の否定は、肯定ね。当然、否定の記号は、そういう性質を持っていなければね」

私「ところで、私がやっと理解し始めた、直観主義論理では、これは、成り立たない」

麻友「どうするの？」

私「先日、リンク集の中の、NKsummary.pdf に間違いがあったと言ったけど、ここで、修正を宣言しよう。以後、あのファイルは、書き換える」

麻友「どの部分？」

私「最後のところだけど、ちょっと長いよ。もうすでに、少し改訂したけど、

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

　直観主義論理とは

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

　本章を読んできて、私達の論理（それは、古典論理と呼ばれる） ${\mathbf{NK}}$ （エヌケーまたは、ドイツ語式に、エヌカーと呼ばれる）と、直観主義論理 ${\mathbf{NJ}}$ （エヌジェイまたは、ドイツ語式に、エヌヨットと呼ばれる）とは、何が違うのだろうと、知りたい人もあるだろう。

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

それは、私達のいう ${\mathbf{NK}}$ での命題は、真（正しい）か、偽（正しくない）かが、定まるものであったのに対し、直観主義論理では、『Aが正しい』とは、『Aを確認する方法をもっている』ということなのである。

${\mathbf{NK}}$ と ${\mathbf{NJ}}$ での推論図の違いは、二重否定の推論、

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

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

${\neg (\neg A)\\ \rule{3.0cm}{0.3mm} \\ ~~~A\\ }$

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

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

を、

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

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

${~~~~\neg A\\ \rule{3.0cm}{0.3mm} \\ ~~A \Rightarrow ( B \wedge \neg B)\\ }$

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

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

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

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

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

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

　ここまでのなかで、麻友さん達に、否定の記号の定義に否定の記号を使っていて、循環論法だと、指摘された。

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

${~~~~\neg A\\ \rule{3.0cm}{0.3mm} \\ ~~A \Rightarrow ( B \wedge \neg B)\\ }$

の、ところだ。『 ${\neg}$ 』が、 ${A \Rightarrow ( B \wedge \neg B)}$ だと言っている。『 ${\neg}$ 』を使わずに定義しなければならないよね。そこで、考えたんだけど、 ${( B \wedge \neg B)}$ という矛盾でなく、任意の、 ${B}$ にしてしまったらってね」