第 3 章 証明反駁アルゴリズム (proof or refutation algorithm) 64
3.5 様相論理 S4
3.5.3 完全性
[9]の構成法は次のようになものである。(2)t規則の下式に2Aが存在し、(2)t規則の左上式にAが存在するので、
w1からw2に関係を付ける。同様に、w1からw3に関係を付ける。次に、左の(init)sに2¬Aが存在し、¬Aが右の シンメトリックイニシャルブロックに存在するので、w2からw3に関係を付ける。同様にして、w3からw2に関係が 付けられる。そして、最後に推移律と反射律の閉包を取る。
このように、[9]の手法では、クリプキフレームを構成するためにはシーケントを構成する論理式に立ち入って調べ る必要がある。このため、規則の種類のみからフレームを作る本手法よりも遥かに手間がかかる。
オーダーを考えてみれば、本手法ではブロックのサイズをnとすると、ブロックの先頭の推論規則が何であるかを 調べればよいため、そのオーダーはO(n)である。それに対して[9]の手法では、論理式がどこに出現しているかを探 す必要があるためO(n2)程度である。二分木を使えばさらに速くすることもできるが、それでもO(nlog(n))程度で ある。
例 3.5.7 (クラスター)
イニシャルクラスター クラスター
始点
図 3.14: クラスターの例
図3.14のように、S4の反駁木から構成されたS4モデルはクラスターの木構造を持ち、そのクラスターには必ず一 つの始点がある。
定義3.5.8 (ソートされた論理式列,ソートされたブロック) 論理式列→A=A1,· · ·, Anがソートされているとは、
∀i, j((i≥j⇒len(Ai)≥len(Aj))かつ(i=j⇒Ai =Aj))が成り立つことである。
ブロックが2→Aによってソートされているとは、ブロック中の全てのT 規則 Γ,B, B,Θ→∆2Π|2Σ
Γ,2B,Θ→∆2Π|2Σ (T)
に対して、∀C∈Γ,∃i(2C≡2Ai かつ∃j(2B≡Aj かつi≥j))が成り立つことである。
補題3.5.9 (規則の入れ換え) 上の規則の主論理式が下の規則の主論理式よりも長いときには、適用している推論規則
の順序を入れ替えることができる。
(証明) 下図のように上の規則が(→ ∧)1 で下の規則が(→⊃)の場合を考える。len(A∧B) ≤ len(C ∧D)かつ len(A)<len(A∧B)かつlen(B)<len(A∧B)であるから、len(A)<len(C∧D)かつlen(B)<len(C∧D)が成り立 つ。すなわち、A=C∧D かつB=C∧D が成り立つ。故に、この場合には下図のように規則を入れ替えることが できる。他の規則の場合も同様である。
Γ, A→B, C,∆
Γ, A→B, C∧D,∆ (→ ∧)1 Γ→A⊃B, C∧D,∆ (→⊃)
入れ換え=⇒
Γ, A→B, C,∆
Γ,→A⊃B, C,∆ (→⊃) Γ→A⊃B, C∧D,∆ (→ ∧)1
補題3.5.10 (ソートされたブロック) あるブロックがΓ, p1,· · ·, pn → q1,· · ·, qm,2∆ 2Π,2Σ で始まりΓ →
∆2Π,2Σで終わるとする。このとき、ソートされた論理式列2→A(⊃2Γ)に対してΓ, p1,· · ·, pn→q1,· · ·, qm,2∆ 2Π,2Σで始まりΓ →∆2Π,2Σで終わるソートされたブロックが存在する。
(証明)補題3.5.9より、主論理式の長さが下式よりも上式が短かくなるように並べ替えることができる。また、主 論理式の長さが同じであるときにも、規則を入れ替えることができるので、ソートされた2→A(⊃2Γ)に対してソート されているように並べ替えることができる。
定義3.5.11 (ポジティブ代入とネガティブ代入) →A≡A1,· · ·, An, B≡→ B1,· · ·, Bn, [→A:=B→]≡[A1:=B1,· · ·, An:=
Bn]とする。このとき、 ポジティブ代入C pos[→A:=→B]とネガティブ代入C neg[→A:=→B]を以下のように定義する。
あるiに対してC≡Aiのとき、
C pos[→A:=→B]≡Bi
それ以外のときは以下のようにCに対して帰納的に定義する。
1. C≡pのとき。
ppos[→A:=→B]≡p pneg[→A:=B→]≡p 2. C≡D∧Eのとき。
(D∧E) pos[→A:=B]→ ≡Dpos[→A:=→B]∧Epos[→A:=→B]
(D∧E) neg[→A:=→B]≡Dneg[→A:=→B]∧Eneg[→A:=→B] 3. C≡D∨Eのとき。
(D∧E) pos[→A:=B]→ ≡Dpos[→A:=→B]∨Epos[→A:=→B]
(D∧E) neg[→A:=→B]≡Dneg[→A:=→B]∨Eneg[→A:=→B] 4. C≡D⊃Eのとき。
(D⊃E) pos[→A:=→B]≡Dneg[→A:=→B]⊃Epos[→A:=→B] (D⊃E) neg[→A:=B→]≡Dpos[→A:=→B]⊃Eneg[→A:=→B] 5. C≡ ¬Dのとき。
(¬D) pos[→A:=→B]≡ ¬Dneg[→A:=→B] (¬D) neg[→A:=B]→ ≡ ¬Dpos[→A:=→B]
6. C≡2Dのとき。
(2D) pos[→A:=B→]≡2Dpos[→A:=B→] (2D) neg[→A:=→B]≡2Dneg[→A:=→B]
定義3.5.12 (シーケントに対するポジティブ代入とネガティブ代入) シーケントC1,· · ·, Cn →D1,· · ·, Dmに対し てポジティブ代入とネガティブ代入を以下のように拡張する。
(C1,· · ·Cn →D1,· · ·Dm)pos[→A:=→B]
≡C1neg[→A:=→B],· · ·, Cnneg[→A:=→B]→D1pos[→A:=B],→ · · ·, Dmpos[→A:=B]→ (C1,· · ·Cn →D1,· · ·Dm)neg[→A:=B→]
≡C1pos[→A:=→B],· · ·, Cnpos[→A:=B→]→D1neg[→A:=→B],· · ·, Dmneg[→A:=B→] 例 3.5.13 (ポジティブ代入とネガティブ代入)
(A∧B, C→C)neg[A∧B:=D, A:=E, C:=F]
≡(A∧B)pos[A∧B :=D, A:=E, C :=F], Cpos[A∧B :=D, A:=E, C:=F]→Cneg[A∧B :=D, A:=
E, C:=F]
≡D, F→C
補題3.5.14 (i)w|=Aのときw|=Apos[→B:=→⊥]。
(ii) w|=Aのときw|=Aneg[B→:=→⊥]。
(証明)A≡Bでw|=Aのとき。Apos[B:=→ →⊥]≡ ⊥。ゆえにw|=A。
A≡Bでw|=Aのとき。Aneg[→B:=→⊥]≡A。ゆえにw|=A。
A≡Bのとき、Aの構造に関する(i),(ii)の同時帰納法で証明する。
(i)でA≡2Cのとき。w|=2Cであるから、∃v(w→v)v|=C。帰納法の仮定より、v|=Cpos[B→:=→⊥]。よって、
w|=2(Cpos[→B:=→⊥])。故にw|= (2C) pos[→B:=→⊥]。
(ii)でA≡2Cのとき。w|=2Cであるから、∀v(w→v)v|=C。帰納法の仮定より、v|=Cneg[B→:=→⊥]。よって、
w|=2(Cneg[→B:=→⊥])。故に、w|= (2C) neg[B:=→ →⊥]。
その他の場合は明らか。
補題3.5.15 クリプキモデルのある可能世界が∧,∨,⊃,¬規則の上式を反駁するとき、その可能世界はまた下式も反 駁する。
(証明)自明。
定理3.5.16 本手法により構成されたクリプキモデルは反例となる。
(証明)クラスターの構成に関する帰納法。
一点からなるイニシャルクラスターのとき。この場合対応するブロックは推移的イニシャルブロックとなり、始式は Γ, p1,· · ·, pn →q1,· · ·, qmという形をしている。このシーケントは対応する可能世界{p1,· · ·, pn}で反駁される。
なぜなら、Γは解釈上無視され、このシーケントの右辺には2論理式が出現しないからである。前補題より、T 規 則以外では下式も順次反駁される。そして、クラスターはイニシャルクラスターとなるので、この可能世界からの他 の可能世界への到達可能関係はない。よって、T規則の下式も反駁される。
故に、このブロックの終式も反駁される。
二点以上からなるイニシャルクラスターのとき。
1. このクラスターに対応するブロックの妥当な履歴をΓとし、このΓをソートしたものを→Γで表す。
2. 対応する全てのブロックを→Γ でソートする。(補題3.5.10より) 3. 対応するブロックの非妥当な履歴の和集合をΣとする。
4. 対応するブロックに出現する全てのシーケントにpos[2→Σ:=→⊥] を代入したブロックを考える。すると、ブロッ クの始式は対応する可能世界で反駁される。なぜなら、代入前の始式はΓ,→p→→q ,2→Aという形をしていて、
(Γ,→p→→q ,2→A)pos [2→Σ:=→⊥] ≡Γpos [2→Σ:=→⊥],→p→→q ,→⊥となり、右辺の2論理式はすべて⊥で置き換えら れるからである。
5. ∧,∨,⊃,¬規則のときは、補題3.5.15より、下式も反駁される。
6. (T), (T)t規則のときは、
Γ,B, B,∆→Π Γ,2B,∆→Π (T)
という形をしている。このとき、各ブロックはソートされて いるので、全て対応する可能世界でBは妥当である。すなわち、そのクラスターでBが妥当であるので、2B も妥当である。故に、T規則の下式は反駁される。
7. 5. と6.を繰り返すと、pos [2→Σ:=→⊥] を代入した各終式が反駁されることが分かる。
8. Σの中で最も複雑さが小さい論理式をCとする。このとき、Cは対応するブロックの終式の右辺のいずれかに 出現する。また、Cpos [2→Σ:=→⊥]≡Cである。なぜなら、Cは全ての2Σより小さいから代入が生じないからで ある。よって、Cはいずれかの可能世界で反駁される。
9. 2Σとして2Σ\{2C}をとり、4.に戻ってこの手続きを繰り返す。
10. Σ≡となったとき、全てのブロックの終式は反駁されることが示される。
一点からなるイニシャルではないクラスターのとき。対応するブロックは、
2Γ→A1 2Γ|2Θ · · · 2Γ→Am2Γ|2Θ Γ, p1,· · ·, pn→2A1,· · ·,2Am, q1,· · ·ql 2Γ| (2)t
から始まる推移的ブロックであり、可能世界の付値は{p1,· · ·, pn}である。このとき、このブロックの始式はこの可 能世界で反駁される。なぜなら、到達可能関係が付いた可能世界でA1,· · ·, Amが反駁されているので、この可能世界 では2A1,· · ·,2Amが反駁されるからである。
∧,∨,⊃,¬規則のときは、補題3.5.15より、下式も反駁される。
(T)あるいは(T)t規則のときは、
Γ,A, A,∆→Π
Γ,2A,∆→Π (T)
という形をしているが、到達可能関係が付いた可能世界 では2Γ,2Aが妥当であるからΓ, Aも妥当。よって、この可能世界でも2Aが妥当となり、結局下式が反駁される。
故に、終式が反駁される。
二点以上からなるイニシャルではないクラスターのとき。
1. このクラスターに対応するブロックの妥当な履歴をΓとし、このΓをソートしたものを→Γで表す。
2. 対応する全てのブロックを→Γ でソートする。(補題3.5.10より) 3. 対応するブロックの非妥当な履歴の和集合をΣとする。
4. I.H.より、このクラスターから到達可能な他のクラスターの各シーケントは対応する可能世界で反駁される。
5. 対応するブロックに出現する全てのシーケントにpos[2→Σ:=→⊥]を代入したブロックを考える。このクラスターから 到達可能な他のクラスターに対応したブロックの各シーケントに対しては、補題3.5.14より、代入したシーケントも 反駁される。よって、ブロックの始式は対応する可能世界で反駁される。なぜなら、代入前の始式はΓ,→p→→q ,2→A という形をしていて、(Γ,→p→→q ,2→A)pos [2→Σ:=→⊥]≡Γpos [2→Σ:=→⊥],→p→→q ,→⊥,2→A(2→A⊂2→Apos [2→Σ:=→⊥]) となり、2→Aは到達可能な他のクラスターに対応したブロックの終式に出現するからである。
6. ∧,∨,⊃,¬規則のときは、補題3.5.15より、下式も反駁される。
7. (T), (T)t規則のときは、
Γ,B, B,∆→Π Γ,2B,∆→Π (T)
という形をしている。このとき、各ブロックはソートされて いるので、全て対応する可能世界でBは妥当である。すなわち、そのクラスターでBが妥当であるので、2B も妥当である。故に、T規則の下式は反駁される。
8. 6. と7.を繰り返すと、pos [2→Σ:=→⊥] を代入した各終式が反駁されることが分かる。
9. Σの中で最も複雑さが小さい論理式をCとする。このとき、Cは対応するブロックの終式の右辺のいずれかに 出現する。また、Cpos [2→Σ:=→⊥]≡Cである。なぜなら、Cは全ての2Σより小さいから代入が生じないからで ある。よって、Cはいずれかの可能世界で反駁される。
10. 2Σとして2Σ\{2C}をとり、5.に戻ってこの手続きを繰り返す。
11. Σ≡となったとき、全てのブロックの終式は反駁されることが示される。