シークエント計算

シークエント計算（シークエントけいさん、英: Sequent calculus）は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。

シークエント計算とその概念全般は証明論や数理論理学において重要な意味を持つ。以下では LK について解説する。

LK

シークエント計算ではシークエントの列で証明が記述され、各シークエントは証明過程で既に出現したシークエントに後述する推論規則を適用することで導出される（シークエントとは、命題群の論理積を前提とし、別の命題群の論理和を帰結とする論理的帰結関係を表す論理式の並びである）。

歴史

シークエント計算 LK は1934年、ゲルハルト・ゲンツェンが自然演繹を研究する道具として生み出した。その後、論理導出を行うのに非常に有効であることから普及した。LK（エルケー、エルカー）という名称はドイツ語の Logischer Kalkül（論理計算）に由来する。

LK の推論規則

ここでは、以下のような記法を用いる:

横線の上の論理式が与えられたとき、横線の下の論理式が推論によって導出されることを示す。
$A$ や $B$ は一階述語論理の論理式を表す（命題論理の論理式に限定する場合もある）。
$\Gamma ,\Delta ,\Sigma$ や $\Pi$ は有限個（0個もありうる）の論理式の列であり、コンテキスト（文脈）と呼ぶ。
$t$ は任意の項を意味する。
$A[t/v]$ は $A$ 内の変項 $v$ の全ての自由出現を項 $t$ で置換した論理式を表すが、 $t,v,A$ は「 $t$ 内のいかなる変項のいかなる自由出現もこの置換によって新たに束縛されない」という（代入可能）条件を満たすものとする。たとえば、 $\forall x(p(x,v))$ （ $p$ は 2 項述語、 $x,v$ は異なる変項）の $v$ の自由出現を $x$ で置換することは許されない。
$x$ や $y$ は（同じでもよい）変項を表す。
量化子 $\forall$ や $\exists$ で束縛されない変項を自由変項と呼ぶ。
$WL$ は Weakening Left、 $WR$ は Weakening Right、 $CL$ と $CR$ は Contraction、 $PL$ と $PR$ は Permutation の略である。

公理:	カット:
${\cfrac {\qquad }{A\vdash A}}\quad (I)$	${\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})$
左論理規則:	右論理規則:
${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})$	${\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})$
${\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})$	${\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})$
${\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}\quad ({\lor }L)$	${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma \vdash B,\Pi }{\Gamma ,\Sigma \vdash A\land B,\Delta ,\Pi }}\quad ({\land }R)$
${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)$	${\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)$
${\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)$	${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)$
${\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)$	${\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)$
${\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)$	${\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)$
${\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})$	${\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})$
${\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})$	${\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})$
${\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})$	${\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})$

制約: (∃L) と (∀R) の規則において、変項 $y$ は $\Gamma ,\exists xA,\Delta$ と $\Gamma ,\forall xA,\Delta$ に自由出現をもたない。

なお、(∃L) と (∀R) の規則、および、制約は次を採用してもよい。

 ${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)$

 ${\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)$

制約: (∃L) と (∀R) の規則において、変項 $x$ は $\Gamma ,\Delta$ に自由出現をもたない。

直観的説明

上記の規則群は「論理規則」と「構造規則」に分けられる。論理規則は帰結関係 $\vdash$ の右辺か左辺に新たな論理式を導入する。一方、構造規則はシークエントの構造を操作し、論理式の正確な形を無視する。例外として同一性の公理 (I) とカット規則 (Cut) がある。

形式化されているものの、これらの規則は古典論理的に直観的に読み解くことができる。例えば、(∧L₁) 規則を見てみよう。これは、A を含む論理式の列から Δ が証明される場合は常に A∧B という（より強い）仮定からも Δ が導かれることを示している。同様に、(¬R) 規則は Γ と A によって Δ が導かれるなら、Γ のみから Δ が真または A が偽であること（A が成り立たない）が導かれることを意味する。どの規則もこのように解釈可能である。

量化子の規則に関する直観的説明として、(∀R) 規則を見てみよう。もちろん、A[y/x] が真であるという事実だけから ∀x A が成り立つとは一般には結論できない。しかしながら、変項 y がどこにも言及されない場合（すなわち、他の論理式に影響を与えることなく自由に選べる場合）、A[y/x] は任意の y の値について成り立つと見なすことができる。他の規則も同様に解釈可能である。

これら規則を述語論理における正当な導出と見なさず、与えられた論理式について証明を構築するための手順と見ることもできる。この場合、規則を下から上に適用していく。例えば、(∧R) では、Γ と Σ という前提から A∧B が帰結されることを証明するには、それぞれ Γ から A が帰結され、Σ から B が帰結されればよい。ただし、先行条件をどのように Γ と Σ に分ければよいかは明らかではない。しかし、先行条件が有限であれば、考慮すべき組合せも有限である。これは証明論における組合せ的証明操作も示している。すなわち、A と B の両方を証明することで A∧B の証明を構築できる。

これらの規則のほとんどは、どう証明すればよいかを示しているが、カット規則だけは異なる。カット規則 (Cut) は、論理式 A が帰結となり、同時に他の帰結の前提にもなる場合、A を除いて論理的帰結関係を結合することができることを示している。証明をボトムアップで行う場合、A を具体的に何にするかという問題が生じる（横棒の下に出現しないため）。この問題はカット除去定理で扱われる。

