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

{{Otheruses|論理学の用語|同名のコンピュータ企業|シークエント・コンピュータ}}
'''シークエント'''（[[英語|英]]: '''Sequent'''）あるいは推件式（すいけんしき）とは、[[演繹]]による[[証明 (数学)|証明]]過程を示すためによく使われる形式表現である。

== 定義 ==
シークエントは次の形式を持つ。
{{Indent|<math>\Gamma\vdash\Sigma</math>}}

ここで、 <math>\Gamma</math> と <math>\Sigma</math> は[[論理式 (数学)|論理式]]の[[列 (数学)|列]]である（その個数と順序が重要である）。記号 <math>\vdash</math> は、ターンスタイル（turnstile、回転扉）あるいはティー (tee) と呼ばれ、意味的には「生成する」あるいは「証明する」と読まれる。これは言語内の記号ではなく、証明を論じる際のメタ言語内の記号である。シークエントにおいて、 <math>\Gamma</math> は前件 (antecedent)、 <math>\Sigma</math> は後件 (succedent) と呼ばれる。

== 直観的な意味 ==
上記のようなシークエントの直観的な意味は、 <math>\Gamma</math> を前提としたとき、結論である &Sigma; を証明可能ということである。古典的な用法では、ターンスタイルの左辺にある論理式列は[[論理積]]的に解釈され、右辺の論理式列は[[論理和]]的に解釈される。つまり、 <math>\Gamma</math> の全論理式が成り立つとき、 <math>\Sigma</math> のうちの少なくとも1つの論理式が成り立つ。後件が空の場合、そのシークエントは偽と解釈される。すなわち <math>\Gamma\vdash</math> という形式は、 <math>\Gamma</math> から偽が証明されること、したがって <math>\Gamma</math> が非整合的な列であることを意味する。一方、前件が空の場合、そのシークエントは真と見なされる。すなわち <math>\vdash\Sigma</math> という形式は、何の前提もなしに <math>\Sigma</math> が成り立ち、（論理和として）恒真であることを意味する。 <math>\Gamma</math> が空の形式のシークエントを'''論理的表明''' (logical assertion) と呼ぶ。

しかし、以上の解釈は単に教育的な意味しかない。形式的証明は純粋に[[統語論 (論理学)|統語的]]であるため、シークエントの[[意味論 (論理学)|意味]]は実際の[[推論規則]]を提供する計算法の属性として与えられるものである。

そのような技術的に厳密な定義に対して矛盾がなければ、入門的な論理形式としてシークエントを説明できる。 <math>\Gamma</math> は論理操作の出発点となる前提群を表す。例えば、「ソクラテスは人間だ」とか「全ての人間は死ぬ」がそれにあたる。 <math>\Sigma</math> は、それらの前提群から導かれる論理的帰結を表している。先の前提の例からは「ソクラテスは死ぬ」という事実が導かれ、これがターンスタイルの右辺の <math>\Sigma</math> に置かれることになる。このような意味において、<math>\vdash</math> は推論過程を表し、自然言語で言えば「従って」という意味となる。

== 例 ==
典型的なシークエントは、次のように記述される。

{{Indent|<math> \phi, \psi \vdash \alpha, \beta</math>}}

これは、つまり <math>\alpha</math> か <math>\beta</math> のいずれかが <math>\phi</math> および <math>\psi</math> から導かれることを意味する。

== 特性 ==
後件（右辺）にある論理式の少なくとも 1 つが真であると結論するためには、前件（左辺）にある論理式は全て真でなければならない。どちらかに論理式を追加するとシークエントは弱くなり、どちらかから論理式を削除するとシークエントは強くなる。

== 規則 ==
多くの証明系は、あるシークエントから別のシークエントを導く方法を提供している。そのための規則は、シークエントのリストを水平な線の上と下に記述した形式で示される。この規則は、線の上にあるシークエントが全て真であれば、線の下にあるシークエントも全て真であることを意味する。

規則の典型例は次の通り。

{{Indent|<math>\frac{\Gamma \vdash \Sigma}{\begin{matrix} \Gamma, \alpha \vdash \Sigma & \alpha, \Gamma \vdash \Sigma \end{matrix}}</math>}}

これは、 <math>\Gamma</math> から <math>\Sigma</math> を導けるなら、 <math>\Gamma</math> に ''&alpha;'' を追加したものからも導けることを示している。

ギリシア文字の大文字は（空を含む）論理式の列を表すのに使われることが多い。 <math>[\Gamma, \Sigma]</math> は <math>\Gamma</math> と <math>\Sigma</math> の縮約 (contraction) を意味し、 <math>\Gamma</math> または <math>\Sigma</math> に現れる論理式のリストを意味する（ただし、同じものは省略される）。

== 派生 ==
ここで示したシークエントの一般的記法は、様々に変形される場合がある。後件に高々 1 つの論理式しかない場合、そのシークエントを'''直観主義的シークエント'''と呼び、[[直観論理]]の計算で必要とされる。同様に、前件が単一の論理式のシークエントは、双対直観論理（[[矛盾許容論理]]の一種）で必要とされる。

多くの場合、論理式の並びではなく、[[多重集合]]や[[集合]]からなるものもシークエントと考えられる。この場合、論理式の個数も順序も重視されない。古典的な[[命題論理]]では、前提群から結論を導き出すのに、順序や個数は関係しない。しかし、[[部分構造論理]]では、順序や個数が非常に重要となる。

== 歴史 ==
歴史的には、シークエントは[[ゲルハルト・ゲンツェン]]が[[シークエント計算]]を記述するのに導入したものであった。ドイツ語で書かれた彼の論文では、"Sequenz" という単語が使われていた。しかし、その英訳である "[[列 (数学)|sequence]]" は、ドイツ語での "Folge" の訳として数学で広く使われていた。そこで、ドイツ語の "Sequenz" の訳語として "Sequent" という言葉が生み出された。

== 外部リンク ==
{{PlanetMath attribution|id=33502|title=Sequent}}

{{DEFAULTSORT:しいくえんと}}
[[Category:証明論]]
[[Category:論理式]]
[[Category:数学に関する記事]]