この章ではシークェント計算による古典論理・直観主義論理の 形式化を紹介する．参考書として

1. 林晋「数理論理学」（コロナ社，1989）
2. 小野寛晰「情報科学における論理」（日本評論社，1994）
3. 松本和夫「数理論理学」（共立出版，初版1970，復刊2001）

目次

1. シークェントとは何か

2. シークェント計算による論理の形式化

3. 命題論理の形式化の完全性

総目次に戻る

1. シークェントとは何か

1.1 シークェントの定義

をシークェント（sequent）という． φ₁,…,φ_m をシークェントの左辺， ψ₁,…,ψ_n をシークェントの右辺と呼ぶ ことにする．なお，右辺が空のシークェント

や左辺が空のシークェント

も考える．両辺が空のシークェントを考えることもできるが， 以下では使わない．

【注意】自然演繹との関係から見れば，シークェントの区切り記号として ⇒の代わりに |- を用いて

とあらわす方が意味はわかりやすい（文献によってはそのような 表記法を採用しているものもある）．実際，あとでさまざまな 例によって示すように，シークェント計算で形式的に証明される シークェントは，⇒を |- に読み替えれば，いずれも自然演繹などで 形式的に証明される演繹関係に対応する．しかしながら， 公理系を設定して形式的理論を論じるような場合には（たとえば 数学基礎論への応用），公理系Ａから論理式（シークェント 計算の場合にはシークェント）φが導出されることを Ａ|-φ とあらわすことが普通なので，シークェントの区切り記号として 別のものを用いないと混乱が生じる．そのような意味でここでは シークェントの区切り記号として⇒を用いることにした． ⇒を含意の記号→と混同しないように注意されたい （含意記号として⊃を用いれば紛らわしさは改善される）．

1.2 シークェントの意味解釈

1. φ₁,…,φ_m ⇒ ψ₁, …, ψ_n
2. ⇒ ψ₁,…,ψ_n （左辺が空）
3. φ₁,…,φ_m ⇒ （右辺が空）

1. φ₁, …, φ_m のすべてが真ならば ψ₁, …, ψ_n のいずれかが真である
2. ψ₁, …, ψ_n のいずれかが真である
3. φ₁, …, φ_m のいずれかが偽である

1. φ₁∧…∧φ_m → ψ₁∨…∨ψ_n
2. Ｔ → ψ₁∨…∨ψ_n
3. φ₁∧…∧φ_m → ⊥

1. φ₁∧…∧φ_m → ψ₁∨…∨ψ_n
2. ψ₁∨…∨ψ_n
3. ¬(φ₁∧…∧φ_m)

【注意】⇒，→の左右でコンマの役割が非対称に見えるが， じつはむしろこれで完全に対称になっている．実際， 古典論理の意味解釈では

あるいは

というよう同値変形ができることである．これは数式

を「移項」によって

あるいは

に同値変形することに似ている（¬が - に相当する）． この同値変形はあとで説明するシークェント計算の推論規則に 組み込まれている．

1.3 古典論理におけるシークェントの意味解釈

Γ，Δで論理式の並び

シークェントΓ⇒Δの意味解釈においては，このΓ，Δを単一の論理式

につぶして Γ_*→Δ^* という論理式をつくり， それによって次のように意味解釈を行う．

命題論理の場合

Γ，Δに含まれる命題記号の真理値割り当て M が 与えられたとき，それに対するシークェント Γ⇒Δ の解釈 M[Γ⇒Δ]（すなわち真理値）を

M[Γ⇒Δ] = M[Γ_*→Δ^*]

と定義する（右辺の真理値は古典命題論理の論理式の意味解釈によって 決まる）．すべての真理値割り当てに対して真理値が常に真（T）の値をもつ シークェントは「恒真」であるという．特に， 初期シークェント φ⇒φ は恒真である．

述語論理の場合

L-構造の解釈 M が与えられたとき， それに対するシークェントΓ⇒Δの解釈 M[Γ⇒Δ]（すなわち M の 対象領域 D 上の述語）を

M[Γ⇒Δ] = M[Γ_*→Δ^*]

と定義する．

2. シークェント計算による論理の形式化

2.1 命題論理の形式化

