IX. シークェント計算

自然演繹と同様に,シークェント計算もゲンツェンが導入した 形式化である.自然演繹は推論規則の意味が理解しやすいという 長所をもつが,論理式に対する「形式的操作」という観点から見れば, すでに置いていた前提の一部をあとで「仮定」として落とすという 処理はあまり望ましいものではない.シークェント計算では, 単一の論理式の代わりに,論理式とそれが依存する前提を組にしたもの (シークェント)を形式的操作の対象にする.それによって自然演繹の 問題点が改善されるだけでなく,さまざまな点で形式的体系として 望ましい性質を備えたものになる.

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

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

目次

1. シークェントとは何か
2. シークェント計算による論理の形式化
3. 命題論理の形式化の完全性

総目次に戻る


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

シークェントは前提と帰結を組にしたもので,前提と帰結の それぞれが一般には複数の論理式からなる.

1.1 シークェントの定義

【定義】 論理式φ1, …, φm, ψ1, …, ψn をコンマで 区切って特別な区切り記号⇒の前後に並べたもの

φ1,…,φm ⇒ ψ1,…,ψn

シークェント(sequent)という. φ1,…,φm をシークェントの左辺, ψ1,…,ψn をシークェントの右辺と呼ぶ ことにする.なお,右辺が空のシークェント

φ1,…,φm

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

⇒ ψ1,…,ψn

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

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

φ1,…,φm |- ψ1,…,ψn

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

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

シークェントの正確な意味解釈は論理体系によって異なるが, おおざっぱに言えば
  1. φ1,…,φm ⇒ ψ1, …, ψn
  2. ⇒ ψ1,…,ψn (左辺が空)
  3. φ1,…,φm ⇒ (右辺が空)
はそれぞれ
  1. φ1, …, φm のすべてが真ならば ψ1, …, ψn のいずれかが真である
  2. ψ1, …, ψn のいずれかが真である
  3. φ1, …, φm のいずれかが偽である
ということを意味する.特に, 左辺のコンマは∧,右辺のコンマは∨と解釈される (シークェントのコンマはただの「区切り」記号ではなくて, それ自体が重要な意味をもつ一種の「つなぎ」記号である). また,左辺が空の場合は前提なしに右辺が従うこと, 右辺が空の場合は前提が矛盾していることを意味する. たとえば古典論理の意味解釈では,これらのシークェントは
  1. φ1∧…∧φm → ψ1∨…∨ψn
  2. T → ψ1∨…∨ψn
  3. φ1∧…∧φm → ⊥
(T,⊥は真,偽をあらわす命題定数),いいかえれば
  1. φ1∧…∧φm → ψ1∨…∨ψn
  2. ψ1∨…∨ψn
  3. ¬(φ1∧…∧φm)
と論理的に同値なものと考える.

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

φ1∧…∧φm →ψ1∨…∨ψn ≡ ¬φ1∨…∨¬φm∨ψ1∨…∨ψn

というように同値変形できて,論理式を∨で結んだものになる. この形の論理式(命題論理の意味論の中で触れた「節形式」は その特別な場合である)の面白いところは

φ1∧…∧φm →ψ1∨…∨ψn ≡ φ1∧…∧φm-1¬φm∨ψ1∨…∨ψn

あるいは

φ1∧…∧φm →ψ1∨…∨ψn ≡ φ1∧…∧φm¬ψ1 →ψ2∨…∨ψn

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

x1 + … + xm = y1 + … + yn

を「移項」によって

x1 + … + xm-1 = - xm + y1 + … + yn

あるいは

x1 + … + xm - y1 = y2 + … + yn,

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

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

古典論理におけるシークェントの意味解釈をもう少し正確に述べる.

Γ,Δで論理式の並び

Γ = "φ1,…,φm",    Δ = "ψ1,…,ψn"

をあらわして,Γ⇒Δ というシークェントを考える.ちなみに,

Γ = φ1,…,φm,    Δ = ψ1,…,ψn

