シークエント計算のソースを表示

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

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

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

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

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

{| border="0" cellpadding="5" style="text-align: center;"
!公理:!!カット:
|-
|
 <math> \cfrac{\qquad }{ A \vdash A} \quad (I) </math>
|
 <math> 
 \cfrac{\Gamma \vdash \Delta, A \qquad A, \Sigma \vdash \Pi} {\Gamma, \Sigma \vdash \Delta, \Pi} \quad (\mathit{Cut})
 </math>
|-
!左論理規則:!!右論理規則:
|-
|
 <math> \cfrac{\Gamma, A \vdash \Delta} {\Gamma, A \land B \vdash \Delta} \quad ({\land}L_1)
 </math>
|
 <math> \cfrac{\Gamma \vdash A, \Delta}{\Gamma \vdash A \lor B, \Delta} \quad ({\lor}R_1)
 </math>
|-
|
 <math> \cfrac{\Gamma, B \vdash \Delta}{\Gamma, A \land B \vdash \Delta} \quad ({\land}L_2)
 </math>
|
 <math> \cfrac{\Gamma \vdash B, \Delta}{\Gamma \vdash A \lor B, \Delta} \quad ({\lor}R_2)
 </math>
|-
|
 <math> \cfrac{\Gamma, A \vdash \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A \lor B \vdash \Delta, \Pi} \quad ({\lor}L)
 </math>
|
 <math> \cfrac{\Gamma \vdash A, \Delta \qquad \Sigma \vdash B, \Pi}{\Gamma, \Sigma \vdash A \land B, \Delta, \Pi} \quad ({\land}R)
 </math>
|-
|
 <math>
 \cfrac{\Gamma \vdash A, \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A\rightarrow B \vdash \Delta, \Pi} \quad ({\rightarrow }L)
 </math>
|
 <math>
 \cfrac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} \quad ({\rightarrow}R)
 </math>
|-
|
 <math>
 \cfrac{\Gamma \vdash A, \Delta}{\Gamma, \lnot A \vdash \Delta} \quad ({\lnot}L)
 </math>
|
 <math>
 \cfrac{\Gamma, A \vdash \Delta}{\Gamma \vdash \lnot A, \Delta} \quad ({\lnot}R)
 </math>
|-
|
 <math>
  \cfrac{\Gamma, A[t/x] \vdash \Delta}{\Gamma, \forall x A \vdash \Delta} \quad ({\forall}L)
  </math>
|
 <math>
  \cfrac{\Gamma \vdash A[y/x], \Delta}{\Gamma \vdash \forall x A, \Delta} \quad ({\forall}R) 
  </math>
|-
|
 <math>
  \cfrac{\Gamma, A[y/x] \vdash \Delta}{\Gamma, \exist x A \vdash \Delta} \quad ({\exist}L)
  </math>
|
 <math>
  \cfrac{\Gamma \vdash A[t/x], \Delta}{\Gamma \vdash \exist x A, \Delta} \quad ({\exist}R)
  </math>
|-!左構造規則:!右構造規則:
|-
|
 <math>
 \cfrac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{WL})
 </math>
|
 <math>
 \cfrac{\Gamma \vdash \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{WR})
 </math>
|-
|
 <math>
 \cfrac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{CL})
 </math>
|
 <math>
 \cfrac{\Gamma \vdash A, A, \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{CR})
 </math>
|-
|
 <math>
 \cfrac{\Gamma_1, A, B, \Gamma_2 \vdash \Delta}{\Gamma_1, B, A, \Gamma_2 \vdash \Delta} \quad (\mathit{PL})
 </math>
|
 <math>
 \cfrac{\Gamma \vdash \Delta_1, A, B, \Delta_2}{\Gamma \vdash \Delta_1, B, A, \Delta_2} \quad (\mathit{PR})
 </math>
|}

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

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

{| border="0" cellpadding="5" style="text-align: center;"
|-
|
 <math>
   \cfrac{\Gamma, A \vdash \Delta}{\Gamma, \exist x A \vdash \Delta} \quad ({\exist}L)
   </math>
|
 <math>
   \cfrac{\Gamma \vdash A, \Delta}{\Gamma \vdash \forall x A, \Delta} \quad ({\forall}R) 
   </math>
|}
制約: (∃L) と (∀R) の規則において、変項 <math>x</math> は <math>\Gamma,\Delta</math> に自由出現をもたない。

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

形式化されているものの、これらの規則は古典論理的に直観的に読み解くことができる。例えば、(∧L<sub>1</sub>) 規則を見てみよう。これは、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 であるという自明なことを意味しているにすぎない。

=== 導出例 ===
例として <math>\vdash</math>(A ∨ ¬A) すなわち[[排中律]]の導出過程を示す。

[[ファイル:Excluded_middle_proof.png|center]]

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

<div style="text-align:center;"><math>
\cfrac {\Gamma \vdash A \lor B, \Delta} {\Gamma \vdash B \lor A, \Delta}
</math></div>

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

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

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

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

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

=== LK の特性 ===
この規則体系は一階述語論理において[[健全性|健全]]かつ完全である。すなわち、<math>\Gamma \vdash A</math> が上記規則群から導出される場合に限って、前提 Γ (<math>\Gamma \vDash A</math>) から命題 A が[[プログラム意味論|意味論]]的に導かれる。

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

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

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

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

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

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

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

{{Indent|<math>
 \cfrac{\Gamma, A \vdash \Delta \qquad \Sigma, B \vdash \Delta }{\Gamma, \Sigma, A \lor B \vdash \Delta} \quad ({\lor}L)
</math>}}

ここで <math>\Delta</math> は1個または0個の論理式の列である。

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

== 参考文献 ==
* {{cite book | first=Jean-Yves | last=Girard | coauthors=Paul Taylor, Yves Lafont | title=Proofs and Types | publisher=Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7) | date=1990年 | origyear=1989年 | id=ISBN 0-521-37181-3 | url= http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html}}
* {{Cite journal|last=Gentzen|first=Gerhard|authorlink=ゲルハルト・ゲンツェン|title=Untersuchungen über das logische Schließen. I|journal=Mathematische Zeitschrift|volume=39 (2)|date=1934|publisher=|pages=pp. 176-210|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?GDZPPN002375508}}
* {{Cite journal|last=Gentzen|first=Gerhard|authorlink=ゲルハルト・ゲンツェン|title=Untersuchungen über das logische Schließen. II|journal=Mathematische Zeitschrift|volume=39 (3)|date=1935|publisher=|pages=pp. 405-431|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?GDZPPN002375605}}
* {{Cite book|last=Gentzen|first=Gerhard|authorlink=ゲルハルト・ゲンツェン|editor=M. E. Szabo|date=1969|title=Collected Papers of Gerhard Gentzen|publisher=North-Holland|isbn=0-7204-2254-X}} - 英訳の論文集。

== 関連項目 ==
* [[演繹定理]]

{{DEFAULTSORT:しいくえんとけいさん}}
[[Category:論理計算]]
[[Category:数理論理学]]
[[Category:論理記号]]
[[Category:形式手法]]
[[Category:数学に関する記事]]
[[Category:自動定理証明]]