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と同値

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

参考

『情報科学における論理』 p.23~

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