数理論理学
論理式の証明体系と、その意味論・拡張を扱う分野。命題論理を出発点に、様相・時制・線形などの非古典論理、そしてSMT ソルバへ広がる。
論理の分類
- 古典論理: 命題論理 / 述語論理
- 非古典論理:
- 直観主義論理（排中律なし、構成的）
- 様相論理（可能性・必然性）→ 時制論理（時間）
- 多値論理（ternary logic、ファジー論理）
- 線形論理（資源の概念）
命題論理と自然演繹
、（iff）、（トートロジー）を使う。自然演繹体系 NK は の導入・除去規則と二重否定除去からなり、終論理式 の証明があれば （証明可能）。
- 健全性: 証明可能な論理式は全てトートロジー
- 完全性: 全てのトートロジーは証明可能
NK は健全かつ完全。古典論理は LK（シーケント計算）として整理される。証明図は前提を上、結論を下に書く木構造で表す。
直観主義
数学的対象は構成的手続きで存在を示さねばならず、背理法を認めない。「具体的な計算（プログラム）が証明になる」という Curry–Howard 的な見方に繋がる。
様相・時制・線形論理
- 様相論理 K: （必然的に A）、（可能）。古典体系 LK に必然化規則を追加。
- 時制論理 Kt: 過去 ・未来 に細分化。
- 線形論理: 「110 円でコーラとチョコのどちらも買える（&）」と「両方同時に買える（）」を区別し、含意を で表す。限りあるリソースを表現でき、並行分離論理（Iris/RustBelt の基盤）など並行プログラム検証に使われる。
余談
ヘンペルのカラス（「全てのカラスは黒い」「黒くないものはカラスでない」）のような確証のパラドクスも論理学的話題。
関連: computability-theory / mathematical-logic / _moc-math
公理的集合論と基礎論
数学全体を集合の言葉で基礎づける公理系と、そこから導かれる独立性・順序構造の話題。
ZF と ZFC
ZF 公理系は一般的に使われる公理系で、述語のドメインは類(class)（すべての集合を集めたもの）。主な公理：
- 外延性（含む元が全て等しい集合は等しい）
- 空集合・無限集合の存在
- 対・和・冪・置換（既存の集合から新しい集合を作る）
- 正則性（パラドクス回避）
これに選択公理を加えたものが ZFC。選択公理は「空でない集合族から各々一つずつ選んで集合を作れる」＝ 。
選択公理と同値な命題
- Zornの補題：全順序部分集合が常に上界を持つ順序集合（Zorn集合）には極大元が存在する。極大元を持たないと仮定して矛盾を導く形で証明する。
- 整列可能定理
これらは選択公理と同値で、代数閉包の存在など多くの存在証明の根拠になる。
独立性
連続体仮説は「可算濃度と連続体濃度の間に他の濃度が無い」とする主張で、ZFC からは証明も反証もできない（公理系から独立）。宇宙（Grothendieck universe）はサイズの問題を回避するための大きな集合の枠組み。
順序構造と測度
- 順序集合を図示するハッセ図、join で閉じた join semilattice など順序理論の道具。
- 可測空間（ 加法族）と測度は確率の基礎であり、確率論・ベイズ統計へ接続する。