自然演繹とシーケント計算

自然演繹とシーケント計算は、論理結合子の導入規則と除去規則を通じて証明を表現する2つのゲンツェン流形式体系であり、構造的証明論の基本的な仕組みを形成しています。

Definition

自然演繹は、非形式的な推論を反映した導入規則と除去規則を用いて仮定から論理式を導出するのに対し、シーケント計算は、ある論理式のリストが別の論理式を伴うという主張であるシーケントを、含意の左側と右側に作用する規則を通じて操作します。

Scope

このトピックでは、自然演繹の規則とその導入・除去ペア、シーケント計算の構造とその左規則・右規則および構造規則、自然演繹の正規化、両体系の関係、そしてそれらの直観主義的および古典的変種について扱います。

Core questions

• 導入規則と除去規則は、論理結合子にどのように意味を与えますか？
• シーケントとは何ですか？また、その規則は自然演繹の規則とどのように異なりますか？
• 正規化は自然演繹の証明をどのように単純化しますか？
• これらの計算の古典的バージョンと直観主義的バージョンはどのように関連していますか？

Key theories

導入規則と除去規則

各結合子は、それを導入する規則とそれを利用する規則によって支配され、導入がもたらすものを除去が正確に回復するというそれらの調和が、結合子の意味を表現します。

正規化定理

プラウィッツは、自然演繹の証明が、導入が除去によって直ちに無効にされる迂回路のない正規形に還元できることを示しました。これはカット除去の自然演繹版です。

2つの計算の対応

自然演繹とシーケント計算は同じ定理を証明し、互いに翻訳可能です。シーケントの左規則は自然演繹の除去規則に対応します。

Clinical relevance

これらの計算は、証明を構造的に研究するための標準的な形式です。自然演繹は、証明とプログラムの対応を通じて型理論と証明支援系の基礎となり、一方、カット除去後の部分論理式特性を持つシーケント計算は、自動証明探索と解析的タブローの基礎となります。

History

ゲンツェンは1934年と1935年に自然演繹とシーケント計算の両方を導入しました。彼は自然演繹の分析が難しいと感じた後、カット除去定理を得るためにシーケント計算を考案しました。プラウィッツは1965年に徹底的な正規化研究によって自然演繹を復活させ、これらの体系は後の証明とプログラムの対応の発展の中心となりました。

Key figures

• Gerhard Gentzen
• Dag Prawitz
• Stanislaw Jaskowski
• Jan von Plato

Seminal works

• troelstra2000
• prawitz1965
• negri2001

Frequently asked questions

自然演繹とシーケント計算の違いは何ですか？

自然演繹は、仮定の文脈の下で論理式を扱い、非形式的な証明に密接に一致する除去規則を使用します。シーケント計算は、明示的な含意を扱い、除去規則を左導入規則に置き換えます。この形式は、カット除去と部分論理式特性を明確にします。

正規化が重要なのはなぜですか？

正規化された証明には迂回路がなく、部分論理式特性を持つため、その中のすべての論理式は結論または前提の部分論理式です。これにより、証明の形状が制約され、無矛盾性結果が得られ、証明とプログラムの対応を通じて、プログラムを値に評価することに対応します。