シークエント計算

シークエント計算（LK）とは

シークエント計算は、一階述語論理や命題論理における演繹を行うための形式的な手法です。特に、LK (Logischer Kalkül) と呼ばれる体系は、その中でも重要な役割を果たします。シークエント計算は、証明論や数理論理学において基本的な概念であり、論理的な推論を厳密に扱うための枠組みを提供します。ゲンツェン・システムとも総称されることもあります。

シークエントとは

シークエント計算における証明は、シークエントの列として記述されます。シークエントとは、前提となる命題群の論理積と、帰結となる命題群の論理和の関係を表す論理式の並びのことです。

具体的には、複数の前提から結論が導かれるという推論の構造を表現しており、形式的な推論規則に従って新しいシークエントを導き出すことで、証明を行います。

歴史

シークエント計算LKは、1934年にゲルハルト・ゲンツェンによって、自然演繹を研究するための道具として考案されました。その後、論理的な導出を行う上で非常に有効な手法であることが認識され、広く普及しました。LKという名称は、ドイツ語の「Logischer Kalkül（論理計算）」に由来します。

LK の推論規則

LKの推論規則は、以下のような記法で表されます。

横線の上にある論理式から、横線の下にある論理式が推論によって導かれることを示します。
`A`, `B` は、一階述語論理の論理式を表します（命題論理の論理式に限定する場合もあります）。
`Γ`, `Δ`, `Σ`, `Π` は、有限個の論理式の列であり、コンテキスト（文脈）と呼ばれます。
`t` は任意の項を表します。
`A[t/v]` は、論理式 `A` 内の変項 `v` の自由出現を項 `t` で置換した論理式を表します。ただし、`t`, `v`, `A` については、置換によって新たに束縛されないという条件を満たすものとします。
`x`, `y` は変項を表します。
`∀`, `∃` は量化子を表します。
`WL` は Weakening Left、`WR` は Weakening Right、`CL`と `CR` は Contraction、`PL`と `PR` は Permutation の略です。

推論規則の例

以下に、LKの代表的な推論規則の例を示します。

論理規則
(∧L1): `Γ, A, Δ ⊢ Σ` から `Γ, A∧B, Δ ⊢ Σ` を導く
(∧R): `Γ ⊢ A`, `Σ ⊢ B` から `Γ, Σ ⊢ A∧B` を導く
(∨L): `Γ, A, Δ ⊢ Σ`, `Γ, B, Δ ⊢ Σ` から `Γ, A∨B, Δ ⊢ Σ` を導く
(∨R1): `Γ ⊢ A` から `Γ ⊢ A∨B` を導く
(¬L): `Γ ⊢ A`, `Δ, ¬A ⊢ Σ` から `Γ, Δ ⊢ Σ` を導く
(¬R): `Γ, A ⊢ Δ` から `Γ ⊢ ¬A, Δ` を導く
(→L): `Γ ⊢ A`, `Δ, B ⊢ Σ` から `Γ, Δ, A→B ⊢ Σ` を導く
(→R): `Γ, A ⊢ B, Δ` から `Γ ⊢ A→B, Δ` を導く
(∀L): `Γ, A[t/x], Δ ⊢ Σ` から `Γ, ∀xA, Δ ⊢ Σ` を導く
(∀R): `Γ ⊢ A[y/x], Δ` から `Γ ⊢ ∀xA, Δ` を導く (制約: `y` は `Γ, Δ` に自由出現しない)
(∃L): `Γ, A[y/x], Δ ⊢ Σ` から `Γ, ∃xA, Δ ⊢ Σ` を導く (制約: `y` は `Γ, ∃xA, Δ` に自由出現しない)
(∃R): `Γ ⊢ A[t/x], Δ` から `Γ ⊢ ∃xA, Δ` を導く

構造規則
(WL): `Γ ⊢ Δ` から `Γ, A ⊢ Δ` を導く（左弱化）
(WR): `Γ ⊢ Δ` から `Γ ⊢ A, Δ` を導く（右弱化）
(CL): `Γ, A, A, Δ ⊢ Σ` から `Γ, A, Δ ⊢ Σ` を導く（左縮約）
(CR): `Γ ⊢ A, A, Δ` から `Γ ⊢ A, Δ` を導く（右縮約）
(PL): `Γ, A, B, Δ ⊢ Σ` から `Γ, B, A, Δ ⊢ Σ` を導く（左転置）
(PR): `Γ ⊢ A, B, Δ` から `Γ ⊢ B, A, Δ` を導く（右転置）

その他の規則
(I): `A ⊢ A` (同一性の公理)
(Cut): `Γ ⊢ A`, `A, Δ ⊢ Σ` から `Γ, Δ ⊢ Σ` (カット規則)


