直観的な意味
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 10:08 UTC 版)
上記のようなシークエントの直観的な意味は、Γ を前提としたとき、結論である Σ を証明可能ということである。古典的な用法では、ターンスタイルの左辺にある論理式列は論理積的に解釈され、右辺の論理式列は論理和的に解釈される。つまり、Γ の全論理式が成り立つとき、Σ のうちの少なくとも1つの論理式が成り立つ。後件が空の場合、そのシークエントは偽と解釈される。すなわち Γ ⊢ {\displaystyle \Gamma \vdash } という形式は、Γ が偽であることを証明することを意味し、従って一貫性がない。一方、前件が空の場合、そのシークエントは真と見なされる。すなわち ⊢ Σ {\displaystyle \vdash \Sigma } という形式は、何の前提もなしに Σ が成り立ち、（論理和として）恒真であることを意味する。Γ が空の形式のシークエントを論理的表明 (logical assertion) と呼ぶ。 しかし、以上の解釈は単に教育的な意味しかない。形式的証明は純粋に統語的であるため、シークエントの意味は実際の推論規則を提供する計算法の属性として与えられるものである。 そのような技術的に厳密な定義に対して矛盾がなければ、入門的な論理形式としてシークエントを説明できる。Γ は論理操作の出発点となる前提群を表す。例えば、「ソクラテスは人間だ」とか「全ての人間は死ぬ」がそれにあたる。Σ は、それらの前提群から導かれる論理的帰結を表している。先の前提の例からは「ソクラテスは死ぬ」という事実が導かれ、これがターンスタイルの右辺の Σ に置かれることになる。このような意味において、 ⊢ {\displaystyle \vdash } は推論過程を表し、自然言語で言えば「従って」という意味となる。
※この「直観的な意味」の解説は、「シークエント」の解説の一部です。
「直観的な意味」を含む「シークエント」の記事については、「シークエント」の概要を参照ください。
- 直観的な意味のページへのリンク