と書くと,Γはφ1, …, φmのいずれかである, 等々という意味に誤解されるおそれがあるので,計算機プログラムの 文字列表記法にならって,論理式のコンマ区切りの並びを引用符 " " で囲むことによって明示してみた.

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

Γ* = φ1∧…∧φm,    Δ* = ψ1∨…∨ψn

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

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

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

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

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

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

と定義する.


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

自然演繹による論理の形式化にNKとNJがあるように, シークェント計算による論理の形式化には「LK」と「LJ」 がある.それぞれ古典論理と直観主義論理の形式化である.

2.1 命題論理の形式化

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

φ⇒φ    (φは任意の論理式)

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

LKとLJの違い

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

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

【構造に関する規則】

Γ⇒Δ

φ,Γ⇒Δ
(希釈左)
    
Γ⇒Δ

Γ⇒Δ,φ
(希釈右)
φ,φ,Γ⇒Δ

φ,Γ⇒Δ
(縮約左)
    
Γ⇒Δ,φ,φ

Γ⇒Δ,φ
(縮約右)
Γ,φ,ψ,Π⇒Δ

Γ,ψ,φ,Π⇒Δ
(交換左)
    
Γ⇒Δ,φ,ψ,Σ

Γ⇒Δ,ψ,φ,Σ
(交換右)
Γ⇒Δ,φ      φ,Π⇒Σ

Γ,Π⇒Δ,Σ
(カット)

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

φ,Γ⇒Δ ψ,Γ⇒Δ

  
(∧左)
φ∧ψ,Γ⇒Δ φ∧ψ,Γ⇒Δ
Γ⇒Δ,φ    Γ⇒Δ,ψ

(∧右)
Γ⇒Δ,φ∧ψ
φ,Γ⇒Δ    ψ,Γ⇒Δ

(∨左)
φ∨ψ,Γ⇒Δ
Γ⇒Δ,φ Γ⇒Δ,ψ

  
(∨右)
Γ⇒Δ,φ∨ψ Γ⇒Δ,φ∨ψ
Γ⇒Δ,φ    ψ,Π⇒Σ

(→左)
φ→ψ,Γ,Π ⇒ Δ,Σ
φ,Γ⇒Δ,ψ

(→右)
Γ ⇒ Δ,φ→ψ
Γ⇒Δ,φ

(¬左)
¬φ,Γ⇒Δ
φ,Γ⇒Δ

(¬右)
Γ⇒Δ,¬φ

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

【例1】⇒Φ→¬¬φ(二重否定の生成:LJで証明できる)

1: φ⇒φ (初期シークェント)
2: ¬φ,φ⇒(1¬左)
3: φ⇒¬¬φ (2¬右)
4: ⇒Φ→¬¬Φ(3→右)
これは自然演繹では |- Φ¬¬φ に相当する.シークェント計算では φを左右に移動するだけで二重否定の生成が証明できてしまう. 自然演繹で二重否定の除去を証明するには,これとは対照的に, ¬φを仮定して⊥を導く,というやや回りくどいことを行った. シークェント計算は非常に機械的なものであることがこの例からうかがえる.

【例2】⇒¬¬φ→φ(二重否定の除去:LKでないと証明できない)

1: φ⇒φ (初期シークェント)
2:⇒φ,¬φ (1¬右)
3: ¬¬φ⇒φ (2¬右)
4: ⇒¬¬Φ→Φ(3→右)
これは自然演繹の |- ¬¬φ→φ に相当する.ここでもφを左右に 移動するだけで証明ができてしまう.ただし,2行目でシークェントの 右辺に論理式が複数現れるので,この証明はLJの枠からはみ出している. LJの枠内では¬¬φ⇒φが導出できそうにないこともすぐにわかる. 実際,論理結合子に関するシークェント計算の推論規則はいずれも 論理結合子の数を変えないか増やすものばかりで,減らすものはない (これは自然演繹との大きな違いである)ので,¬¬φをつくり出すには どこかで¬の規則をちょうど2回適用するしかないが,それには実質的に 上のやり方しかない.構造に関する規則を適用すればこれ以外にいろいろと 回り道はできるが,改善にはつながらない.

