LJpm の完全性

ここでは，LJpmの完全性の証明について見ていきたいと思う．まず，シークエント が反証される条件を定める．

定義 30. もし，V(∧

Γ, w) = 1 かつV(∨

∆, w) = 0 なら，Γ ⇒ ∆はクリプキモデル

第2章 シークエント計算とその発展 49

⟨W, R, V⟩^の，w ∈W で反証される．このとき，V(Γ⇒∆, w) = 0と書く．

さて，以下でモデルを構成するために必要となる概念の定義を与える．

定義 31 (完備シークエント). Γ の全部分論理式からなる集合をSub(Γ)と書く．ある シークエントΓ⇒∆が完備(complete)であるのは，

(1) (導出不可能性)そのシークエントが導出不可能．LJpm̸⊢Γ⇒∆ かつ

(2) (部分論理式Aに関わる条件) A∈Sub(Γ,∆)であるどんな論理式に対しても：

(2-1) (Aの明示的出現) A∈Γ∪∆ か

(2-2) (Aのclash性) LJpm⊢Γ⇒∆, AかつLJpm⊢A,Γ ⇒∆ のどちらかである．

以下，完備であるシークエントのことを「完備シークエント（complete sequent）」と呼ぶ

*12．

つまり，Γ ⇒ ∆が導出不可能で，しかもA ∈ Sub(Γ,∆)であるどの部分論理式 Aも

(2-1) または(2-2)の条件を満たしているものが，完備シークエントとなる．実際には，

Γ ⇒ ∆が完備シークエントであるとき，その部分論理式A^{はすべて，}(2-1)^{の条件を満} たすのであり，(2-2)の条件を満たすことはない．より詳しく言えば，(2-2)のclash性条 件を満たす部分論理式 A^{があるときは}Γ ⇒ ∆ ^{が導出可能になり，}(1)^{と矛盾してしま} う．そのため，(2-2)の条件を満たすことはないと言えるのである．このことを示すには LJpmには本来含まれないカット規則を使う必要がある．しかし，当面の論証ではカッ ト規則抜きの体系LJpmを対象としているので，直ちに，(2-2)の場合が空であると，結 論することはできない．このように述べると，最初から(2-2) の条件を取り除いて完備 シークエントの条件を与えればよいように思われるかもしれないが，それでは補題 8の証 明が行えなくなってしまう．そのため，(2-2)のclash性の可能性をひとまず認めておか なければならないのである．

定義 32. あるシークエントΓ ⇒ ∆が反転可能規則に対して，飽和（saturated）してい るのは：

*12定義31は本論でまとめ直したものである．

第2章 シークエント計算とその発展 50 (i) (導出不可能性) LJpm̸⊢Γ⇒∆ かつ，

(ii) (飽和条件) Γ ⇒∆に出現しているすべての論理式A, Bに対して，次のいずれ かが満たされている：

(&⇒) A&B∈Γ ならば，A∈ΓかつB ∈Γ． (⇒&) A&B∈∆ ^ならば，A ∈∆^またはB ∈∆^．

(∨ ⇒) A∨B∈Γ ならば，A∈ΓまたはB∈Γ． (⇒ ∨) A∨B∈∆ ならば，A ∈∆かつB∈∆．

(⊃⇒) A⊃B∈Γ ならば，A∈∆またはB∈Γ．

以下，反転可能規則に対して飽和したシークエントのことを「飽和シークエント（saturated sequent）」と呼ぶ ^*13．このとき，(ii)の五つの条件はすべて，Γ⇒∆に出現している各 論理式C について，それが複合式であるとき，つまり，CがA&BかA∨BかA⊃Bの とき，その部分論理式，つまりAとB（のうち少なくとも一つ）がそれ自身Γ⇒∆中に どのように出現していなければならないのかを定めている．ここでは，C ≡ A⊃B のと き，∆にCが出現する場合についての議論がなされていない．それは，(R⊃)がLJpm において反転可能でない規則であることによる．

