シークエント計算
上記の規則群は「論理規則」と「構造規則」に分けられる。論理規則は帰結関係 ⊢ {\displaystyle \vdash } の右辺か左辺に新たな論理式を導入する。一方、構造規則はシークエントの構造を操作し、論理式の正確な形を無視する。例外として同一性の公理 (I) とカット規則 (Cut) がある。
形式化されているものの、これらの規則は古典論理的に直観的に読み解くことができる。例えば、(∧L1) 規則を見てみよう。これは、A を含む論理式の列から Δ が証明される場合は常に A∧B という(より強い)仮定からも Δ が導かれることを示している。同様に、(¬R) 規則 は Γ と A によって Δ が導かれるなら、Γ のみから Δ が真または A が偽であること(A が成り立たない)が導かれることを意味する。どの規則もこのように解釈可能である。
量化子の規則に関する直観的説明として、(∀R) 規則を見てみよう。もちろん、A[y/x] が真であるという事実だけから ∀x A が成り立つとは一般には結論できない。しかしながら、変項 y がどこにも言及されない場合(すなわち、他の論理式に影響を与えることなく自由に選べる場合)、A[y/x] は任意の y の値について成り立つと見なすことができる。