【例3】⇒φ∨¬φ(排中律:LKでないと証明できない)

1: φ⇒φ (初期シークェント)
2:⇒φ,¬φ (1¬右)
3:⇒φ,φ∨¬φ (2∨右)
4:⇒φ∨¬φ,φ (3交換右)
5:⇒φ∨¬φ,φ∨¬φ (4∨右)
6:⇒φ∨¬φ (5縮約右)
これは自然演繹では |- φ∨¬φ に相当する. 2行目から5行目までは要するにコンマを∨に書き換えているだけ であるが,推論規則通りに行うとこれだけの手間がかかる.なお, 2行目以下ではシークェントの右辺に複数の論理式が現れるので, これもLJの枠からはみ出している.

【例4】⇒φ∧(φ→ψ)→ψ(modus ponens:LJで証明できる)

1: φ⇒φ (初期シークェント)
2: ψ⇒ψ (初期シークェント)
3: φ,φ→ψ⇒ψ (1,2→左)
4: Φ∧(Φ→ψ),Φ⇒ψ(3∧左)
5: Φ,Φ∧(Φ→ψ)⇒ψ(4交換左)
6: Φ∧(Φ→ψ),Φ∧(Φ→ψ)⇒ψ(5∧左)
7: Φ∧(Φ→ψ)⇒ψ(6希釈左)
8: ⇒Φ∧(Φ→ψ)→ψ(7→右)
含意記号→とシークェントの区切り記号⇒が紛らわしいが, 自然演繹ではこれは |- φ∧(φ→ψ) |- ψ に相当する. 4行目から7行目は Φ,χ⇒ψ から Φ∧χ⇒ψ を導く推論で, 構造規則の使い方の典型的な例を示している.

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

すでに述べた古典命題論理の意味解釈に基づいて,LKの推論規則の妥当性を 確かめよう.直観主義命題論理の意味解釈に基づくLJの推論規則の妥当性の 確認は大掛かりなものになるので,ここでは立ち入らない (冒頭に掲げた参考書に譲る).

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

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

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

Γ⇒Δ

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

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

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

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

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

M[φ,Γ⇒Δ] = M[φ∧Γ*→Δ*],
M[φ∧ψ,Γ⇒Δ] = M[φ∧ψ∧*→Δ*] = M[ψ]∧M[φ,Γ⇒Δ]

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

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

M[Γ⇒Δ,φ] = M[Γ*→Δ*∨φ],    M[Γ⇒Δ,ψ] = M[Γ*→Δ*∨ψ]

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

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

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

A→ B∨(P∧Q) ¬A∨B∨(P∧Q)
(¬A∨B∨P)∧(¬A∨B∨Q)
(A→B∨P)∧(A→B∨Q)

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

M[Γ⇒Δ,φ∧ψ] =M[Γ*→Δ*∨φ]∧ M[Γ*→Γ*∨ψ]
= M[Γ⇒Δ,φ]∧M[Γ⇒Δ,ψ]

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

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

M[Γ⇒Δ,φ] = M[Γ*→Δ*∨φ],    M[ψ, Π⇒Σ] = M[ψ∧Π*→Σ*]

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

M[φ→ψ, Γ, Π⇒Δ, Σ] = M[(φ→ψ)∧Γ*∧Π* →Δ*∨Σ*]

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

(P→Q)∧A∧C→B∨D ¬(¬P∨Q)∨¬A∨¬C∨B∨D
(P∨¬A∨¬C∨B∨D)∧(¬Q∨¬A∨¬C∨B∨D)
((A→B∨P)∨(C→D))∧((A→B)∨(Q∧C→D))

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

M[φ→ψ, Γ, Π⇒Δ, Σ] = (M[Γ*→Δ*∨φ] ∨ M[Π*→Σ*])
(M[Γ*→Δ*] ∨ M[ψ∧Π*→Σ*])
= (M[Γ⇒Δ,φ]∨M[Π⇒Σ])∧(M[Γ⇒Δ]∨M[ψ,Π⇒Σ])

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

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

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

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

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