これらの規則は、論理的な推論を形式的に表現したものです。論理規則は、シークエントの右辺または左辺に新たな論理式を導入します。一方、構造規則は、シークエントの構造を操作します。同一性の公理 (I) は自明な真理を、カット規則 (Cut) は証明の結合を表現します。

直観的な解釈

これらの規則は、古典論理の直観的な解釈に対応しています。例えば、(∧L1) 規則は、「Aを含む論理式の列からΔが証明されるならば、A∧Bというより強い仮定からもΔが導かれる」ことを意味します。同様に、(¬R) 規則は、「ΓとAからΔが導かれるならば、ΓのみからΔが真であるかAが偽であることが導かれる」ことを意味します。量化子の規則も同様に解釈できます。

これらの規則は、与えられた論理式について証明を構築するための手順としても見ることができます。この場合、規則を下から上に適用していきます。

カット規則と同一性公理

カット規則 (Cut) は、ある論理式Aが帰結となり、同時に他の帰結の前提にもなる場合、Aを除いて論理的帰結関係を結合できることを示しています。証明をボトムアップで行う場合、Aを具体的に何にするかという問題が生じますが、カット除去定理でこの問題が扱われます。同一性の公理 (I) は、AならばAであるという自明なことを示しています。

導出例

排中律（¬A ∨ A）の導出過程を示すことで、形式的な計算構造を理解できます。


I
-----
A ⊢ A
-----(¬R)
⊢ ¬A, A
--(∨R2)
⊢ ¬A ∨ A


この導出は、構文的な計算の厳密さを表しています。例えば、右の論理規則は常にシークエントの右辺の最初の論理式に適用されています。論理式 ¬A ∨ A と A ∨ ¬A は意味的には同じですが、形式的な導出過程では異なるものとして扱われます。

構造規則

構造規則は、それぞれ「弱化規則」、「縮約規則」、「転置規則」と呼ばれます。

弱化規則は、シークエントに任意の要素を追加することを許可します。これは、証明において前提や結論に余分な情報を加えても、証明の妥当性に影響を与えないことを意味します。
縮約規則は、シークエント内の同じ式が複数回現れても、それらを一つにまとめることができることを示します。
転置規則は、シークエント内の式の順序を入れ替えても、証明の妥当性に影響を与えないことを示します。

これらの規則により、シークエント内の論理式の順序や重複を気にせずに扱うことができ、証明の簡略化や抽象化に役立ちます。

LK の特性

LKは一階述語論理において健全かつ完全です。すなわち、`Γ ⊢ A` がLKの規則群から導出されるのは、前提Γから命題Aが意味論的に導かれる場合に限ります。

また、LKにはカット除去定理が成り立ちます。これは、カット規則を用いた証明を、カット規則を用いない証明に変換できることを示しており、証明の正規化や効率化に重要な役割を果たします。ゲンツェンは、この定理を Hauptsatz（主定理）と呼びました。

派生

LKは、本質を変えることなく修正が可能です。たとえば、シークエントの列を集合や多重集合とみなすことで、転置規則や縮約規則を省略できます。また、弱化規則を公理 (I) に組み込むことで、簡略化も可能です。

コンテキストの分割方法を変更することもできます。これにより、コンテキストをコピーすることで、重要なコンテキストが失われるのを防ぐことができます。

LJ

LKの規則を少し修正することで、直観論理の証明体系であるLJ (Intuitionistic logic) が得られます。LJでは、シークエントの右辺に現れる論理式を1つまたは0個に制限し、直観主義的シークエントになるように推論規則を修正します。

例えば、(∨L) 規則は以下のように修正されます。

(∨L): `Γ, A, Δ ⊢ Σ`, `Γ, B, Δ ⊢ Σ` から `Γ, A∨B, Δ ⊢ Σ` を導く。ただし、`Σ` は1個または0個の論理式の列。

LJは直観論理において健全かつ完全であり、LKと同様のカット除去証明が存在します。

まとめ

シークエント計算LKは、論理的な推論を形式的に行うための強力な手法であり、その規則や特性を理解することで、より深く論理の世界を理解することができます。また、LJのように、わずかな修正で別の論理体系を構築することも可能です。これらの知識は、証明論や数理論理学だけでなく、計算機科学など幅広い分野で応用されています。

参考文献

Girard, Jean-Yves; Paul Taylor, Yves Lafont (1990年) [1989年]. Proofs and Types. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7).
Gentzen, Gerhard (1934). “Untersuchungen über das logische Schließen. I”. Mathematische Zeitschrift 39 (2): pp. 176-210.
Gentzen, Gerhard (1935). “Untersuchungen über das logische Schließen. II”. Mathematische Zeitschrift 39 (3): pp. 405-431.
Gentzen, Gerhard (1969). M. E. Szabo. ed. Collected Papers of Gerhard Gentzen. North-Holland.

関連項目

演繹定理

もう一度検索