初期シークェント

シークェント計算では公理系と呼ばれるものがない．その代わりに

φ⇒φ    （φは任意の論理式）

という形のシークェント（「初期シークェント」と呼ばれる） から出発して，下記の推論規則を適用することによって証明を行う．

LKとLJの違い

• LK: 任意の形のシークェントを許す
• LJ: 右辺が高々１個の論理式からなるシークェントのみを許す

証明の過程に現れるシークェントにもこれを要求する．

推論規則

推論規則は「構造に関する規則」と「論理結合子に関する規則」 の二種類に分かれる．以下ではLKの場合の規則を示す（Γ, Δ, Π, Σは コンマで区切られた論理式の並びであり，φ，ψは単一の論理式である）． LJの場合にはこれらの推論規則に現れるシークェントを右辺に論理式が 高々１個しか現れない（すなわちΓ⇒φあるいはΓ⇒という形をもつ） ものに限定する．

【構造に関する規則】

Γ⇒Δ φ,Γ⇒Δ （希釈左）		Γ⇒Δ Γ⇒Δ,φ （希釈右）
φ,φ,Γ⇒Δ φ,Γ⇒Δ （縮約左）		Γ⇒Δ,φ,φ Γ⇒Δ,φ （縮約右）
Γ,φ,ψ,Π⇒Δ Γ,ψ,φ,Π⇒Δ （交換左）		Γ⇒Δ,φ,ψ,Σ Γ⇒Δ,ψ,φ,Σ （交換右）
Γ⇒Δ,φ      φ,Π⇒Σ Γ,Π⇒Δ,Σ （カット）

【論理結合子に関する規則】

φ,Γ⇒Δ ψ,Γ⇒Δ    （∧左） φ∧ψ,Γ⇒Δ φ∧ψ,Γ⇒Δ	Γ⇒Δ,φ    Γ⇒Δ,ψ （∧右） Γ⇒Δ,φ∧ψ
φ,Γ⇒Δ    ψ,Γ⇒Δ （∨左） φ∨ψ,Γ⇒Δ	Γ⇒Δ,φ Γ⇒Δ,ψ    （∨右） Γ⇒Δ,φ∨ψ Γ⇒Δ,φ∨ψ
Γ⇒Δ,φ    ψ,Π⇒Σ （→左） φ→ψ,Γ,Π ⇒ Δ,Σ	φ,Γ⇒Δ,ψ （→右） Γ ⇒ Δ,φ→ψ
Γ⇒Δ,φ （¬左） ¬φ,Γ⇒Δ	φ,Γ⇒Δ （¬右） Γ⇒Δ,¬φ

これらの規則に基づく証明の簡単な例を示す．

【例１】⇒Φ→¬¬φ（二重否定の生成：LJで証明できる）

1: φ⇒φ （初期シークェント）

2: ¬φ,φ⇒（１¬左）

3: φ⇒¬¬φ （２¬右）

4: ⇒Φ→¬¬Φ（3→右）

【例２】⇒¬¬φ→φ（二重否定の除去：LKでないと証明できない）

1: φ⇒φ （初期シークェント）

2:⇒φ,¬φ （１¬右）

3: ¬¬φ⇒φ （２¬右）

4: ⇒¬¬Φ→Φ（3→右）

【例３】⇒φ∨¬φ（排中律：LKでないと証明できない）

1: φ⇒φ （初期シークェント）

2:⇒φ,¬φ （１¬右）

3:⇒φ,φ∨¬φ （２∨右）

4:⇒φ∨¬φ,φ （３交換右）