反転可能規則は推論規則の結論の反証モデルが前提の反証モデルになり，推論規則の前 提の反証モデルが結論の反証モデルにもなるため，推論規則の前提の反証モデルが結論の 反証モデルにもなる．したがって，反証モデルを探したいシークエントが飽和シークエン トであり，後件に ⊃式を含まないときには，自分自身を参照することで，モデルを構成 できることになる．そのため，あるシークエントが飽和シークエントで，後件に含意式を 含まないときには，そのシークエントの証明図をそれ以上遡らなくても，原子式に注目す るだけで，反証モデルを構成できるということになる．このとき，前件中の原子式はすべ て成立，後件中の原子式はすべて不成立になるように値を振ると，前件中の複合式はすべ て成立，後件中の複合式はすべて不成立にすることができる．

さて，ここまで，完備シークエントと飽和シークエントの定義を与えた．続いて，以下 では，完備シークエントが飽和シークエントを含意することについて見る．

補題 7 (^飽和化, (Mints 2000, Lemma 8.3)). 与えられたシークエントΓ ⇒ ∆ ^が完備 シークエントであるとき，そのシークエントは飽和シークエントである．

*13飽和シークエントという呼び方は(Mints 2000)では用いられてはいない．

第2章 シークエント計算とその発展 51 この補題 7 が成り立つことにより，完備シークエントは必ず飽和シークエントであ るということは保証されたが，この逆は成り立たない．つまり，飽和シークエントが常 に完備シークエントであるとは限らないのである．例えば，⇒ P&Qについて考えてみ る．これは導出不可能なシークエントである．このシークエントの飽和シークエントは

⇒ P&Q, P^（⇒ P&Q, Qでも良い）このとき，完備シークエントは⇒P&Q, P, Q^であ るか，Q⇒P&Q, P（⇒P&Q, Qの時は，⇒P&Q, P, Qであるか，P ⇒P&Q, Q）で ある．飽和シークエントはもとのシークエントの部分論理式を全て含まなくても良いが，

完備シークエントはもとのシークエントの部分論理式をすべて含む必要があるので，完備 シークエントと飽和シークエントは一般的には異なる．しかし，飽和シークエントの条件 を満たすだけで，完備シークエントになるものも存在する．例えば，⇒P ∨Qについて 考える．これは導出不可能なシークエントである．このシークエントの飽和シークエント は⇒ P ∨Q, P, Qである．しかし，このシークエント中にはもとのシークエントの部分 論理式が全て出現しているので，完備シークエントでもある．また，導出不可能なシーク エントは完備シークエントへと必ず拡張できる．その拡張の仕方を以下の補題で見る．

補題 8 (完備化, (Mints 2000, Lemma 8.4)). 導出不可能などのシークエント Γ₀ ⇒ ∆₀ も，Γ0,∆0の部分論理式からなる完備シークエントへと拡張できる．このとき，導出不可 能なシークエントが定義 31を満たすことを示せばよい．

Proof. Γ0, ∆0の部分論理式をA0, . . . , Anのように列挙する．このとき，0≤i≤n^であ り，{A₀, . . . , A_n} ⊆Sub (Γ₀,∆₀)である．

今，Γi ⇒∆i の導出不可能性を保存しながら，AiがΓi ⇒∆iの前件，後件のどちらに 入るかについて考えればよい．A_i,Γ_i ⇒∆_iのときを考える．

(1) ̸⊢Ai,Γi ⇒∆i のとき

Γ_i+1 = Γ_i∪{A_i}^，∆_i+1 = ∆_iであり，Γ_i+1 ⇒∆_i+1は定義31の(2-1)を満たす．

(2) ⊢Ai,Γi ⇒∆i のとき

(i) ̸⊢ Γ_i ⇒ ∆_i, A_i であるか，(ii) ⊢ Γ_i ⇒ ∆_i, A_i である．(i)のときは，∆_i+1 =

∆i∪ {Ai}^，Γi+1 = Γiであり，Γi+1 ⇒∆i+1は定義 31の(2-1)を満たす．(ii)の ときは，⊢A_i,Γ_i ⇒∆_i，⊢Γ_i ⇒∆_i, A_i なので，Γ_i+1 ⇒∆_i+1 は定義31の(2-2) を満たす．このとき，Γi+1 = Γi，∆i+1 = ∆iとなる．

したがって，Γ₀ ⇒∆₀ は完備シークエントへと必ず拡張できる．