同一性の公理 (I) もある意味で特殊である。直観的には A ならば A であるという自明なことを意味しているにすぎない。

導出例

例として $\vdash$ (A ∨ ¬A) すなわち排中律の導出過程を示す。

この導出は構文的計算の厳密に形式的な構造を強調している。例えば、上述の右論理規則は常にシークエントの右辺の最初の論理式に適用されている。この厳格な推論は最初は分かりにくいかもしれないが、形式論理における「文法」と「意味」の根本的な違いを示している。A ∨ ¬A という論理式と ¬A ∨ A という論理式は同じ「意味」だが、形式的な導出過程においては異なるものとして扱われる。しかし、推論をより簡単にするために補題（lemma）すなわち何らかの標準的な導出をもたらす事前定義された図式を導入することもある。例えば、以下のような変換がある。

{\cfrac {\Gamma \vdash A\lor B,\Delta }{\Gamma \vdash B\lor A,\Delta }}

この推論を導出する規則適用過程が分かっていれば、これを証明の中で略記法として使うことができる。しかし、よい補題は証明を読みやすくするが、かえって複雑化させる場合もあり、その選択は単純ではない。これは特に証明論を使った自動化演繹で重要となる。

構造規則

構造規則にはもう少し説明が必要である。規則の名称は Weakening (W)、Contraction (C)、Permutation (P) であり、日本語で言えばそれぞれ「弱化規則」、「縮約規則」、「転置規則」である。

弱化規則は任意の要素を付け加える。直観的には前提に何かを加えるというのは証明でもよくあることで自然である。帰結は要素の論理和となっているため、どちらかが成り立っていればよいため、証明されていない式を追加しても成り立つのである。

縮約規則と転置規則は、記述順序（転置規則）や同じ式が複数個登場すること（縮約規則）が問題とならないことを示している。従って、列ではなく集合とみなすことができる。

シークエント計算から構造規則の一部を除いたものを部分構造論理と呼ぶ。この場合、逆に列としての意味を重視する。

LK の特性

この規則体系は一階述語論理において健全かつ完全である。すなわち、 $\Gamma \vdash A$ が上記規則群から導出される場合に限って、前提 Γ ( $\Gamma \vDash A$ ) から命題 A が意味論的に導かれる。

シークエント計算では、カット除去定理が許される。これをゲンツェンの Hauptsatz（主定理）とも呼ぶ。

派生

上述の規則群は LK の本質を変えることなく修正可能である。そのような修正を加えた体系も LK と呼ばれる。

まず、上述の通り、シークエント群を集合や多重集合と見ることもできる。この場合、転置規則と（集合の場合）縮約規則は陳腐化する。

弱化規則は公理 (I) を Γ, A $\vdash$ A, Δ という任意のシークエントが導出されるように修正することで許容される。これは、任意のコンテキストで、A ならば A であること意味している。導出の途中に出現する弱化規則は導出開始直後に実施できるようになる。これはボトムアップの証明で特に便利な変形である。

これとは別に、コンテキストを規則内で分ける方法を変更することもある。(∧R)、(∨L)、(→L) は下から上に適用する場合、コンテキストを Γ と Σ にどうにかして分けることになる。縮約規則を下から上に適用すれば、これらが重複してもよいので、常に全コンテキストが両方の分岐に適用されるとしてもよい。そうすると、重要なコンテキストを省いてしまう危険がなくなる。不要なコンテキストは後から弱化規則を適用することで削除できる。

これらの変形を施しても LK とは本質的には違わず、相互に変換が可能である。

LJ

LK の規則に少しだけ変更を加えることで、直観論理の証明体系となる。この場合、直観主義的シークエントになるよう制限を加え、推論規則はこの制限が保たれるように修正を加える。たとえば、規則 (∨L) には以下のような修正を加える。

${\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Delta }{\Gamma ,\Sigma ,A\lor B\vdash \Delta }}\quad ({\lor }L)$

ここで $\Delta$ は1個または0個の論理式の列である。

このような体系を LJ（エルジェー、エルヨット）と呼ぶ。これは直観論理においては健全かつ完全な体系であり、LK と同様なカット除去証明が存在する。

参考文献

Girard, Jean-Yves; Paul Taylor, Yves Lafont (1990年) [1989年]. Proofs and Types. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7). ISBN 0-521-37181-3. http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html
Gentzen, Gerhard (1934). “Untersuchungen über das logische Schließen. I”. Mathematische Zeitschrift 39 (2): pp. 176-210. http://gdz.sub.uni-goettingen.de/dms/resolveppn/?GDZPPN002375508.
Gentzen, Gerhard (1935). “Untersuchungen über das logische Schließen. II”. Mathematische Zeitschrift 39 (3): pp. 405-431. http://gdz.sub.uni-goettingen.de/dms/resolveppn/?GDZPPN002375605.
Gentzen, Gerhard (1969). M. E. Szabo. ed. Collected Papers of Gerhard Gentzen. North-Holland. ISBN 0-7204-2254-X - 英訳の論文集。