相対性理論を学びたい人のために

まだ一度も相対性理論を勉強したことのない人は、何か一冊相対性理論の本を読みかじってみて、なぜこんなことが?という、疑問を持ってからこのブログに来てください。ブログの先頭に戻るには表題のロゴをクリックしてください

数学を悟ってみて(その27)

 現在2020年12月24日20時21分である。

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

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

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

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

私「確かにそうだけど」

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

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

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

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

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

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

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

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

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

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

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


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

麻友「数学の推論で、『{\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})}が、同値であるという論理学の定理が、『現代論理学』においても、証明されている」

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

現代論理学

現代論理学

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

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

麻友「今までのは?」

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

麻友「命題論理学か。それで、残りの5つの、最後の1個は?」

私「そこが、ハイライトなんだ。まず古典論理では、『{\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)\\
}

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


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


麻友「そうすると、どうなるの?」

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

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

となる」

麻友「それで、上手く行くの?」

私「今のところ、問題は、見つかってない」


麻友「太郎さん。面白い話だけど、もう23時28分よ。寝た方がいいわ」

私「直観主義論理の話、かなり長くなってるね」

麻友「それじゃ、2人だけのクリスマスイヴだったわね。おやすみ」

私「おやすみ」

 現在2020年12月24日23時32分である。おしまい。