数理論理学
論理式の証明体系と、その意味論・拡張を扱う分野。命題論理を出発点に、様相・時制・線形などの非古典論理、そしてSMT ソルバへ広がる。
論理の分類
- 古典論理: 命題論理 / 述語論理
- 非古典論理:
- 直観主義論理（排中律なし、構成的）
- 様相論理（可能性・必然性）→ 時制論理（時間）
- 多値論理（ternary logic、ファジー論理）
- 線形論理（資源の概念）
命題論理と自然演繹
、（iff）、（トートロジー）を使う。自然演繹体系 NK は の導入・除去規則と二重否定除去からなり、終論理式 の証明があれば （証明可能）。
- 健全性: 証明可能な論理式は全てトートロジー
- 完全性: 全てのトートロジーは証明可能
NK は健全かつ完全。古典論理は LK（シーケント計算）として整理される。証明図は前提を上、結論を下に書く木構造で表す。
直観主義
数学的対象は構成的手続きで存在を示さねばならず、背理法を認めない。「具体的な計算（プログラム）が証明になる」という Curry–Howard 的な見方に繋がる。
様相・時制・線形論理
- 様相論理 K: （必然的に A）、（可能）。古典体系 LK に必然化規則を追加。
- 時制論理 Kt: 過去 ・未来 に細分化。
- 線形論理: 「110 円でコーラとチョコのどちらも買える（&）」と「両方同時に買える（）」を区別し、含意を で表す。限りあるリソースを表現でき、並行分離論理（Iris/RustBelt の基盤）など並行プログラム検証に使われる。
余談
ヘンペルのカラス（「全てのカラスは黒い」「黒くないものはカラスでない」）のような確証のパラドクスも論理学的話題。