第2章 シークエント計算とその発展 52 この補題によって，導出不可能なシークエントが完備シークエントへと必ず拡張できる ことが保証された．つまり，部分論理式がシークエントの導出不可能性を維持して，シー クエント中に現れるようにすれば，導出不可能なシークエントから，完備シークエントを 作ることができるということである．さて，では以下で，反証モデルを構成する際に用い られるカノニカルモデルの定義を与えよう．

定義 33 (カノニカルモデル). 次のクリプキモデルK=⟨W_K, R_K, V_K⟩^{をカノニカルモデ} ルと呼ぶ．

• W_K：完備シークエントすべてからなる集合

• (Γ⇒∆)RK(Γ^′ ⇒∆^′) ⇔ Γ⊆Γ^′

• Γ⇒∆∈V_K(P) ⇔ P ∈Γ

⊆が反射的で推移的であることにより，RK は反射的で推移的であり，∈^は⊆^に関し て，単調であるので，V_Kは原子式に対して単調である．

定義 34. シークエントからなる集合M が反転可能でない規則に対して，飽和しているの は，M 中のどのΓ⇒∆に対しても，以下の条件が満たされているとき：

(⇒⊃) A⊃B ∈∆ なら，A,Γ⊆Γ^′ かつB∈∆^′ なるシークエントΓ^′ ⇒∆^′ がM 中に存 在する．

この定義によって，後件に含意式が出現する場合についても扱うことができるようにな る．ある集合 M ^が定義 34の条件を満たすようなシークエントとして含意式を中に含む シークエントの例を考えてみる．このとき，例えば，̸⊢(P⊃Q)⊃P ⇒P, P⊃Qを例にとる．

このシークエントは飽和シークエントであるが，ここで考えているM が反転可能でない 規則に対して飽和しているためには，このM の要素として，̸⊢(P⊃Q)⊃P, P ⇒Q, P⊃Q か̸⊢P,(P⊃Q)⊃P, P ⇒Qが含まれていなければならない．

また，完備シークエントすべてからなる集合W_Kは反転可能でない規則に対して飽和し ている．

命題 9. WK を完備シークエント全てからなる集合とする．そのとき，任意のΓ⇒ ∆ ∈ W_Kに対して，

(i) C ∈Γなら，K,Γ ⇒∆|=_K C

第2章 シークエント計算とその発展 53 (ii) C ∈∆なら，K,Γ⇒∆̸|=_K C

(iii) K,Γ⇒∆̸|=K Γ⇒∆．つまり，Γ⇒∆はΓ⇒∆∈WKで不成立．

では以下で，完全性の証明について見る． (Mints 2000)では，より一般的な飽和モデ ルに対して完全性の証明が与えられているが，本論で必要となる概念は，カノニカルモデ ルが扱う範囲に収めることができるので，カノニカルモデルを用いてその議論を考える．

命題 10 (完全性). LJpm中のどの導出不可能なシークエントもカノニカルモデルKで

反証される．したがって，どんな妥当なシークエントもLJpmで導出可能である．

Proof. 今，どんな導出不可能なシークエントΓ ⇒ ∆も，補題 8より，完備シークエン

トへと拡張できるので，完備シークエントΓ^′ ⇒∆^′ を持つ．カノニカルモデルKの集合 WKは全完備シークエントからなる集合なので，今拡張したシークエントもその中に含ま れる．命題 9よりK,Γ^′ ⇒ ∆^′ ̸|=_K Γ^′ ⇒∆^′ が成立する．ところで，今R_Kは定義 33よ り，Γ ⊆Γ^′なので，K,Γ^′ ⇒∆^′ ̸|=KΓ ⇒∆も成立．

このとき，LJpmの完全性の証明を与えることが可能であることからLJpm+ (Cut) なる体系に対するカット除去定理も意味論的に証明される（ただし，LJpm+ (Cut)の健 全性が示されている必要がある）^*14．ここでは，LJpmでの，形式体系からどのようにク リプキモデルを構成し，完全性の証明を与えるかを見てきたが，LJの完全性も，LJpm で見たのと同様に，形式体系からクリプキモデルを構成することによって示される．LJ の場合にも，構成されるクリプキモデルの到達可能性関係は，シークエントの前件の包含 関係によって定められる（cf. (^鹿島 2006)^）．