第3章第3節 証明論 【基本】¶
学習目標¶
この節では、様相論理における形式的証明の方法を学習します。具体的には、ヒルベルト形式体系における公理的証明の構成法の習得、自然演繹体系による直観的な推論の実践、タブロー法による機械的な証明探索の理解、そして各証明体系の長所と短所の比較評価を目標とします。
本節の概要
多様な証明体系：ヒルベルト形式、自然演繹、タブロー法という異なるアプローチが、それぞれの特徴を活かして様相論理の証明を可能にする。
証明の構造化：形式的証明を段階的に構築する技法により、複雑な様相論理の定理も体系的に証明可能となる。
機械化への道：タブロー法などの手法により、様相論理の証明探索が機械的に実行可能となり、自動証明への道が開かれる。
前節までで様相論理の様々な体系を学びましたが、この節では、これらの体系において実際に証明を構築する方法を詳しく探求します。証明論は、論理的推論を形式的かつ体系的に実行するための理論的基盤を提供します。
3.3.1 ヒルベルト形式体系¶
公理的アプローチの特徴¶
ヒルベルト形式体系は、最も伝統的な証明体系です。少数の公理と推論規則から出発し、定理を段階的に導出していく方法は、ユークリッド幾何学以来の数学的伝統に根ざしています。
ヒルベルト形式体系の基本的な考え方は、「最小限の仮定から最大限の結果を導く」ことです。これは建築に例えると、しっかりとした基礎（公理）の上に、一つ一つレンガ（定理）を積み上げていく作業に似ています。各レンガは、既に置かれたレンガの上にのみ置くことができ、空中に浮かせることはできません。
K体系での証明構築¶
論理Kのヒルベルト形式体系で、具体的な証明を構築してみましょう。目標は \(\Box(p \to q) \to (\Box p \to \Box q)\)（K公理自体）から、より複雑な定理を導出することです。
定理3.3.1：\(\vdash_K \Box(p \land q) \to \Box p\)
この定理は「pかつqが必然的ならば、pも必然的である」という自然な原理を表現しています。証明を段階的に構築します。
まず、命題論理から \((p \land q) \to p\) がトートロジーとして得られます。これは「\(p\)かつ\(q\)」から「\(p\)」が導かれるという基本的な推論です。次に、ネセシテーション規則を適用して \(\Box((p \land q) \to p)\) を得ます。論理的真理は必然的真理でもあるという原理です。最後に、K公理 \(\Box((p \land q) \to p) \to (\Box(p \land q) \to \Box p)\) を適用し、モーダスポネンスにより目標の定理が得られます。
この証明プロセスは、各ステップが明確に正当化され、機械的に検証可能です。しかし、証明を発見するプロセスは必ずしも機械的ではなく、創造性と洞察が必要となります。
証明の戦略と技法¶
ヒルベルト形式体系での証明構築には、いくつかの基本的な戦略があります。
後ろ向き推論の戦略では、証明したい定理から出発し、それを導出できる既知の定理や公理を探します。例えば、\(\Box\varphi \to \Box\psi\) を証明したい場合、K公理の形 \(\Box(\varphi \to \psi) \to (\Box\varphi \to \Box\psi)\) を思い出し、\(\Box(\varphi \to \psi)\) を証明すれば良いことに気づきます。
補題の活用も重要な技法です。複雑な定理を直接証明する代わりに、有用な補題を先に証明し、それらを組み合わせることで目標に到達します。例えば、\(\Box(\varphi \land \psi) \leftrightarrow (\Box\varphi \land \Box\psi)\) を証明する際は、両方向の含意を別々に証明します。
ヒルベルト形式体系の長所と短所¶
ヒルベルト形式体系の最大の長所は、その理論的優雅さです。最小限の公理から出発する体系は、論理の基礎を明確にし、メタ理論的な分析を容易にします。独立性、一貫性、完全性などの性質を研究する際には、ヒルベルト形式体系が最も適しています。
一方で、実際の証明構築においては困難が伴います。人間の自然な推論とは異なり、公理からの導出は迂回的で直観に反することがあります。また、長い証明では中間段階を追跡することが困難になり、証明の全体構造を把握しにくくなります。
3.3.2 自然演繹体系¶
推論規則による構成¶
自然演繹（Natural Deduction）は、人間の実際の推論により近い証明体系です。公理の代わりに、各論理結合子と様相演算子に対する導入規則と除去規則を使用します。
自然演繹の基本的な考え方は、「仮定から結論へ」という自然な推論の流れを形式化することです。数学の証明で「～と仮定すると」「したがって～」という推論を行うように、自然演繹でも仮定を立て、そこから結論を導きます。
定義3.3.1 —— 様相論理の自然演繹規則
\(\Box\)の導入規則（\(\Box\)I）：
\(\Box\)の除去規則（\(\Box\)E）： [ \frac{\Box \phi}{\phi} \Box E \quad \text{（T体系以上で有効）} ]
\(\Diamond\)の導入規則（\(\Diamond\)I）： [ \frac{\phi}{\Diamond \phi} \Diamond I ]
仮定の管理と文脈¶
自然演繹の特徴的な側面は、仮定の管理です。証明の過程で仮定を導入し、後でそれを除去（discharge）することで、条件文を証明します。
例えば、\((\Box p \land \Box q) \to \Box(p \land q)\) を証明する場合を考えましょう。まず \(\Box p \land \Box q\) を仮定します。この仮定から \(\Box p\) と \(\Box q\) が得られ、それぞれから \(p\) と \(q\) が導出されます（T体系の場合）。これらを結合して \(p \land q\) を得、\(\Box\)導入規則により \(\Box(p \land q)\) が得られます。最後に、最初の仮定を除去して、求める条件文が証明されます。
この証明の流れは、「もし\(\Box p\)かつ\(\Box q\)ならば、\(p\)かつ\(q\)が成り立ち、したがって\(\Box(p \land q)\)も成り立つ」という自然な推論を反映しています。
ボックス証明の技法¶
様相論理の自然演繹では、ボックス証明（boxed proof）という特殊な技法を使用します。\(\Box\varphi\)を証明する際、新しい「ボックス」を開き、その中で\(\varphi\)を証明します。このボックスは、可能世界への移行を表現しています。
ボックス内では、外側の仮定のうち、\(\Box\)が付いたものだけを使用できます。これは、別の可能世界では、必然的でない事実は成り立たない可能性があることを反映しています。この制約により、様相論理特有の推論が正しく扱われます。
自然演繹の利点¶
自然演繹の最大の利点は、その直観性です。人間が実際に行う推論のパターンを直接反映しているため、証明の構造が理解しやすく、証明の発見も比較的容易です。
また、証明の構造が推論の構造を直接反映するため、証明から計算内容を抽出するカリー・ハワード対応の文脈でも重要な役割を果たします。これにより、証明と計算の深い関係が明らかになります。
3.3.3 タブロー法¶
反証による証明¶
タブロー法（Tableau Method）は、反証法の原理に基づく証明方法です。定理を証明するために、その否定から矛盾を導きます。この方法は、「背理法」として知られる古典的な証明技法の形式化と言えます。
タブロー法の基本的なアイデアは、式の真理可能性を体系的に探索することです。式が偽であると仮定し、その仮定の下で可能な状況をすべて展開していきます。すべての可能性が矛盾に至れば、元の式は必然的に真であることが証明されます。
タブローの構築規則¶
タブローは木構造として構築されます。各ノードには符号付き式（TφまたはFφ）が含まれ、Tは「真」、Fは「偽」を表します。
様相論理のタブロー規則
T□規則：
F□規則：
T◇規則：
具体例による理解¶
□(p → q) → (□p → □q)（K公理）をタブロー法で証明してみましょう。
まず、この式が偽であると仮定します：F(□(p → q) → (□p → □q))。条件文が偽となるのは、前件が真で後件が偽の場合なので、T□(p → q) と F(□p → □q) が得られます。さらに展開すると、F(□p → □q) から T□p と F□q が得られます。
\(F\Box q\) は「\(q\)が必然的でない」ことを意味するので、\(q\)が偽となる到達可能世界が存在します。その世界を\(w_1\)とすると、\(w_1\)で \(Fq\) となります。一方、\(T\Box(p \to q)\) と \(T\Box p\) から、\(w_1\)で \(T(p \to q)\) と \(Tp\) が成り立ちます。
\(w_1\)で \(p \to q\) が真で \(p\) も真なので、\(q\) も真でなければなりません。しかし、既に \(Fq\) があるため矛盾が生じます。すべての枝が閉じたため、元の式は証明されました。
タブロー法の機械化¶
タブロー法の大きな利点は、その機械的性質です。規則の適用は決定的で、証明探索を系統的に実行できます。
証明探索のアルゴリズムは以下のようになります：未処理の符号付き式を選び、対応する規則を適用し、新しい符号付き式を追加します。矛盾（TφとFφが同じ世界に現れる）が見つかれば、その枝を閉じます。すべての枝が閉じれば証明完了、開いた枝が残れば反例が見つかったことになります。
この機械的性質により、タブロー法は自動定理証明システムの基礎として広く使用されています。
証明体系の選択指針
各証明体系の使い分け：
- 理論研究：ヒルベルト形式（メタ理論的性質の分析）
- 人間による証明：自然演繹（直観的理解）
- 自動証明：タブロー法（機械的探索）
- 教育目的：自然演繹とタブロー法の併用
3.3.4 証明体系の比較と等価性¶
表現力の等価性¶
驚くべきことに、これらの異なる証明体系は、証明能力において等価です。つまり、ある体系で証明可能な定理は、他の体系でも証明可能です。
この等価性は、各証明体系が同じ論理を異なる視点から捉えていることを示しています。ヒルベルト形式は公理的構造を、自然演繹は推論過程を、タブロー法は意味論的構造を重視しています。これらの視点は相補的で、論理の全体像を理解する上で、それぞれが重要な役割を果たします。
証明の変換¶
ある証明体系での証明を、別の体系での証明に変換することができます。この変換プロセスは、証明の本質的構造を保存しながら、表現形式を変更します。
例えば、自然演繹の証明をヒルベルト形式に変換する際は、推論規則の各適用を、対応する公理と定理の組み合わせで置き換えます。逆に、ヒルベルト形式の証明を自然演繹に変換する際は、公理を基本的な推論規則の組み合わせとして実現します。
計算複雑性の観点¶
証明体系の選択は、計算複雑性にも影響を与えます。証明の長さは体系によって大きく異なる可能性があります。
ヒルベルト形式では、単純な定理でも長い証明が必要になることがあります。これは、基本的な推論ステップを公理から導出する必要があるためです。一方、自然演繹では、より直接的な証明が可能ですが、仮定の管理に計算コストがかかります。
タブロー法は、最悪の場合、指数的なサイズの木を生成する可能性がありますが、多くの実用的な場合には効率的に動作します。ヒューリスティックを使用することで、証明探索の効率を大幅に改善できます。
実装における考慮事項¶
証明支援システムや自動定理証明器を実装する際は、各証明体系の特性を考慮する必要があります。
タブロー法は、その機械的性質から、自動証明に最も適しています。分岐の順序や規則適用の戦略により、性能を最適化できます。自然演繹は、対話的証明支援システムに適しており、ユーザーが証明の構造を理解しやすいという利点があります。
ヒルベルト形式は、証明の検証には適していますが、証明の発見には適していません。そのため、実装では他の体系で証明を発見し、必要に応じてヒルベルト形式に変換するアプローチが取られることがあります。
3.3.5 証明論の応用と展望¶
証明支援システムへの応用¶
現代の証明支援システム（Proof Assistant）では、様相論理の証明論が重要な役割を果たしています。Coq、Isabelle、Leanなどのシステムでは、様相論理を内部的に使用して、プログラムの性質や数学的定理を証明します。
これらのシステムでは、人間が証明の大まかな構造を指定し、システムが詳細な証明ステップを自動的に埋めるという協調的アプローチが取られます。自然演繹の直観性とタブロー法の機械性を組み合わせることで、効率的な証明開発が可能になります。
プログラム検証への応用¶
様相論理の証明論は、プログラムの正しさを検証する際にも使用されます。時相論理を使用してプログラムの動作を仕様化し、モデル検査や定理証明によって、プログラムが仕様を満たすことを証明します。
例えば、「必ず終了する」「デッドロックが起きない」といった性質は、様相論理で自然に表現できます。証明論の技法により、これらの性質を形式的に証明することが可能になります。
認知科学への示唆¶
証明論の研究は、人間の推論プロセスの理解にも貢献しています。自然演繹が人間の推論に近いという観察は、認知科学において重要な示唆を与えています。
人間が様相的推論（「もし～ならば」「必ず」「可能性がある」など）を行う際の認知プロセスは、自然演繹の推論規則と類似したパターンを示すことが実験的に確認されています。これは、論理と認知の深い関係を示唆しています。
発展的話題：証明論的意味論
証明そのものから意味を構成する証明論的意味論は、現代論理学の重要な研究分野です：
- 証明の正規化と計算内容の抽出
- 構成的様相論理と直観主義的解釈
- 証明の複雑性と論理の表現力の関係
これらの話題は、次節以降でさらに詳しく扱います
まとめ¶
この節では、様相論理における三つの主要な証明体系を学習しました。重要なポイントは以下の通りです：
ヒルベルト形式体系は、最小限の公理から出発する理論的に優雅な体系ですが、実際の証明構築には困難が伴います。公理的アプローチは、論理の基礎を明確にし、メタ理論的分析に適しています。
自然演繹は、人間の自然な推論パターンを反映した直観的な体系です。仮定の導入と除去、ボックス証明などの技法により、様相論理の推論を自然に表現できます。証明の構造が推論の構造を直接反映するため、理解しやすく、教育的価値も高いです。
タブロー法は、反証法の原理に基づく機械的な証明方法です。体系的な証明探索が可能で、自動定理証明に適しています。規則の適用が決定的で、アルゴリズム化が容易という利点があります。
これらの証明体系は証明能力において等価ですが、それぞれ異なる特徴と利点を持ちます。理論研究、人間による証明、自動証明など、目的に応じて適切な体系を選択することが重要です。
次節への展望¶
次の第4節「対応理論」では、様相論理の公理とフレーム条件の対応関係をより深く探求します。この美しい理論により、構文論と意味論の密接な関係が明らかになり、様相論理の理解がさらに深まります。
参考文献¶
- Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal Logic. Cambridge University Press.
- Fitting, M., & Mendelsohn, R. L. (1998). First-Order Modal Logic. Kluwer Academic Publishers.
- Garson, J. W. (2013). Modal Logic for Philosophers (2nd ed.). Cambridge University Press.
- Girard, J. Y., Taylor, P., & Lafont, Y. (1989). Proofs and Types. Cambridge University Press.
- Goldblatt, R. (1992). Logics of Time and Computation (2nd ed.). CSLI Publications.
- Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell.
- Smullyan, R. M. (1968). First-Order Logic. Springer-Verlag.
- Troelstra, A. S., & Schwichtenberg, H. (2000). Basic Proof Theory (2nd ed.). Cambridge University Press.