シークエント

ウィキペディア

シークエント

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/06/28 08:08 UTC 版)

この項目では、論理学の用語について説明しています。同名のコンピュータ企業については「シークエント・コンピュータ」をご覧ください。

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

定義

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

${\displaystyle \Gamma \vdash \Sigma }$

ウィキペディア小見出し辞書

シークエント

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/12/29 05:00 UTC 版)

「カット除去定理」の記事における「シークエント」の解説

シークエントは複数の文からなる論理表現であり、 A , B , C , … ⊢ P , Q , R , … という形式をとる。これは、直観的には 「A かつ B かつ C かつ… を仮定すれば、P または Q または R または… が証明可能である」 という意味に理解することができる（ここで左辺が論理積で、右辺は論理和であることに注意されたい）。前提である左辺は任意個の論理式からなり、左辺が空のシークエントが証明できた場合、その右辺は無前提に主張可能なトートロジーだということになる。逆に、結論である右辺が空となるなら、左辺は矛盾していると言える。LK（古典論理）では、右辺もまた任意個の論理式からなるが、LJ（直観論理）では、右辺には多くとも一つの文しか置くことが許されない。右辺に複数の論理式を置けることと、右縮約規則があるときに排中律が成り立つこととは等価である。ただし、シークエント計算は非常に表現能力が高く、右辺に多数の論理式のある直観論理のシークエント計算も存在する。Jean-Yves Girard の論理体系 LC においては、右辺に高々一個の論理式しか持たない古典論理の自然な定式化も容易に得られている。ここで鍵となるのは、論理的な推論規則と構造に関する推論規則との相互作用である。