数理論理学 入門
構文・意味・証明・Curry–Howard の入口
この章について
入門では、数理論理学の最も基本的な視点を身につける。鍵となるのは「記号の操作（構文）」と「それが意味すること（意味）」を区別するという発想である。この区別ができると、「証明」という日常語を形式的にとらえ直すことができ、さらに「証明はプログラムでもある」という Curry–Howard 対応の世界の入口に立てる。
目次
形式体系とは：構文と意味
論理学のすべての出発点。
- 記号操作としての構文
- 真理・モデルとしての意味
- $\vdash$（導ける）と $\models$（真である）
命題論理を推論規則で
もっとも単純な論理。
- 論理結合子 $\land, \lor, \to, \neg$
- 推論規則という考え方
- 真理値表との関係
述語論理と量化子
「すべて」と「存在する」。
- 述語と変数
- 全称 $\forall$・存在 $\exists$
- 束縛変数と自由変数
「証明とは何か」を形式的に
日常語を厳密にする。
- 導出（規則の適用列）としての証明
- 公理と推論規則
- 証明検査という発想
Curry–Howard のやさしい紹介
この分野の背骨を一望。
- 命題 ＝ 型
- 証明 ＝ プログラム
- 証明の簡約 ＝ 計算
次のステップ
入門で構文と意味の区別・Curry–Howard の発想をつかんだら、初級編へ進み、自然演繹（導入・除去規則）として証明体系を実際に組み立て、健全性と完全性、λ計算、直観主義論理 vs 古典論理を学ぼう。
このレベルで理解できること
構文と意味の分離
「規則に従って記号を並べる」ことと「それが正しい（真）」ことは別物である、という核心的な区別を理解する。
推論規則の体系
論理を「真理値表」ではなく「どの規則から何を導けるか」の体系として見る視点を得る。
証明とプログラムの一致
Curry–Howard 対応の直感をつかみ、後続の型理論・証明アシスタントの章への橋を渡す。