M[Γ⇒Δ,φ] = M[Γ*→Δ*∨φ],
M[¬φ,Γ⇒Δ] = M[¬φ∧Γ*→Δ*∨φ] = M[Γ⇒Δ,φ]

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

2.3 証明の考え方

すでに非常に簡単な例をいくつか紹介したが,意味論や自然演繹で扱った 恒真式・定理・演繹をシークェントに読み替えれば,そのまま シークェント計算の例題になる.

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

  1. ⇒¬(φ∨ψ)→¬φ∧¬ψ
  2. ⇒¬φ∧¬ψ→¬(φ∨ψ)
  3. ⇒¬(φ∧ψ)→¬φ∨¬ψ
  4. ⇒¬φ∨¬ψ→¬(φ∧ψ)
自然演繹ではそれぞれ
  1. |- ¬(φ∨ψ)→¬φ∧¬ψ
  2. |- ¬φ∧¬ψ→¬(φ∨ψ)
  3. |- ¬(φ∧ψ)→¬φ∨¬ψ
  4. |- ¬φ∨¬ψ→¬(φ∧ψ)
に相当することに注意されたい.自然演繹では三番目以外は 排中律を使わずにNJで証明できたが,シークェント計算も同様で, 三番目以外はLJで証明できる.

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

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

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

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

φ⇒φ

(∨右)
φ⇒φ∨ψ

(¬左)
¬(φ∨ψ),φ⇒

(交換左)
φ,¬(φ∨ψ)⇒

(¬右)
¬(φ∨ψ)⇒¬φ
ψ⇒ψ

(∨右)
ψ⇒φ∨ψ

(¬左)
¬(φ∨ψ),ψ⇒

(交換左)
ψ,¬(φ∨ψ)⇒

(¬右)
¬(φ∨ψ)⇒¬ψ

(∧右)
¬(φ∨ψ)⇒¬φ∧¬ψ

(→右)
⇒ ¬(φ∨ψ)→¬φ∧¬ψ

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

φ⇒φ

(¬左)
¬φ,φ⇒

(∧左)
¬φ∧¬ψ,φ⇒

(交換左)
φ,¬φ∧¬ψ⇒
ψ⇒ψ

(¬左)
¬ψ,ψ⇒

(∧左)
¬φ∧¬ψ,ψ⇒

(交換左)
ψ,¬φ∧¬ψ⇒

(∨左)
φ∨ψ,¬φ∧¬ψ⇒

(¬右)
¬φ∧¬ψ⇒¬(φ∨ψ)

(→右)
⇒¬φ∧¬ψ→¬(φ∨ψ)

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

φ⇒φ

(¬右)
⇒φ,¬φ

(∨左)
⇒φ,¬φ∨¬ψ
ψ⇒ψ

(¬右)
⇒ψ,¬ψ

(∨右)
⇒ψ,¬φ∨¬ψ

(∧右)
⇒φ∧ψ,¬φ∨¬ψ

(交換右)
⇒¬φ∨¬ψ,φ∧ψ

(¬左)
¬(φ∧ψ)⇒¬φ∨¬ψ

(→右)
⇒¬(φ∧ψ)→¬φ∨¬ψ

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

φ⇒φ

(∧左)
φ∧ψ⇒φ

(¬左)
¬φ,φ∧ψ⇒
ψ⇒ψ

(∧左)
φ∧ψ⇒ψ

(¬左)
¬ψ,φ∧ψ⇒

(∨左)
¬φ∨¬ψ,φ∧ψ⇒

(交換左)
φ∧ψ,¬φ∨¬ψ⇒

(¬右)
¬φ∨¬ψ⇒¬(φ∧ψ)

(→右)
⇒¬φ∨¬ψ→¬(φ∧ψ)

