講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編のPDF資料を快適に閲覧・印刷することができます。
セミナーの概要
本セミナー「命題論理の演繹ルール」は、論理学の基礎である命題論理を、単なる真偽判定の道具として捉えるのではなく、「証明とは何か」「推論とはどのような構造を持つか」という哲学的・数理的な問いに真摯に向き合うことを出発点としています。[p.1]
講義はまず、∧（かつ）、∨（または）、→（ならば）、¬（ではない）といった基本的な論理記号とその真理表から丁寧に出発します。[p.5, p.6]論理式が「真」であるとはいかなることかを問うと、それは単なる記号操作ではなく「私はAが真であることを知っている」という認識論的な「判断」の問題であることが明らかになります。[p.26, p.27]このとき「判断」の概念は「命題」の概念に先立ち、論理的帰結の概念もまた命題における含意よりも先に説明されなければなりません。
こうした認識論的基盤の上に立って、本講義はGentzenのSequent Calculusという強力な演繹システムを導入します。[p.53]記号「⊢」（ターンスタイル）によって表される「A⊢B」という判断は、前提Aから帰結Bが論理的に導かれることを意味し、これが「証明」の形式的な骨格を成します。[p.45]Sequent Calculusでは証明すべき論理式から出発して演繹ルールを逆向きに適用し、すべての枝が公理「A⊢A」に到達したとき証明が完成するというボトムアップの証明戦略が採用されます。[p.53, p.58]
さらに講義の後半ではNatural Deductionへと議論が展開されます。古典論理のLKに対し、Sequentの右辺を1個に制限したLJが直観主義論理に対応することが示され、そこからNatural Deductionの演繹ルールが自然に導出されます。[p.130, p.131]最終章では対話型証明支援システムCoqとNatural Deductionの演繹ルールが対応していることが具体的に示され、intros、split、left、rightといったtacticが∧右・∨右などの演繹ルールの「逆向き適用」として解釈できることが明確化されます。[p.147, p.148]証明とは判断を明証なものにする行為であり、証明することと知ることは同じことであるという哲学的洞察で全体が統合されています。[p.36]
講義のロードマップ
ここでは、セミナーの講演資料がどのようなパートから構成されているかを示します。また、それぞれのパートのポイントを紹介します。
■ Part 1: 論理式と推論ルール
命題論理の基本記号と真理表の復習から始まり、論理式の「値」を問うことが実は「判断」という認識論的概念の問題であることを明らかにします。論理式の意味論（同値、恒真式）と構文論（Formation Rule）の両面を整理し、「A⊢B」という論理的帰結の判断の概念と、それを推論ルール（演繹ルール）として表現する横棒（inference line）記法を導入します。[p.25, p.37, p.44]
■ Part 2: Sequent Calculus
GentzenのSequent Calculusを証明システムとして導入し、証明すべき論理式から演繹ルールを逆向きに適用してすべての葉を公理に到達させる「ボトムアップ証明」の方法論を確立します。Γ、Δというギリシャ文字による論理式の集合の表現と、各論理記号に対応した演繹ルール（公理・→左右・∧左右・∨左右・¬左右）を体系的に整備し、複数の具体的な証明例を通じてシステムの理解を深めます。[p.53, p.56, p.66]
■ Part 3: Natural Deduction
GentzenのLKにおいてSequentの右辺を0または1個に制限したLJが直観主義論理に対応すること、さらに右辺を厳密に1個に制限したものがNatural Deductionであることを示します。LKの各演繹ルールからNatural Deductionの演繹ルールを系統的に導出し、対話型証明支援システムCoqのtacticがこれらのルールの逆向き適用として解釈されることを具体例で示します。[p.130, p.131, p.132]
ページのナビゲート