論理学入門 I ? 命題論理の演繹ルール

全体概要

本セミナー「命題論理の演繹ルール」は、論理学の基礎である命題論理を、単なる真偽判定の道具として捉えるのではなく、「証明とは何か」「推論とはどのような構造を持つか」という哲学的・数理的な問いに真摯に向き合うことを出発点としています。[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]

• 論理展開:
• ∧、∨、→、¬の真理表と同値・恒真式の定義を確認し、「A→B ≡ ¬A∨B」を真理表で証明する。[p.11], [p.12], [p.18]
• 「Aは真である」とは「私はAが真であることを知っている」という判断であり、表現・判断の形式・明証的な判断という階層構造を持つことを示す。[p.26], [p.30], [p.35]
• 論理式の構成ルール（Formation Rule）を∧F、→F、∨F、¬Fとして横棒記法で形式化し、「形の整った論理式はすべてこのルールで構成される」という原理を示す。[p.39], [p.40], [p.41]
• 「A⊢B」という判断と「⊢A→B」という判断の関係を横棒で結びつけることで「演繹ルール」の概念を導入する。[p.47]

■ Part 2: Sequent Calculus

• この部の核心:

GentzenのSequent Calculusを証明システムとして導入し、証明すべき論理式から演繹ルールを逆向きに適用してすべての葉を公理に到達させる「ボトムアップ証明」の方法論を確立します。Γ、Δというギリシャ文字による論理式の集合の表現と、各論理記号に対応した演繹ルール（公理・→左右・∧左右・∨左右・¬左右）を体系的に整備し、複数の具体的な証明例を通じてシステムの理解を深めます。[p.53], [p.56], [p.66]

• 論理展開:
• 公理「Γ,A⊢A,Δ」から出発し、→右・∧右・∨右・¬右の各右辺ルールと→左・∧左・∨左・¬左の各左辺ルールを演繹ルールのまとめとして提示する。[p.66]
• 「A→A」「A∧B→A」「A∧B→B∧A」「A∨B→B∨A」「A→(A→B)→(B→C)→C」などの恒真式の証明図（証明樹）を段階的に示す。[p.68], [p.73], [p.84], [p.98], [p.99]
• Logitextを用いた演習課題として、インタラクティブにSequent Calculusの証明を体験する方法を紹介する。[p.126], [p.127], [p.128]

■ Part 3: Natural Deduction

• この部の核心:

GentzenのLKにおいてSequentの右辺を0または1個に制限したLJが直観主義論理に対応すること、さらに右辺を厳密に1個に制限したものがNatural Deductionであることを示します。LKの各演繹ルールからNatural Deductionの演繹ルールを系統的に導出し、対話型証明支援システムCoqのtacticがこれらのルールの逆向き適用として解釈されることを具体例で示します。[p.130], [p.131], [p.132]

• 論理展開:
• LKのSequent（右辺が複数）からLJ（右辺が0または1個）、Natural Deduction（右辺が1個）への制限の過程で、∨右ルールのみ2つに分割する必要があることを示す。[p.135], [p.136]
• Coqが出力する「仮説部＋サブゴール」という「証明の状態」が演繹ルールの各段「Γ⊢命題」に対応していることを図解する。[p.141], [p.142], [p.143]
• tactic introsが→右ルール、splitが∧右ルール、leftが∨右1ルール、rightが∨右2ルールにそれぞれ対応し、各tacticの適用前後での仮説部・サブゴールの変化が演繹ルールの逆向き適用として説明できることを具体的な画面例で示す。[p.148], [p.154], [p.161]