5:⇒φ∨¬φ,φ∨¬φ (４∨右）

6:⇒φ∨¬φ (５縮約右）

【例４】⇒φ∧(φ→ψ)→ψ（modus ponens：LJで証明できる）

1: φ⇒φ （初期シークェント）

2: ψ⇒ψ （初期シークェント）

3: φ,φ→ψ⇒ψ （１，２→左）

4: Φ∧(Φ→ψ),Φ⇒ψ（3∧左）

5: Φ,Φ∧(Φ→ψ)⇒ψ（4交換左）

6: Φ∧(Φ→ψ),Φ∧(Φ→ψ)⇒ψ（5∧左）

7: Φ∧(Φ→ψ)⇒ψ（6希釈左）

8: ⇒Φ∧(Φ→ψ)→ψ（7→右）

2.2 推論規則の意味・妥当性

まず「妥当性」の意味を明確にしよう．シークェントに対する推論規則はいずれも

1. 一つのシークェントから一つのシークェントを導出する	Γ1⇒Δ1 Γ⇒Δ
2. 二つのシークェントから一つのシークェントを導出する	Γ1⇒Δ1  Γ2⇒Δ2 Γ⇒Δ

のいずれかの形をもつ．これらが「妥当」であるとは， それぞれが任意の真理値割り当て M に対して

1. M[Γ₁⇒Δ₁] = T ならば M[Γ⇒Δ] = T
2. M[Γ₁⇒Δ₁] = T かつ Γ₂⇒Δ₂] = T ならば M[Γ⇒Δ] = T

という条件を満たすことを意味する．特に，恒真なシークェントから 妥当な推論規則によって導出されるシークェントはやはり恒真である． 初期シークェントは恒真だから，推論規則がすべて妥当であれば 形式的証明によって得られるシークェントはすべて恒真である （特に，LKは「健全」である）ということになる．以下で 確かめようとするのはこの性質である．

1. 構造に関する推論規則：妥当性はほとんど明らかだろう．

2. ∧左と∨右：¬左を考える．任意の真理値割り当て M に対して 上下のシークェントの真理値は

となるので，M[φ,Γ⇒Δ] = T のもとで M[φ∧ψ,Γ⇒Δ] = T であり， 推論規則の妥当性がわかる．∨右の妥当性も同様にして確かめられる．

3. ∨左と∧右：∧右を考える．任意の真理値割り当て M に対して 上側のシークェントの真理値は

となる．他方，下側のシークェントの真理値は

だが，→の書き換えと分配法則によって一般に

という同値変形ができるので

という等式が得られる．M[Γ⇒Δ,φ] = T かつ M[Γ⇒Δ,ψ] = T ならば この式の真理値は T に等しい．∧右の妥当性はこのようにして確かめられる． ∨左の場合も同様である．

4. →左：任意の真理値割り当て M に対して上側のシークェントの真理値は

となる．他方，下側のシークェントの真理値は

であるが，ここでも→の書き換えと結合法則によって一般に

という変形ができるので，

という等式が得られる．M[Γ⇒Δ,φ] = T かつ M[ψ,Π⇒Σ] = T ならば この式の真理値は T になる．このようにして→左の妥当性が確かめられる．

5. →右：任意の真理値割り当て M に対して上下のシークェントの真理値は

となる．これはともに M[¬Γ_*∨Δ^*∨¬φ∨ψ] に等しいので，推論規則の妥当性がわかる．

6. ¬左と¬右：¬左を考える．任意の真理値割り当て M に対して 上下のシークェントの真理値は

だが，これはともに M[¬φ∨¬Γ_*∨Δ^*] に等しいので，推論規則の妥当性がわかる． ¬右の妥当性も同様にして確かめられる．

2.3 証明の考え方

【例】ド・モルガンの法則

1. ⇒¬(φ∨ψ)→¬φ∧¬ψ
2. ⇒¬φ∧¬ψ→¬(φ∨ψ)
3. ⇒¬(φ∧ψ)→¬φ∨¬ψ
4. ⇒¬φ∨¬ψ→¬(φ∧ψ)

1. |- ¬(φ∨ψ)→¬φ∧¬ψ
2. |- ¬φ∧¬ψ→¬(φ∨ψ)
3. |- ¬(φ∧ψ)→¬φ∨¬ψ
4. |- ¬φ∨¬ψ→¬(φ∧ψ)

シークェント計算による証明の基本的戦略は「ゴールから逆に考える」 ということに尽きる．同様の考え方は自然演繹の場合にも有効だったが， 自然演繹の場合には「どのような仮定（あとで落とす）を選ぶか」という やや発見的な議論が要求された．それとは対照的に，シークェント計算は 命題論理に関する限り目標のシークェントから逆にたどることで ほぼ機械的に証明を書き下すことができる．

証明を書き下す一般的な手順の詳細は完全性定理の証明の際に説明するが， 要は，論理結合子に関する推論規則に注目し，それを逆向きに （つまり下から上へ）使って，シークェントを論理結合子の数の少ない シークェントに分解して行くのである．その様子は「木」の イメージとして描くことができる．この木（「分解木」という）の 「根」は目標のシークェントである．分解木は分解の操作を適用する ごとに成長し，末端（「葉」）のシークェントが論理結合子を 含まないものになった時点で成長を止める．末端のシークェントがいずれも 初期シークェントであれば，分解木を少し修正する（構造に関する推論規則を補う） ことによって，目標のシークェントの証明図が得られる．

このような方針に従って，ド・モルガンの法則に対する以下のような証明図 （これは一つの例である）が得られる．自然演繹による証明は普通の数学の証明に 似ているので，一行ずつ証明を書いて行く表記法を用いたが，シークェント計算 の場合には今述べた理由で証明図の方が考えやすい．

【例】⇒¬(φ∨ψ)→¬φ∧¬ψの証明

【例】⇒¬φ∧¬ψ→¬(φ∨ψ)の証明

【例】⇒¬(φ∧ψ)→¬φ∨¬ψの証明

【例】⇒¬φ∨¬ψ→¬(φ∧ψ) の証明

【演習問題】次のシークェント（ウカシェビッチの公理あるいはその逆を シークェントに読み替えたもの）をLKあるいはLJで証明せよ．

1. ⇒φ→(ψ→φ)
2. ⇒(φ→(ψ→χ)→((φ→ψ)→(φ→χ))
3. ⇒((φ→ψ)→(φ→χ))→(φ→(ψ→χ)
4. ⇒(¬ψ→¬φ)→(φ→ψ)
5. ⇒(φ→ψ)→(¬ψ→¬φ)

【演習問題】 古典命題論理の意味論で見たさまざまな恒真式（可換律，結合律， 分配律， 吸収律，→の別表現，ド・モルガンの法則，対偶の法則）や意味論的演繹関係 （modus tollens，選言三段論法，仮言三段論法）をシークェントの言葉に翻訳し， LKあるいはLJにおける証明を与えよ．

2.4 述語論理の形式化

推論規則

推論規則は，命題論理の場合と同じ形の規則に加えて， 量化子に関する以下の推論規則を用意する．この中で， t, a はそれぞれ項および自由変数，φ[t/x] および φ[a/x] は φに含まれる自由変数 x を t, a に置き換えたものを表わす． 自由変数 a は後で示す「固有変数条件」を満たさなければならない．

φ[t/x], Γ⇒Δ （t: 項） ∀x φ, Γ⇒Δ （∀左）		Γ⇒Δ, φ[a/x] （a: 自由変数） Γ⇒Δ, ∀x φ （∀右）
φ[a/x], Γ⇒Δ （a: 自由変数） ∃x φ, Γ⇒Δ （∃左）		Γ⇒Δ, φ[t/x] （t: 項） Γ⇒Δ, ∃x φ （∃右）

固有変数条件

自由変数 a は横線の下側のシークェントに自由変数として現れない．

∧と∨の推論規則と同様，ここでも∀と∃がまったく対称な形で 扱われている．これもシークェント計算の特徴である． 自然演繹と比較してみれば，上の４つの推論規則のうち， ∀右と∃右はそれぞれ自然演繹の∀導入と∃導入に対応する ものであることがわかる．∃左は∃除去に相当する． ∀左については対応関係がそれほど明らかではないが， 使われ方を想像すれば事実上∀除去に変わる役割を演じる ことが想像できる．

これらの推論規則を用いた証明の簡単な例を以下に示す．

【例】∀x(φ∧ψ) ⇒ ∀xφ∧∀xψの証明

上から２段目の∧左を適用する際には t = x とみなしている． また，３段目の∧右では a = x とみなしている． ４段目では x が∀で束縛されて自由変数として残っていないから， ∧右の適用に際して固有変数条件は確かに満たされている．

【例】∀xφ∧∀xψ⇒∀x(φ∧ψ）の証明

3. 命題論理の形式化の完全性

なお，以下に示す証明は小野寛晰「情報科学における論理」 （日本評論社，1994）の第１章7節に基づく．

3.1 シークェントの分解規則

(1a) Γ⇒Δ₁,φ∧ψ,Δ₂ を Γ⇒Δ₁,φ,Δ₂ と Γ⇒Δ₁,ψ,Δ₂ に分解する．

(1b) Γ₁,φ∧ψ,Γ₂⇒Δ を Γ₁,φ,ψ,Γ₂⇒Δに分解する．

(2a) Γ⇒Δ₁,φ∨ψ,Δ₂ を Γ⇒Δ₁,φ,ψ,Δ₂ に分解する．

(2b) Γ₁,φ∨ψ,Γ₂⇒Δ を Γ₁,φ,Γ₂⇒Δ と Γ₁,ψ,Γ₂⇒Δ に分解する．

(3a) Γ⇒Δ₁,φ→ψ,Δ₂ を φ,Γ⇒Δ₁,Δ₂ に分解する．

(3b) Γ₁,φ→ψ,Γ₂⇒Δ を Γ₁,Γ₂⇒Δ,φ と Γ₁,ψ,Γ₂⇒Δ に分解する．

(4a) Γ⇒Δ₁,¬φ,Δ₂ を φ,Γ⇒Δ₁,Δ₂ に分解する．

(4b) Γ₁,¬φ,Γ₂⇒Δ を Γ₁,Γ₂⇒Δ,φ に分解する． あとで示す補助定理１の証明からわかるように，八つの分解規則は いずれも本質的には推論規則を逆に読んだものである．

シークェントの証明の考え方のところで触れたように，与えられた シークェントから出発して分解規則を次々に適用して行けば （一般にはこれは一通りではないが），出発点のシークェントを根として， 分解によって得られたシークェントを節に配置した木ができる． これを「分解木」という．シークェントに対して分解規則を 適用すると，得られるシークェント（一つの場合と二つの場合がある） の中の論理結合子は必ず一つ減る．したがって，分解木の葉の シークェントが論理結合子を含まないものばかりになれば， それ以上は枝を伸ばせない．このような分解木を「完全分解木」 と呼ぶ．

【例】⇒¬(p∨q)→¬p∧¬q（p, q は命題記号） の完全分解木（矢印は分解の方向をあらわす）

p⇒p,q ↑ （2a） p⇒p∨q ↑ （4b） p,¬(p∨q)⇒ ↑ （4a） ¬(p∨q)⇒¬p q⇒p,q ↑ （2a） q⇒p∨q ↑ （4b） q,¬(p∨q)⇒ ↑ （4a） ¬(p∨q)⇒¬q

（1a） ¬(p∨q)⇒¬p∧¬q ↑ （3a） ⇒ ¬(p∨q)→¬p∧¬q

3.2 シークェントの分解に関する補助定理

次の補助定理によって，シークェントの証明可能性は分解によって得られる シークェントの証明可能性に帰着する．特に，完全分解木の葉のシークェントが 証明可能ならば，根のシークェントも証明可能であることがわかる．

【補助定理１】シークェント S に分解規則を適用して得られるものを S₁（１個のシークェントに分解されるとき）あるいは S₁, S₂（２個のシークェントに分解されるとき） とする．このとき，LKにおいて S₁, S₂から S が 導出できる．特に，S₁, S₂ がLKで証明可能ならば S も LKで証明可能である．

【注意】以下の証明を見ればわかるように，いずれについても S は カットを用いずに導出できる．

【証明】八つの分解規則のそれぞれについて確かめる．(1a)の場合は

Γ⇒Δ1,φ,Γ2 ： （交換右反復） Γ⇒Δ1,Γ2,φ Γ⇒Δ1,ψ,Γ2 ： （交換右反復） Γ⇒Δ1,Γ2,ψ
	（∧右）
Γ⇒Δ1,Δ2,φ∧ψ ： （交換右反復） Γ⇒Δ1,φ∧ψ,Δ2

という証明図からわかる．∧右以外は交換規則によって論理式を 移動しているだけであることに注意．(2b)の場合も∨左と交換規則の 組み合わせで同様に確かめられる．(1b)の場合は

Γ1,φ,ψ,Γ2⇒Δ
：	（交換左反復）
φ,ψ,Γ1,Γ2⇒Δ
	（∧左）
φ∧ψ,ψ,Γ1,Γ2⇒Δ
	（交換左）
ψ,φ∧ψ,Γ1,Γ2⇒Δ
	（∧左）
φ∧ψ,φ∧ψ,Γ1,Γ2⇒Δ
	（縮約左）
φ∧ψ,Γ1,Γ2⇒Δ
：	（交換左反復）
Γ1,φ∧ψ,Γ2⇒Δ

という証明図からわかる（交換規則による移動を別にすれば，これは要するに， シークェントの左辺のコンマを∧に置き換える手順を示している）． (2a)の場合も∨右と交換・縮約右の組み合わせで同様に確かめられる． (3a)の場合は→右と交換右，(4a)の場合は¬右と交換右， (4b)の場合は¬左と交換左の組み合わせで同様に確かめられる． 最後に(3b)の場合は

Γ1,Γ2⇒φ,Δ      Γ1,ψ,Γ2⇒Δ ： （交換右反復） ψ,Γ1,Γ2⇒Δ
	（→左）
φ→ψ,Δ1,Δ2⇒Δ ： （交換右反復） Δ1,φ→ψ,Δ2⇒Δ

という証明図からわかる．（証明終わり）

証明可能性はこのように分解木の葉から根の方向に伝わるが， 次の補助定理は逆に恒真性が根から葉の方向に伝わることを 示している．

【補助定理２】シークェント S に分解規則を適用して得られるものを S₁（１個のシークェントに分解されるとき）あるいは S₁, S₂（２個のシークェントに分解されるとき） とする．このとき，任意の真理値割り当て M に対して M[S] = T から M[S₁] = T, M[S₂] = T が従う．

【証明】八つの分解規則のそれぞれについて確かめる．

(1a)の場合： このとき

M[Γ⇒Δ1,φ∧ψ,Δ2]	=	M[Γ*→Δ1*∨(φ∧ψ) ∨Δ2*]
	=	M[¬Γ*∨Δ1*∨(φ∧ψ) ∨Δ2*]
	=	M[¬Γ*∨Δ1*∨φ ∨Δ2*] ∧M[¬Γ*∨Δ1*∨ψ ∨Δ2*]
	=	M[Γ*→Δ1*∨φ ∨Δ2*] ∧M[Γ*→Δ1*∨ψ ∨Δ2*]
	=	M[Γ⇒Δ1,φ,Δ2] ∧M[Γ⇒Δ1,ψ,Δ2]

という等式が成り立つので， M[Γ⇒Δ₁,φ∧ψ,Δ₂] = T から M[Γ⇒Δ₁,φ,Δ₂] = T および M[Γ⇒Δ₁,ψ,Δ₂] = T が従う．

(1b)の場合：

M[Γ₁,φ∧ψ,Γ₂⇒Δ] = M[Γ₁,φ,ψ,Γ₂⇒Δ]

という等式からわかる．

(2a), (2b) の場合：(1a), (1b) と同様である

(3a) の場合：

M[Γ⇒Δ1,φ→ψ,Δ2]	=	M[Γ*→Δ1*∨(φ→ψ) ∨Δ2*]
	=	M[¬Γ*∨Δ1*∨¬φ∨ψ ∨Δ2*]
	=	M[(¬Γ*∨¬φ)∨Δ1*∨ψ ∨Δ2*]
	=	M[Γ*∧φ→Δ1*∨ψ ∨Δ2*]
	=	M[Γ,φ⇒Δ1,ψ,Δ2]

という等式からわかる．

(3b)の場合：

M[Γ1,φ→ψ,Γ2⇒Δ]	=	M[Γ1*∧(φ→ψ)∧Γ2* →Δ*]
	=	M[¬Γ1*∨(φ∧¬ψ)∨¬Γ2* ∨Δ*]
	=	M[¬Γ1*∨φ∨¬Γ2*∨Δ*] ∧M[¬Γ1*∨¬ψ∨¬Γ2*∨Δ*]
	=	M[Γ1*∧Γ2*→φ∨Δ*] ∧M[Γ1*∧ψ∧Γ2*→Δ*]
	=	M[Γ1,Γ2⇒φ,Δ] ∧M[Γ1,ψ,Γ2⇒Δ]

という等式が成立するので， M[Γ₁,φ→ψ,Γ₂⇒Δ] = T から M[Γ₁,Γ₂⇒φ,Δ] = T および M[Γ₁,ψ,Γ₂⇒Δ] = T が従う．

(4a), (4b) の場合：(3a) と同様．（証明終わり）

3.3 完全性定理

LKの完全性の証明に入る．与えられたシークェント S が恒真であると 仮定して，LKにおいて証明可能であることを示せばよい．

S の完全分解木をつくると，葉に現れるのはいずれも論理結合子を含まない p₁,…,p_m⇒q₁,…,q_n （p₁, …, p_m, q₁, …, q_n は命題変数）という形のシークェントである．S が恒真であることから 補助定理２によってこれらのシークェントも恒真であることになる． この形のシークェントに恒真性と証明可能性については次のことがわかる．

【補助定理３】 1. p₁,…,p_m⇒q₁,…,q_n （p₁, …, p_m, q₁, …, q_n は命題変数）という形のシークェントが恒真であるための必要十分条件は 左辺の命題変数と右辺の命題変数の中に同じものがあること （すなわちある i,j に対して p_i = q_j）である．

2. p₁,…,p_m⇒q₁,…,q_n （p₁, …, p_m, q₁, …, q_n は命題変数）という形のシークェントにおいて， 左辺の命題変数と右辺の命題変数の中に同じものがあれば， このシークェントはLKで証明可能である．

【証明】1. 十分性： ある i,j に対して p_i = q_j とする． このとき ¬p_i∨q_j ≡ T であるから

p₁,…,p_m⇒q₁,…,q_n ≡ ¬p_i∨q_j∨… ≡ T

したがってシークェント p₁,…,p_m⇒q₁,…,q_n は 恒真である．

必要性：すべての i,j に対して p_i と q_j が異なる とする．このとき

M[p₁] = … = M[p_m] = T,    M[q₁] = … = M[q_n] = F

という真理値割り当て M が存在する．この真理値割り当てに対して

M[p₁,…,p_m⇒q₁,…,q_n] = F

となるから，シークェント p₁,…,p_m⇒q₁,…,q_n は 恒真でない．

2. p_i = q_j = p とすると，p⇒p という 初期シークェントから希釈と交換を繰り返すことによって 求めるシークェントが得られる．（証明終わり）

この補題から，恒真なシークェント S の完全分解木の葉に現れる シークェントは …,p,…⇒…,p,…（p は命題変数）という形をしていて， LKで証明可能である，ということがわかる．他方，補助定理１によって 証明可能性は葉から根の方向へ伝わるから，S もLKで証明可能である． こうして次の「完全性定理」が証明された．

【定理】LKは完全性をもつ．すなわち，任意のシークェントは 恒真ならば証明可能である．

3.4 カット除去定理

証明の最後の段階で補助定理１を用いたが， その証明でカットが用いられていないことからわかるように， 補助定理１の主張は「証明可能」を 「カットを使わずに証明可能」に置き換えても成立する． このことに注意すれば，完全性定理の主張も 「恒真ならばカットを使わずに証明可能である」 という形に強めることができる．一方，LKの健全性によって LKで証明可能なシークェントは恒真であるから， この強められた完全性の主張と合わせると，次のような 「カット除去定理」が成立することがわかる．

【定理】LKで証明可能なシークェントはカットを使わずに証明可能である．

これはシークェント計算におけるもっとも基本的な定理の一つである． シークェント計算の推論規則の中でカットは例外的な性格をもつ． カット以外の推論規則はシークェント中の論理式を全体としては そのまま保持しているが，カットだけは論理式の一部を消してしまう （文字通り「カット」する）．したがって，同じシークェントに対して カットを使わない証明と使う証明があれば，カットを使う証明の方は （あとで消える余分な論理式を含んでいるという意味で）無駄がある ことになる．カット除去定理はこの無駄を省いた証明が存在することを 主張している．

なお，無駄がないということは見た目に証明が短いということではない． カットは仮言三段論法（A→B かつ B→C から A→C が従う）の拡張と みなせるから，直観的にはわかりやすい規則である．カットを多用すれば 与えられたシークェントに対して証明を書き下す作業が楽になるかも 知れないし，証明自体が短くなることも起こり得る．しかしながら， 一般的に言って，カットのように記号列の一部を消してしまう操作は 構造帰納法を適用する際の障害になる．そのような意味で， カットのない証明の存在は基本的なことなのである．

なお，ここではカット除去定理に対して恒真性を介した 間接的な証明を与えたが，証明図を変形して行くことによって 直接的に証明することもできる（ゲンツェンによる証明）． それを用いればLJの場合にも同じ定理が成立することがわかる．

3.4 決定可能性

完全性定理の証明の中で，恒真なシークェントから完全分解木をつくれば， 葉に現れるシークェントはすべて恒真である，ということを見た． それでは恒真でないシークェントの場合はどうなるだろうか．

恒真でないシークェントの場合，その完全分解木の葉のシークェントが すべて恒真になることはあり得ない．仮にそれらがすべて恒真であると すると，補助定理３によってLKの中で証明可能でもあるから， 補助定理１によって根のシークェントの証明可能性が従う． 健全性によって，証明可能ならば恒真だから，もとのシークェントが 恒真ということになるが，これは矛盾している．

まとめると

• 恒真なシークェントから完全分解木をつくれば， 葉に現れるシークェントはすべて恒真である
• 恒真でないシークェントから完全分解木をつくれば， 葉に現れるシークェントの中には恒真でないものがある

ということがわかった．LKの健全性と完全性により， 恒真性と証明可能性は同値であるから，これは

• 証明可能なシークェントから完全分解木をつくれば， 葉に現れるシークェントはすべて証明可能である
• 証明可能でないシークェントから完全分解木をつくれば， 葉に現れるシークェントの中には証明可能でないものがある

というようにも言い換えられる．

ところで，補助定理３が示すように，完全分解木の葉に現れる シークェントの恒真性・証明可能性はシークェントの形から ただちに判定できる．したがって与えられたシークェントが LKで証明可能か否かは

1. シークェントの完全分解木をつくる
2. 葉に現れたシークェントが補助定理３の条件を 満たすかどうかを調べる

という手続きで決定できることになる． 完全分解木をつくることはシークェントに対して八つの 分解規則のどれかが適用できるかどうかを次々試すこと （一種の「パターンマッチング」）であるから， 有限の手続きである（正確な議論はここでは省く）． 葉に現れたシークェントが補助定理３の条件を満たすかどうかを 確かめることも明らかに有限の手続きである．このようにして 次の定理（命題論理に関するLKの「決定可能性」） が成立することがわかる．

【定理】与えられた命題論理のシークェントがLKで証明可能か否かを 決定する有限の手続きが存在する．

【注意】述語論理に関してはこれに対応することは成立しない （述語論理の「決定不可能性」）．これは 「チャーチの定理」として知られている結果で， ヒルベルトの「決定問題」に対する否定的解決を与えた． また，チューリングがチャーチとは独立に「機械」の概念を用いて 見出したことも同じ内容である（第１章参照）．チューリングの機械 （あるいはそれと同等な任意の計算モデル）の言葉で言えば， 論理の決定可能性とは

1. 入力：論理式やシークェント（適当な形でコード化しておく）
2. 出力：証明可能であるか否かに応じて，それを区別する 特定のコード（たとえば１と０）を返して停止する

という機械が存在する，ということを意味する．述語論理の場合には このような機械が存在し得ない，というのがチューリングの示した 結果である．ただし，機械では何も決定できない，というわけではなくて

1. 証明可能な場合には特定のコード（たとえば証明をコード化したもの） を返して停止する
2. 証明不可能な場合には停止しない

という機械は存在する（この性質を「半決定可能性」という）．

---

キーワード

シークェント，シークェントの左辺・右辺，シークェントの意味解釈， LK，LJ，初期シークェント，構造に関する推論規則， 論理結合子に関する推論規則，妥当性，健全性， ゴールから逆に考える，分解規則，分解木，完全分解木， 完全性定理，カット除去定理，決定可能性，決定問題， チャーチの定理，半決定可能性

---