シークエント

シークエント（英: Sequent）あるいは推件式（すいけんしき）とは、演繹による証明過程を示すためによく使われる形式表現である。

定義

シークエントは次の形式を持つ。

$\Gamma \vdash \Sigma$

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

直観的な意味

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

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

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

例

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

$\phi ,\psi \vdash \alpha ,\beta$

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

特性

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

規則

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

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

${\frac {\Gamma \vdash \Sigma }{\begin{matrix}\Gamma ,\alpha \vdash \Sigma &\alpha ,\Gamma \vdash \Sigma \end{matrix}}}$

これは、 $\Gamma$ から $\Sigma$ を導けるなら、 $\Gamma$ に α を追加したものからも導けることを示している。

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

派生

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

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

歴史

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

外部リンク

この記事は、クリエイティブ・コモンズ・ライセンス 表示-継承 3.0 非移植のもと提供されているオンライン数学辞典『PlanetMath』の項目Sequentの本文を含む