【演習問題】次のシークェント(ウカシェビッチの公理あるいはその逆を シークェントに読み替えたもの)を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 は横線の下側のシークェントに自由変数として現れない.

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

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

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

φ⇒φ

(∧左)
φ∧ψ⇒φ

(∀左)
∀x(φ∨ψ)⇒φ

(∀右)
∀x(φ∨ψ)⇒∀xφ
ψ⇒ψ

(∧左)
φ∧ψ⇒ψ

(∀左)
∀x(φ∧ψ)⇒ψ

(∀右)
∀x(φ∧ψ)⇒∀xψ

(∧右)
∀x(φ∧ψ)⇒∀xφ∧∀xψ

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

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

φ⇒φ

(∀左)
∀xφ⇒φ

(∧左)
∀xφ∧∀xψ⇒φ
ψ⇒ψ

(∀左)
∀xψ⇒ψ

(∧左)
∀xφ∧∀xψ⇒ψ

(∧右)
∀xφ∧∀xψ⇒φ∧ψ

(∀右)
∀xφ∧∀xψ⇒∀x(φ∧ψ)


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

この節のおもな目標はLKによる命題論理の形式化の「完全性」 を証明することである.そのためにまずシークェントの分解規則を 導入する.この分解規則を与えられたシークェントに適用すること によって分解木が得られる.与えられたシークェントが恒真ならば, この分解木を少し修正することによって証明図が得られて, 完全性の証明ができる.さらに,分解木による証明からいくつかの 重要な副産物も得られる.

なお,以下に示す証明は小野寛晰「情報科学における論理」 (日本評論社,1994)の第1章7節に基づく.

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

分解規則」として次の八通りの規則を考える (一つのシークェントを一つのシークェントに書き換えるものは 「分解」よりも「還元」と言う方がふさわしいが,ここでは 「分解」で統一する).
(1a) Γ⇒Δ1,φ∧ψ,Δ2 を Γ⇒Δ1,φ,Δ2 と Γ⇒Δ1,ψ,Δ2 に分解する.
(1b) Γ1,φ∧ψ,Γ2⇒Δ を Γ1,φ,ψ,Γ2⇒Δに分解する.
(2a) Γ⇒Δ1,φ∨ψ,Δ2 を Γ⇒Δ1,φ,ψ,Δ2 に分解する.
(2b) Γ1,φ∨ψ,Γ2⇒Δ を Γ1,φ,Γ2⇒Δ と Γ1,ψ,Γ2⇒Δ に分解する.
(3a) Γ⇒Δ1,φ→ψ,Δ2 を φ,Γ⇒Δ12 に分解する.
(3b) Γ1,φ→ψ,Γ2⇒Δ を Γ12⇒Δ,φ と Γ1,ψ,Γ2⇒Δ に分解する.
(4a) Γ⇒Δ1,¬φ,Δ2 を φ,Γ⇒Δ12 に分解する.
(4b) Γ1,¬φ,Γ2⇒Δ を Γ12⇒Δ,φ に分解する. あとで示す補助定理1の証明からわかるように,八つの分解規則は いずれも本質的には推論規則を逆に読んだものである.

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

