シークエント
多くの証明系は、あるシークエントから別のシークエントを導く方法を提供している。そのための規則は、シークエントのリストを水平な線の上と下に記述した形式で示される。この規則は、線の上にあるシークエントが全て真であれば、線の下にあるシークエントも全て真であることを意味する。
規則の典型例は次の通り。
Γ ⊢ Σ Γ , α ⊢ Σ α , Γ ⊢ Σ {\displaystyle {\frac {\Gamma \vdash \Sigma }{\begin{matrix}\Gamma ,\alpha \vdash \Sigma &\alpha ,\Gamma \vdash \Sigma \end{matrix}}}}
これは、Γ から Σ を導けるなら、Γ に α を追加したものからも導けることを示している。
ギリシア文字の大文字は(空を含む)論理式の列を表すのに使われることが多い。[Γ, Σ] は Γ と Σ の縮約 (contraction) を意味し、Γ または Σ に現れる論理式のリストを意味する(ただし、同じものは省略される)。