シークエント計算
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/06/24 19:20 UTC 版)
シークエント計算（シークエントけいさん、英: Sequent calculus）は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。
シークエント計算とその概念全般は証明論や数理論理学において重要な意味を持つ。以下では LK について解説する。
LK
シークエント計算ではシークエントの列で証明が記述され、各シークエントは証明過程で既に出現したシークエントに後述する推論規則を適用することで導出される（シークエントとは、命題群の論理積を前提とし、別の命題群の論理和を帰結とする論理的帰結関係を表す論理式の並びである）。
歴史
シークエント計算 LK は1934年、ゲルハルト・ゲンツェンが自然演繹を研究する道具として生み出した。その後、論理導出を行うのに非常に有効であることから普及した。LK（エルケー、エルカー） という名称はドイツ語の Logischer Kalkül（論理計算）に由来する。
LK の推論規則
ここでは、以下のような記法を用いる:
- 横線の上の論理式が与えられたとき、横線の下の論理式が推論によって導出されることを示す。
この導出は構文的計算の厳密に形式的な構造を強調している。例えば、上述の右論理規則は常にシークエントの右辺の最初の論理式に適用されている。この厳格な推論は最初は分かりにくいかもしれないが、形式論理における「文法」と「意味」の根本的な違いを示している。A ∨ ¬A という論理式と ¬A ∨ A という論理式は同じ「意味」だが、形式的な導出過程においては異なるものとして扱われる。しかし、推論をより簡単にするために補題（lemma）すなわち何らかの標準的な導出をもたらす事前定義された図式を導入することもある。例えば、以下のような変換がある。
この推論を導出する規則適用過程が分かっていれば、これを証明の中で略記法として使うことができる。しかし、よい補題は証明を読みやすくするが、かえって複雑化させる場合もあり、その選択は単純ではない。これは特に証明論を使った自動化演繹で重要となる。
構造規則
構造規則にはもう少し説明が必要である。規則の名称は Weakening (W)、Contraction (C)、Permutation (P) であり、日本語で言えばそれぞれ「弱化規則」、「縮約規則」、「転置規則」である。
弱化規則は任意の要素を付け加える。直観的には前提に何かを加えるというのは証明でもよくあることで自然である。帰結は要素の論理和となっているため、どちらかが成り立っていればよいため、証明されていない式を追加しても成り立つのである。
縮約規則と転置規則は、記述順序（転置規則）や同じ式が複数個登場すること（縮約規則）が問題とならないことを示している。従って、列ではなく集合とみなすことができる。
シークエント計算から構造規則の一部を除いたものを部分構造論理と呼ぶ。この場合、逆に列としての意味を重視する。
LK の特性
この規則体系は一階述語論理において健全かつ完全である。すなわち、 が上記規則群から導出される場合に限って、前提 Γ () から命題 A が意味論的に導かれる。
シークエント計算では、カット除去定理が許される。これをゲンツェンの Hauptsatz（主定理）とも呼ぶ。
派生
上述の規則群は LK の本質を変えることなく修正可能である。そのような修正を加えた体系も LK と呼ばれる。
まず、上述の通り、シークエント群を集合や多重集合と見ることもできる。この場合、転置規則と（集合の場合） 縮約規則は陳腐化する。
弱化規則は公理 (I) を Γ, A A, Δ という任意のシークエントが導出されるように修正することで許容される。これは、任意のコンテキストで、A ならば A であること意味している。導出の途中に出現する弱化規則は導出開始直後に実施できるようになる。これはボトムアップの証明で特に便利な変形である。
これとは別に、コンテキストを規則内で分ける方法を変更することもある。(∧R)、(∨L)、(→L) は下から上に適用する場合、コンテキストを Γ と Σ にどうにかして分けることになる。縮約規則を下から上に適用すれば、これらが重複してもよいので、常に全コンテキストが両方の分岐に適用されるとしてもよい。そうすると、重要なコンテキストを省いてしまう危険がなくなる。不要なコンテキストは後から弱化規則を適用することで削除できる。
これらの変形を施しても LK とは本質的には違わず、相互に変換が可能である。
LJ
LK の規則に少しだけ変更を加えることで、直観論理の証明体系となる。この場合、直観主義的シークエントになるよう制限を加え、推論規則はこの制限が保たれるように修正を加える。たとえば、規則 (∨L) には以下のような修正を加える。
ここで は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
- 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. ISBN 0-7204-2254-X - 英訳の論文集。
