シークエント
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/12/29 05:00 UTC 版)
シークエントは複数の文からなる論理表現であり、 A , B , C , … ⊢ P , Q , R , … {\displaystyle A,B,C,\ldots \vdash P,Q,R,\ldots } という形式をとる。これは、直観的には 「A かつ B かつ C かつ… を仮定すれば、P または Q または R または… が証明可能である」 という意味に理解することができる（ここで左辺が論理積で、右辺は論理和であることに注意されたい）。前提である左辺は任意個の論理式からなり、左辺が空のシークエントが証明できた場合、その右辺は無前提に主張可能なトートロジーだということになる。逆に、結論である右辺が空となるなら、左辺は矛盾していると言える。LK（古典論理）では、右辺もまた任意個の論理式からなるが、LJ（直観論理）では、右辺には多くとも一つの文しか置くことが許されない。右辺に複数の論理式を置けることと、右縮約規則があるときに排中律が成り立つこととは等価である。ただし、シークエント計算は非常に表現能力が高く、右辺に多数の論理式のある直観論理のシークエント計算も存在する。Jean-Yves Girard の論理体系 LC においては、右辺に高々一個の論理式しか持たない古典論理の自然な定式化も容易に得られている。ここで鍵となるのは、論理的な推論規則と構造に関する推論規則との相互作用である。
※この「シークエント」の解説は、「カット除去定理」の解説の一部です。
「シークエント」を含む「カット除去定理」の記事については、「カット除去定理」の概要を参照ください。
ウィキペディア小見出し辞書の「シークエント」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
このページでは「ウィキペディア小見出し辞書」からシークエントを検索した結果を表示しています。
Weblioに収録されているすべての辞書からシークエントを検索する場合は、下記のリンクをクリックしてください。
全ての辞書からシークエント
を検索
Weblioに収録されているすべての辞書からシークエントを検索する場合は、下記のリンクをクリックしてください。
全ての辞書からシークエント
を検索
- シークエントのページへのリンク
