自然演繹

自然演繹の概観

自然演繹（しぜんえんえき）は、論理的推論の自然な形式を提供する証明理論の手法であり、哲学的論理学でしばしば言及されます。この方法は、さまざまな論理体系の中でも特に重要な役割を果たし、数理論理における証明の構築において広く用いられています。

自然演繹論理の基本

自然演繹におけるある特定のバージョンでは、公理が存在しない形式が採用されています。この流派の一例として、ジョン・レモンによって開発された体系 L があり、これは主に9つの基本的な証明規則から成り立っています。これらは次の通りです：

• - 仮定の規則 (A): 自明な命題の仮定を扱います。
• - モーダスポネンス (MPP): 前件ともしもしの条件から結論を導く手法です。
• - 二重否定の規則 (DN): 否定の否定はその命題自体であるとする規則です。
• - 条件付き証明の規則 (CP): 条件が成立する場合に結論を導く手法です。
• - ∧-導入の規則 (∧I): 複数の命題が成立した場合に、その結合が成立することを示します。
• - ∧-除去の規則 (∧E): 複合命題から構成要素を導出するための規則です。
• - ∨-導入の規則 (∨I): 一方の命題からその結合を成立させる方法です。
• - ∨-除去の規則 (∨E): いずれかの選択肢を用いて結論を導出します。
• - 背理法 (RAA): 矛盾から結論を導く論法です。

これらの規則に基づいて、自然演繹における証明は、論理式（wff）の限られた列を用いて構築され、各行は体系 L の規則によって支持されなければなりません。最終的に証明の結論は、示されるべき命題である必要があります。また、前提が存在しない場合、証明は定理として見なされます。

証明の例

自然演繹での証明は、正当化された論理式の列を用いて構成され、様々な演算を駆使して結論を導きます。例えば、モーダスポネンスの規則を使った証明や排中律に関する証明は、基本的な論理法則を利用して導かれます。

背景と歴史

自然演繹の考え方は、伝統的な論理学における公理主義への批判から生じました。特に、ヒルベルトやフレーゲ、ラッセルらによる命題論理の公理化に対する不満が根底にありました。1926年には、ヤン・ウカシェヴィチが論理をより自然に扱う必要性を提唱し、その後、スタニスワフ・ヤスコウスキーが自然演繹の概念をさらに発展させました。

1935年にはドイツの数学者ゲルハルト・ゲンツェンが自然演繹の形式を提案し、「自然演繹」という用語を初めて使用しました。ゲンツェンの目的は、数論の一貫性を証明することにあり、自然演繹をそれに役立てました。その後、彼はシークエント計算を考案し、証明手法をさらに進化させました。

形式的定義と推論規則

論理的推論は形式体系中で正確に定義され、命題 α は、前提の集合 Σ に繰り返し適用される推論規則によって導かれます。この場合、すべての命題 β1 、… 、βn が、前提 Σ からの α の演繹であるためには、βn が α であり、全ての前提が前提 Σ に含まれるか、以前に現れた命題を用いることが求められます。

推論と判断

推論の形成は、命題の真理値とその妥当性を決定する上で重要です。言い換えれば、判断 A が真であるとされるとき、その証明に必要な根拠や前提があって初めて妥当性が確保されます。したがって、「雨が降っている」という判断は、その実際の確認が可能である場合にのみ、妥当とされます。このように、数理論理の文脈では、証拠は観測可能でない場合もありますが、基本的な判断からの演繹を通じて導出されます。

一貫性と完全性

数学的理論における一貫性は、仮定なしに偽を証明できない場合に成り立ち、完全性は推論規則によって全ての定理が証明可能であることを意味します。これらの性質は、論理の一般性に関する重要な洞察を提供し、証明理論や型理論との関連が探求されます。

自然演繹の体系化によって、論理学はより深く探求され、理論的な構築が進められています。

もう一度検索