内容

目次

1.　準備 言葉づかいについて：集合，順序と同値関係，写像と関数 2.　命題論理 2.1　日常的推論と記号化 2.2　数理パズルと記号化 2.2.1　スマリヤン流のパズル 2.2.2　不思議の国のパズル 2.2.3　スマリヤン流パズル再考 2.2.4　パズルランドのアリス 2.2.5　同値式の代数的性質 2.2.6　映画Labyrinthのパズル 2.2.7　ジョージ・ブーロスの最強のパズル 2.3　命題論理の言語：論理式 2.4　命題論理の意味論 2.4.1　論理式の値：真理値 2.4.2　恒真（トートロジー），充足可能，充足不可能 2.4.3　意味論的同値関係 2.4.4　意味論的帰結Γ|=A 2.5　ブール代数 2.6　ブール関数 2.7　命題論理の形式的体系 2.7.1　自然演繹の体系NJとNK 2.7.2　古典論理と直観主義論理：埋め込み 2.8　形式的体系の健全性と完全性 2.8.1　NKの健全性 2.8.2　NKの完全性 3.　述語論理 3.1　数理パズルと述語論理による記号化 3.1.1　だれがヒゲを剃るか？ 3.1.2　スマリヤン流パズル述語論理版 3.1.3　TiffanyDuneau:SolvinglogicalpuzzlesinDisCoCircにおけるスマリヤン流パズル 3.1.4　関数の連続性の定義 3.1.5　言葉づかいについての復習 3.2　述語論理の言語 3.3　述語論理の形式的体系 3.3.1　自然演繹の体系NKとNJ 3.3.2　述語論理におけるグリベンコの定理：埋め込み 3.4　述語論理の意味論 3.4.1　構造と解釈 3.4.2　NKの健全性 3.4.3　NKの完全性：シーケントの分解と反例の構成 4.　証明の形式化とラムダ計算 4.1　証明図の簡約 4.2　証明の記号化・形式化 4.2.1　ラムダ記法：関数と値の区別 4.2.2　ラムダ項（ラムダ式） 4.2.3　ベータ変換 4.2.4　チャーチ・ロッサーの定理 4.2.5　型付きラムダ計算：型推論 4.2.6　型付きラムダ項とベータ変換 4.3　カリー・ハワード同型 4.3.1　論理式と型 4.3.2　証明図の簡約とベータ変換，CPS変換と埋め込み 4.3.3　古典論理の証明項：ラムダ・ミュー計算 引用・参考文献 索引