シークエント (Γ ⊢ Δ)

シークエントΓ⊢Δは、仮定の集合Γから結論側Δの少なくとも一つが導けるという関係を表す。シークエント計算では、式の構造に沿った規則で証明を分解する。

仕組みと確認

左右の文脈、構造規則、結合子ごとの左規則・右規則を明記し、証明木の各ノードを検査する。アクセス条件やポリシーを扱う場合も、前提・許可される結論・例外を分ける。

限界と注意点

Γ⊢φとΓ⊨φは構文的導出と意味的帰結である。空の結論、複数結論、弱化や縮約を許すかは体系の定義に依存する。