数理論理学(鹿島亮)1

数理論理学

数学で使われる論理を研究する数学の一分野

証明は論理という抽象的な存在に迫るための具体的な研究対象

全称量化子∀と存在量化子∃が2つ以上組み合わさる場合は順番が重要

どちらも同じ意味

∃x∃y(xはyのことが嫌いだ)

∃y∃x(xはyのことが嫌いだ)

https://scrapbox.io/files/6747c2b942422a3a73302a13.png

順番がわかると意味が変わる

∀x∃y(xはyのことが嫌いだ)

https://scrapbox.io/files/6747c418e146a9d271d335de.png

∃x∀y(xはyのことが嫌いだ)

https://scrapbox.io/files/6747c43396e580bbb0ada917.png

どちらも同じ意味

∀x∀y(xはyのことが嫌いだ)

∀y∀x(xはyのことが嫌いだ)

https://scrapbox.io/files/6747c55d73e082e7391554e3.png

AならばB

日常の言葉遣いでは因果関係や時間の前後関係を示すこともある

数学では「Aではない、または、Bである」と完全に同じ意味で使われる

数理論理学でもメタ論理？は古典論理だったりすることが多いんでしたけ？

演習

∃c,∃n,∀x(x>nならばf(x)≤c×g(x))の否定を書け

f(x) ∈ O(g(x)) ってことかな

¬(∃c,∃n,∀x(x>nならばf(x)≤c×g(x)))

∀c,∀n,∃x(x>nかつf(x)>c×g(x))

束縛変数 bound variable

全称量化子∀や存在量化子∃で指示されている変数

自由変数 free variable

束縛変数ではない変数

自由変数は、その値に依存して自由変数を含む論理式全体の真偽が定まるパラメータのようなもの

証明

前提から結論へ至る論理的な筋道を書いたもの

自然演繹

具体的な数学の証明ではなく、その証明を写し取ったもの(記号列)を対象にしたい

自然演繹はゲンツェンによって考案された記号列の構成の仕方の流儀の一つ

現実の証明を自然演繹に写し取ることができるが、長く読みにくくなってしまう

実際の長い証明を書くための実用的な言語ではない

少数の基本的な組み合わせで構成されているため、証明を厳密に議論できる

数学の証明の仕方をちゃんと良い感じに形式化したもの