自然演繹のシーケント計算について、最小限の基本則から完全性を示す。

命題論理

統語論: アルファベットは {￢,∧,p1,p2,....}および括弧。その他の真理関数は以下で定義: p∨q=￢(￢p∧￢q), p→q=￢(p∧￢q), p↔q=(p→q)∧(q→p), ⊥=p1∧￢p1, ⊤=￢⊥ 。また、Fを論理式全体、2^Fをそのべき集合、PV :={p1,p2,...} とする。

意味論: 値付け w: PV→{0,1} および (真理関数￢) ↦ (ブール関数￢), (真理関数∧) ↦ (ブール関数∧) で式の意味を定める。こうすることで、∨,→,↔に関しても対応するブール関数が対応づく。式の集合X のすべての元に 1 を値付ける値付けw において、式αも 1 に値付けられる 2^F×F 上の関係を、X⊨α とかく（注：X⊨α,β は X⊨α かつ X⊨β の略記。X⊨Yも同様）。特にX が空集合のとき ⊨α と記載しこれは「αは妥当式である」と読める。

基本則と派生則: (IS)(MR)(EFQ)(CASE)(∧I)(∧E)の6つの導出規則で十分。

(IS) 前提なしに α ⊢ α
(MR) X⊢α ⇒ X'⊢α where X ⊆ X'
(EFQ) X⊢α,￢α ⇒ X⊢β
(CASE) X,α⊢β & X,￢α⊢β ⇒ X⊢β
(∧I) X⊢α,β ⇒ X⊢α∧β; (∧E) X⊢α∧β ⇒ X⊢α,β

証明の際に極めてよく使う派生規則を記載:

(￢E) X,￢α ⊢ α ⇒ X⊢α      
(RAA) X,￢α ⊢ β,￢β ⇒ X⊢α  注: 背理法とも。 (RAA') X,α ⊢ β,￢β ⇒ X⊢￢α
(DT) X⊢α→β ⇔ X,α ⊢β
(CUT) X⊢α & X,α⊢β ⇒ X⊢β
(DNE/DNI) X⊢α ⇔ X⊢￢￢α

完全性: X⊢α ⇔ X⊨αの示し方。⇒は、健全性と呼ばれ 妥当性が推論規則において保存されることから帰納的に示される。⇐は 対偶 X⊬α ⇒ X⊭αを考える。X⊬α は (C+) により X∪￢α が整合であることを示すので、(lindenbaum) より極大整合 Y に拡大すると(cs)により充足可能性と結びつく。その結果 Y の部分集合 X∪￢α が充足可能であることが示され X⊭αが示される。

(C+) X⊢α ⇔ Cons(X,￢α); (C-) X⊢￢α ⇔ ￢Cons(X, α)
(lindenbaum) X が整合なら極大整合 Y⊇X が存在
(cs) 極大整合なら否定完全で充足可能

証明のポイントは、整合性と充足性を結びつける部分の「非常にシンプルな」モデル構築である。Xが極大整合なら帰結関係に閉じているので、2つのルール [∧] α∧β∈X ⇔ α,β∈X; [￢] ￢α∈X ⇔ α∉X さえ満たしていればよいとわかる（別の証明体系の道）。