シークエント

sequent

$ A_m, B_nを論理式の並びとした時、以下の形の式をシーケントと呼ぶ

$ A_1,\cdots,A_m \vdash B_1,\cdots,B_n

だたし、$ m,n\ge0

これに以下のような論理式を対応させる

$ A_1\land\cdots\land A_m \to B_1\lor\cdots\lor B_n

シーケントの真偽は、それに対応する論理式の真偽によって定義する

特に

$ m=0のとき、

$ A_1\land\cdots\land A_mは$ \topと考えられる

$ \vdash B_1,\cdots,B_n

仮定無しで、無条件に$ B_1\lor,\cdots,\lor B_nが導かれる、という意味

$ n=0のとき

$ B_1\lor\cdots\lor B_nは$ \botであると考えられる

$ A_1,\cdots,A_m\vdash

$ A_1から$ A_mまでを仮定すると矛盾が導かれる、という意味

$ m,n=0のとき

$ \vdash　

$ \top\to\bot

これは$ \botと同値

無条件に矛盾が導かれる、という意味

参考

かなり丁寧に色々書かれている