【例】⇒¬(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 シークェントの分解に関する補助定理

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

【補助定理1】シークェント S に分解規則を適用して得られるものを S1(1個のシークェントに分解されるとき)あるいは S1, S2(2個のシークェントに分解されるとき) とする.このとき,LKにおいて S1, S2から S が 導出できる.特に,S1, S2 がLKで証明可能ならば S も LKで証明可能である.

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

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

Γ⇒Δ1,φ,Γ2


(交換右反復)
Γ⇒Δ12
Γ⇒Δ1,ψ,Γ2


(交換右反復)
Γ⇒Δ12

(∧右)
Γ⇒Δ12,φ∧ψ


(交換右反復)
Γ⇒Δ1,φ∧ψ,Δ2

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

Γ1,φ,ψ,Γ2⇒Δ


(交換左反復)
φ,ψ,Γ12⇒Δ

(∧左)
φ∧ψ,ψ,Γ12⇒Δ

(交換左)
ψ,φ∧ψ,Γ12⇒Δ

(∧左)
φ∧ψ,φ∧ψ,Γ12⇒Δ

(縮約左)
φ∧ψ,Γ12⇒Δ


(交換左反復)
Γ1,φ∧ψ,Γ2⇒Δ

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

Γ12⇒φ,Δ     
Γ1,ψ,Γ2⇒Δ


(交換右反復)
ψ,Γ12⇒Δ

(→左)
φ→ψ,Δ12⇒Δ


(交換右反復)
Δ1,φ→ψ,Δ2⇒Δ

という証明図からわかる.(証明終わり)

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

【補助定理2】シークェント S に分解規則を適用して得られるものを S1(1個のシークェントに分解されるとき)あるいは S1, S2(2個のシークェントに分解されるとき) とする.このとき,任意の真理値割り当て M に対して M[S] = T から M[S1] = T, M[S2] = 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[Γ⇒Δ1,φ∧ψ,Δ2] = T から M[Γ⇒Δ1,φ,Δ2] = T および M[Γ⇒Δ1,ψ,Δ2] = T が従う.

(1b)の場合:

M[Γ1,φ∧ψ,Γ2⇒Δ] = M[Γ1,φ,ψ,Γ2⇒Δ]

という等式からわかる.

(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[Γ12⇒φ,Δ] ∧M[Γ1,ψ,Γ2⇒Δ]

という等式が成立するので, M[Γ1,φ→ψ,Γ2⇒Δ] = T から M[Γ12⇒φ,Δ] = T および M[Γ1,ψ,Γ2⇒Δ] = T が従う.

(4a), (4b) の場合:(3a) と同様.(証明終わり)

3.3 完全性定理

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

S の完全分解木をつくると,葉に現れるのはいずれも論理結合子を含まない p1,…,pm⇒q1,…,qn (p1, …, pm, q1, …, qn は命題変数)という形のシークェントである.S が恒真であることから 補助定理2によってこれらのシークェントも恒真であることになる. この形のシークェントに恒真性と証明可能性については次のことがわかる.

【補助定理3】 1. p1,…,pm⇒q1,…,qn (p1, …, pm, q1, …, qn は命題変数)という形のシークェントが恒真であるための必要十分条件は 左辺の命題変数と右辺の命題変数の中に同じものがあること (すなわちある i,j に対して pi = qj)である.

2. p1,…,pm⇒q1,…,qn (p1, …, pm, q1, …, qn は命題変数)という形のシークェントにおいて, 左辺の命題変数と右辺の命題変数の中に同じものがあれば, このシークェントはLKで証明可能である.

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

p1,…,pm⇒q1,…,qn ≡ ¬pi∨qj∨… ≡ T

したがってシークェント p1,…,pm⇒q1,…,qn は 恒真である.

必要性:すべての i,j に対して pi と qj が異なる とする.このとき

M[p1] = … = M[pm] = T,    M[q1] = … = M[qn] = F

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

M[p1,…,pm⇒q1,…,qn] = F

となるから,シークェント p1,…,pm⇒q1,…,qn は 恒真でない.

2. pi = qj = p とすると,p⇒p という 初期シークェントから希釈と交換を繰り返すことによって 求めるシークェントが得られる.(証明終わり)

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

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

3.4 カット除去定理

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

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

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

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

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

3.4 決定可能性

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

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

まとめると

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

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

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

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

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

  1. 入力:論理式やシークェント(適当な形でコード化しておく)
  2. 出力:証明可能であるか否かに応じて,それを区別する 特定のコード(たとえば1と0)を返して停止する
という機械が存在する,ということを意味する.述語論理の場合には このような機械が存在し得ない,というのがチューリングの示した 結果である.ただし,機械では何も決定できない,というわけではなくて
  1. 証明可能な場合には特定のコード(たとえば証明をコード化したもの) を返して停止する
  2. 証明不可能な場合には停止しない
という機械は存在する(この性質を「半決定可能性」という).


キーワード

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