数学とプログラミングとくだらないこと

プログラミングの事とか数学のこととかを書いていきます。

数理論理学のノート1

本を読んだメモ。

数理論理学の目的

以下要約


証明の妥当性は、数学的な訓練を受けている人には直感的に判断できる。 昔の欧州の人たちは、「理性」というものの存在が原因と考えていた。 しかしこのままでは「理性とは何か?」という疑問が生じる。 この「理性」というものの性質を示す必要がある。

そのために、「証明を説明対象とした理論」、論理学を作り上げて、数学的な証明と照らし合わせて検証することが必要になる。

ここでいう検証とは、直感による数学的な証明の妥当性と、論理学が予測する証明の妥当性が一致することを確かめることである。 この検証には、自然科学的な方法論を用いる。

記号論理学とは、証明とその構成要素を記号化することで 「証明の妥当性」を根本的な原理から導出しようとするものである。


この内容、実のところさっぱりわからん。

という訳で、Wikipediaの数学基礎論なんて見てみた。

個人的にだした結論は、

  • 「客観的に証明の妥当性を検証する」のが論理学
  • 「記号化による検証を行う論理学」が記号論理学

多分。

間違ってなかろうか。

命題と真偽

証明には以下のような「構文」が繰り返しあらわれ、その「構文」の組み合わせで表現されている。

  1. φではない
  2. φであり、かつψである
  3. φであるか、またはψである
  4. φならばψである
  5. すべてのxについてφである
  6. (したがって)φ1,..., φnより, ψである

それ以外の構文は、これらの構文の組み合わせで表現できる。

φやψの位置に入るものについては、表す内容が真偽を問えるということ。 真偽を問える形式を命題と呼ぶ。

しかし真偽や命題が何かという話にはいまだ議論の余地があるらしい。 たとえば様相論理というものがある。 この様相論理では、主観的な内容も命題として扱えるらしい。 数学的推論が世界を変えるって本には、この様相論理が金融HFT(だと思う)分野で重要らしい。 まだ途中までしか読んでない。

さて、話をもどそうか。

上の「構文」を持つ文についても真偽が問える。 そうすると、命題を組み合わせて命題を作れるから、その組み合わせの規則があれば、命題の集合というものが作れる。

推論と妥当性

証明に現れる文が命題なら、証明は複数の命題を並べたものと考えられる。 上の構文の6つ目の形式は、複数の命題から、一つの命題を導いている。 これを

φ1,..., φnψ

と表す。

この形式を推論と呼ぶ。また、φ1,..., φn前提、ψを帰結と呼ぶ。

こうすると、今度は証明を推論がなにかの規則によって連なったものであると考えられる。

ならば正しい証明とは、

  • 「妥当な推論」から構成される
  • 「推論」と「推論」の組み合わせ方が妥当である

の、二つの条件を満たしていなければならない。

「妥当な推論」とは、前提の命題が全て真であるとき、帰結の命題も真であるものである。


以上から、「証明」を説明するのには、

  1. どのような形式が推論であり、どんな形式が推論でないかを定義する(推論の集合を定める)
  2. 推論の集合の内、妥当な推論をそうでない推論を定義する

が必要なことがわかる…はず。

ノートにするはずが、本の丸写しになってしまった…。 もうちょっとどうにかならんかな。

疲れた。今日はこんな感じでいいか…。