シークエント計算
構造規則にはもう少し説明が必要である。規則の名称は Weakening (W)、Contraction (C)、Permutation (P) であり、日本語で言えばそれぞれ「弱化規則」、「縮約規則」、「転置規則」である。
弱化規則は任意の要素を付け加える。直観的には前提に何かを加えるというのは証明でもよくあることで自然である。帰結は要素の論理和となっているため、どちらかが成り立っていればよいため、証明されていない式を追加しても成り立つのである。
縮約規則と転置規則は、記述順序(転置規則)や同じ式が複数個登場すること(縮約規則)が問題とならないことを示している。従って、列ではなく集合とみなすことができる。
シークエント計算から構造規則の一部を除いたものを部分構造論理と呼ぶ。この場合、逆に列としての意味を重視する。
ここでは、以下のような記法を用いる:
横線の上の論理式が与えられたとき、横線の下の論理式が推論によって導出されることを示す。
A {\displaystyle A} や B {\displaystyle B} は一階述語論理の論理式を表す(命題論理の論理式に限定する場合もある)。
Γ , Δ , Σ {\displaystyle \Gamma ,\Delta ,\Sigma } や Π {\displaystyle \Pi } は有限個(0個もありうる)の論理式の列であり、コンテキスト(文脈)と呼ぶ。
t {\displaystyle t} は任意の項を意味する。
A [ t / v ] {\displaystyle A[t/v]} は A {\displaystyle A} 内の変項 v {\displaystyle v} の全ての自由出現を項 t {\displaystyle t} で置換した論理式を表すが、 t , v , A {\displaystyle t,v,A} は「 t {\displaystyle t} 内のいかなる変項のいかなる自由出現もこの置換によって新たに束縛されない」という(代入可能)条件を満たすものとする。たとえば、 ∀ x ( p ( x , v ) ) {\displaystyle \forall x(p(x,v))} ( p {\displaystyle p} は 2 項述語、 x , v {\displaystyle x,v} は異なる変項)の v {\displaystyle v} の自由出現を x {\displaystyle x} で置換することは許されない。
x {\displaystyle x} や y {\displaystyle y} は(同じでもよい)変項を表す。
量化子 ∀ {\displaystyle \forall } や ∃ {\displaystyle \exists } で束縛されない変項を自由変項と呼ぶ。
W L {\displaystyle WL} は Weakening Left、 W R {\displaystyle WR} は Weakening Right、 C L {\displaystyle CL} と C R {\displaystyle CR} は Contraction、 P L {\displaystyle PL} と P R {\displaystyle PR} は Permutation の略である。
制約: (∃L) と (∀R) の規則において、変項 y {\displaystyle y} は Γ , ∃ x A , Δ {\displaystyle \Gamma ,\exists xA,\Delta } と Γ , ∀ x A , Δ {\displaystyle \Gamma ,\forall xA,\Delta } に自由出現をもたない。
なお、(∃L) と (∀R) の規則、および、制約は次を採用してもよい。
制約: (∃L) と (∀R) の規則において、変項 x {\displaystyle x} は Γ , Δ {\displaystyle \Gamma ,\Delta } に自由出現をもたない。
例として ⊢ {\displaystyle \vdash } (A ∨ ¬A) すなわち排中律の導出過程を示す。
この導出は構文的計算の厳密に形式的な構造を強調している。例えば、上述の右論理規則は常にシークエントの右辺の最初の論理式に適用されている。この厳格な推論は最初は分かりにくいかもしれないが、形式論理における「文法」と「意味」の根本的な違いを示している。A ∨ ¬A という論理式と ¬A ∨ A という論理式は同じ「意味」だが、形式的な導出過程においては異なるものとして扱われる。しかし、推論をより簡単にするために補題(lemma)すなわち何らかの標準的な導出をもたらす事前定義された図式を導入することもある。例えば、以下のような変換がある。
この推論を導出する規則適用過程が分かっていれば、これを証明の中で略記法として使うことができる。しかし、よい補題は証明を読みやすくするが、かえって複雑化させる場合もあり、その選択は単純ではない。これは特に証明論を使った自動化演繹で重要となる。