文献あり

様相論理の有限モデル性について

809

代表的な様相論理の体系は、有限モデル性という行儀のよい性質を満たします。本稿では、この有限モデル性の証明に用いられる濾過法という手法を見ていきます。最後に補足として、有限モデル性と決定可能性との関係を説明します。

本稿の説明のベースとなっているのはThe Open Logic Projectの様相論理の教科書です。また、妥当性の定義などは大西『論理学』をもとにしています(説明の簡略化のため一部改変しています)。本稿が、これらの文献で説明されていることを自分用に嚙み砕いて書いたメモのようなものであることを予めご了承ください。詳細を知りたい方は参考文献を参照してください。

準備

以下では、様相論理の語彙は加算無限個の命題変項の集合 $PV$ と $\neg, \land, ◻$ からなるものとし、これにより帰納的に構成される論理式の集合を $Fml$ とする。その他の通常の論理結合子は糖衣構文として定義する(e.g. $◊ A \overset{def}{=} \neg ◻ \neg A$ )。

可能世界意味論

ここでは、(正規)様相論理のモデル論として、可能世界意味論(possible world semantics)というものを導入する。詳細な説明は行わないので、興味のある方には適宜教科書などを参照していただきたい。

フレーム

様相論理のフレーム(frame)とは、以下により定まる組 $⟨ W, R ⟩$ のことである(以下では単に「フレーム」という)。

$W$ : 非空な集合
- これを可能世界(possible world)の集合という
$R \subseteq W^{2}$
- これを到達可能性関係(accesibility relation)という

モデル

様相論理のモデル(model)とは、以下により定まる組 $⟨ W, R, v ⟩$ のことである(以下では単に「モデル」という)。

$⟨ W, R ⟩$ : フレーム
$v : W \times PV \to {0, 1}$
- これを付値(valuation)という
付値の拡張: 付値 $v$ は以下のようにして $W \times Fml \to {0, 1}$ となるよう帰納的に拡張される
- $v (w, \neg A) = 1 \overset{def}{⟺} v (w, A) = 0$
- $v (w, A \land B) = 1 \overset{def}{⟺} v (w, A) = 1 and v (w, B) = 1$
- $v (w, ◻ A) = 1 \overset{def}{⟺}^{\forall} x \in W . w R x ⟹ v (w, A) = 1$

妥当性

$A \in Fml$ と、モデル $M = ⟨ W, R, v ⟩$ ・フレーム $F$ について、

$M ⊨ A \overset{def}{⟺}^{\forall} w \in W . v (w, A) = 1$
- このことを、 $A$ がモデル $M$ 上で妥当である(valid)という
- これが成り立たない $M$ を $A$ に対する反例モデル(counter model)という
$F ⊨ A \overset{def}{⟺}^{\forall} v : (F 上の付値) . ⟨ F, v ⟩ ⊨ A$
- このことを、 $A$ がフレーム $F$ 上で妥当であるという

以下では、全てのフレームのクラスを $F_{K}$ とする。さらに、フレームの到達可能性関係に対して、以下のような制約を加えることを考える。

$T$ : 反射性 ( $^{\forall} x \in W . x R x$ )
$B$ : 対称性 ( $^{\forall} x, y \in W . x R y ⟹ y R x$ )
$D$ : 継続性 ( $^{\forall} x \in W .^{\exists} y \in W . x R y$ )
$4$ : 推移性 ( $^{\forall} x, y, z \in W . x R y and y R x ⟹ x R z$ )
$5$ : ユークリッド性 ( $^{\forall} x, y, z \in W . x R y and x R z ⟹ y R z$ )

これらの制約を加えて得られるフレームのクラスを、 $K$ の後ろに対応するラベルを付けた名前で表す(e.g. $F_{KT}$ は反射的な $R$ を持つモデルのクラス)。慣習的に、 $KT 4, KT 5$ をそれぞれ $S 4, S 5$ という。

このようにフレームの定義を変えると、妥当になる論理式も変わる。フレームのクラスに対応して定まる妥当な式の集合を論理として定める。

論理

フレームのクラス $F_{K}$ に対して、様相論理 $K$ を任意の $F \in F_{K}$ 上で妥当な論理式の集合とする。その他のフレームのクラスに対しても同様に論理を定める。

また、論理 $Λ$ に対して $A \in Λ$ となることを、 $A$ が $Λ$ で妥当であるという。

有限モデル性

論理 $Λ$ を定義するフレームのクラスを $F_{Λ}$ とする。 $Λ$ が有限モデル性(finite model property)を満たすとは、以下が成り立つことである: 任意の $A \in Fml$ に対して、 $A$ に対する $F_{Λ}$ 上の反例モデルが存在するならば、 $A$ への推論に対する $F_{Λ}$ 上の有限の反例モデルが存在する

ただし、有限のモデルとは、モデル $M = ⟨ W, R, v ⟩$ であって $W$ が有限集合であるものを指す。

有限モデル性を証明するためには、所与の推論に対する任意の反例モデル $M = ⟨ W, R, v ⟩$ ( $W$ が無限集合でありうる)を、有限の反例モデルに変換する手続きを与える必要がある。より具体的には、 $W$ の要素の個数を、反例モデルとしての性質を失わないように「減らす」ないし「圧縮する」必要がある。

そこで方針として有力なのは、適当な同値関係 $\equiv$ を定めて $W$ の要素を「同一視」し、商集合 $W / \equiv$ を考えることで世界の個数を減らす、という方法である。このようなモデルの構成方法を濾過法 (filtration method)という。

同値関係を考えることで付値は自然に定められるが、到達可能性関係の定義はそこまで自明ではない。対象となる論理体系に応じてどのように到達可能性関係を設定するかが、有限モデル性の証明における焦点となる。

濾過法

定義

濾過法を定義するための道具立てとして、2つの概念を用意する。

$Γ \subseteq Fml$ について、 $Γ$ が部分論理式について閉じている(closed under sub-formulae)とは、以下が成り立つことである。
$^{\forall} A \in Γ . sub (A) \subseteq Γ$
ただし $sub (A)$ は、 $A$ の部分論理式( $A$ 自身も含む)の集合を表す

モデル $M = ⟨ W, R, v ⟩$ 、および部分論理式について閉じている $Γ \subseteq Fml$ が与えられたとき、 $W$ 上の同値関係 $\equiv_{Γ}$ を以下のように定める (これは確かに同値関係になる)
$x \equiv_{Γ} y \overset{def}{⟺}^{\forall} A \in Γ . v (x, A) = 1 ⟺ v (y, A) = 1$
以下では、この同値関係により定まる同値類を $[w]$ のように( $Γ$ を明示せずに)表す

これらを用いて、モデルに対する「濾過」の仕様を以下のように定める。

濾過

モデル $M = ⟨ W, R, v ⟩$ 、および部分論理式について閉じている $Γ \subseteq Fml$ に対して、 $M$ の $Γ$ による濾過(filtration)とは、以下を満たすモデル $M^{*} = ⟨ W^{*}, R^{*}, v^{*} ⟩$ である

$W^{*} = {[w] ∣ w \in W}$
任意の $x, y \in W$ に対して、
1. $x R y ⟹ [x] R^{*} [y]$
2. $[x] R^{*} [y] ⟹ (^{\forall} ◻ A \in Γ . v (x, ◻ A) = 1 ⟹ v (y, A) = 1)$
$v^{*} ([w], p) = v (w, p)$

$R$ の定義は一見複雑であるが、2-1は $R$ がwell-definedになるための条件であり、2-2は「 $R^{*}$ が $◻$ に関する $v$ の挙動を模倣すること」を要求していると(非形式的に)捉えることができる。

濾過は一意に定まるとは限らない(「仕様」と書いたのはそのためである)。 $W^{*}, v^{*}$ は定義から一意に定まるが、 $R^{*}$ の部分に自由度がある。
本当は $R^{*}, v^{*}$ がwell-definedになることの確認が必要であるが、割愛する。
濾過は部分論理式について閉じている $Γ \subseteq Fml$ に対してのみ定まる。よって、これ以降で「 $M$ の $Γ$ による濾過」と書いた場合、 $Γ$ が部分論理式について閉じていることを(明示せずに)前提にすることがある。

前述のとおり、濾過を定義する動機は、反例モデルとしての性質を保ったまま世界の個数を減らすことであった。以下の定理は、濾過法は $Γ$ の範囲内では付値を変えないことを主張しており、「反例モデルとしての性質を保つ」という部分を保証している。

モデル $M$ の $Γ \subseteq Fml$ による任意の濾過 $M^{*} = ⟨ W^{*}, R^{*}, v^{*} ⟩$ は以下を満たす。
$^{\forall} A \in Fml .^{\forall} w \in W . A \in Γ ⟹ (v (w, A) = 1 ⟺ v^{*} ([w], A) = 1)$

$A$ の構成に関する帰納法で示す。 $Γ$ は部分式について閉じているので、帰納法の各ステップで出現する $A$ の部分式もまた $Γ$ の要素となることに注意する。

$A = p \in PV$ の場合: 定義より明らか
$A = \neg B, A = B \land C$ の場合: 複合式に対する付値の定義を用いて部分式の条件へと分解し、帰納法の仮定を適用すればよい(詳細は割愛)。
$A = ◻ B$ の場合:
$\begin{aligned} v (w, ◻ B) = 1 & ⟺^{\forall} x \in W . w R x ⟹ v (x, B) = 1 \\ ⟺^{\forall} [x] \in W^{*} . w R x ⟹ v (x, B) = 1 \\ \overset{(*)}{⟺}^{\forall} [x] \in W^{*} . [w] R^{*} [x] ⟹ v (x, B) = 1 \\ ⟺^{\forall} [x] \in W^{*} . [w] R^{*} [x] ⟹ v^{*} ([x], B) = 1 (∵ 帰納法の仮定) \\ ⟺ v^{*} ([w], ◻ B) = 1 \end{aligned}$

$(*)$ の証明: $(\Rightarrow)$ については、仮定より $◻ B \in Γ, v (w, ◻ B) = 1$ であり、 $[w] R^{*} [x]$ を仮定すると、定義8の2-2から $v (x, B) = 1$ となるので成立。 $(\Leftarrow)$ については、定義8の2-1より $w R x ⟹ [w] R^{*} [x]$ となるので成立。

例

まだ濾過の定義が与えられただけで、実際にそれが存在するかは分かっていない。以下では、一般的に構成できる2つの濾過の例を挙げる。

最も粗い・最も細かい

モデル $M = ⟨ W, R, v ⟩$ と部分論理式について閉じている $Γ \subseteq Fml$ に対して、 $W^{*}$ と $v^{*}$ を定義8の1,3の通りに定めたとき、

最も細かい濾過は、 $R^{*}$ を以下のように定義することで得られる
$[x] R^{*} [y] \overset{def}{⟺}^{\exists} x^{'} \in [x] .^{\exists} y^{'} \in [y] . x^{'} R y^{'}$
最も粗い濾過は、 $R^{*}$ を以下のように定義することで得られる
$[x] R^{*} [y] \overset{def}{⟺}^{\forall} ◻ A \in Γ . v (x, ◻ A) ⟹ v (y, A) = 1$

最も細かい濾過・最も粗い濾過は、どちらも実際に濾過になる。証明は割愛する。

到達可能性関係の性質

モデル中の到達可能性関係が持つ性質のうちの一部は、濾過に対してそのまま「引き継がれる」という特徴がある。

モデル $M$ の $Γ \subseteq Fml$ による任意の濾過 $M^{*} = ⟨ W^{*}, R^{*}, v^{*} ⟩$ は以下を満たす。

$R$ は反射的 $⟹$ $R^{*}$ は反射的
$R$ は継続的 $⟹$ $R^{*}$ は継続的
$R = W^{2}$ $⟹$ $R^{*} = (W^{*})^{2}$
- $R = W^{2}$ となることを $R$ が普遍的であるという。普遍的なフレームのクラスにより定まる論理は $S 5$ と一致することが知られている。

定義8の2-1( $x R y ⟹ [x] R^{*} [y]$ )より、明らかに成り立つ。

この定理は、対称性・推移性などに対しては一般には成り立たない。しかし、 $R^{*}$ をうまく「設計」することで、濾過にも同じ性質を引き継がせることができる。この「設計」のパーツとして必要なものをまずは定義する。

モデル $M = ⟨ W, R, v ⟩$ に対して、 $W$ に関する2項述語を(メタレベルで)以下のように定義する。

$C_{1} (x, y) \overset{def}{⟺}^{\forall} ◻ A \in Γ . v (x, ◻ A) = 1 ⟹ v (y, A) = 1$
$C_{2} (x, y) \overset{def}{⟺}^{\forall} ◻ A \in Γ . v (y, ◻ A) = 1 ⟹ v (x, A) = 1$
$C_{3} (x, y) \overset{def}{⟺}^{\forall} ◻ A \in Γ . v (x, ◻ A) = 1 ⟹ v (y, ◻ A) = 1$
$C_{4} (x, y) \overset{def}{⟺}^{\forall} ◻ A \in Γ . v (y, ◻ A) = 1 ⟹ v (x, ◻ A) = 1$

ここで定義した $C_{1}$ ～ $C_{4}$ に対しては、直観的な説明を与えることができる。

$C_{1}$ : 濾過の定義の2-2に該当する → 濾過となるために必要
$C_{2}$ : (ある意味で) $C_{1}$ の「逆」になっている→ 対称性を反映
$C_{3}$ : $x$ で $◻ A$ が成り立つなら任意の到達可能な $y$ でも $◻ A$ となるということなので、 $◻ A \to ◻ ◻ A$ を意図したものになっている → 推移性を反映
$C_{4}$ : $C_{2}$ と $C_{3}$ の両方を反映

以下の定理は、これらの説明を形式的に表現している。

モデル $M = ⟨ W, R, v ⟩$ と部分論理式について閉じている $Γ \subseteq Fml$ に対して、 $W^{*}, v^{*}$ を定義8の1,3の通りに定めたとき、

$[x] R^{*} [y] ⟺ C_{1} (x, y) and C_{2} (x, y)$ であるならば、以下が成り立つ
- $R^{*}$ は対称的である
- $R$ が対称的ならば、 $⟨ W^{*}, R^{*}, v^{*} ⟩$ は $M$ の $Γ$ による濾過である
$[x] R^{*} [y] ⟺ C_{1} (x, y) and C_{3} (x, y)$ であるならば、以下が成り立つ
- $R^{*}$ は推移的である
- $R$ が推移的ならば、 $⟨ W^{*}, R^{*}, v^{*} ⟩$ は $M$ の $Γ$ による濾過である
$[x] R^{*} [y] ⟺ C_{1} (x, y) and C_{2} (x, y) and C_{3} (x, y) and C_{4} (x, y)$ であるならば、以下が成り立つ
- $R^{*}$ は対称的かつ推移的である
- $R$ が対称的かつ推移的ならば、 $⟨ W^{*}, R^{*}, v^{*} ⟩$ は $M$ の $Γ$ による濾過である
$[x] R^{*} [y] ⟺ C_{1} (x, y) and C_{3} (x, y) and C_{4} (x, y)$ であるならば、以下が成り立つ
- $R^{*}$ は推移的かつユークリッド的である
- $R$ が推移的かつユークリッド的ならば、 $⟨ W^{*}, R^{*}, v^{*} ⟩$ は $M$ の $Γ$ による濾過である

(3)の証明のみ与える(その他の場合もだいたい同様である)。

$R^{*}$ の対称性・推移性
- 対称性: $[x] R^{*} [y]$ を仮定する。定義より $C_{1} (w, w^{'}) ⟺ C_{2} (w^{'}, w)$ , $C_{3} (w, w^{'}) ⟺ C_{4} (w^{'}, w)$ であるから、明らかに $[y] R^{*} [x]$ が成り立つ。
- 推移性: $[x] R^{*} [y], [y] R^{*} [z]$ を仮定する。 $[x] R^{*} [z]$ を示すためには、上で示した対称性より、 $C_{1} (x, z)$ と $C_{3} (x, z)$ を示せば十分である。
  - $C_{1}$ : $v (x, ◻ A) = 1$ を仮定する。これと $C_{3} (x, y)$ より $v (y, ◻ A) = 1$ であり、これと $C_{1} (y, z)$ より $v (z, A) = 1$ となるので、 $C_{1} (x, z)$ が成り立つ。
  - $C_{3}$ : $v (x, ◻ A) = 1$ を仮定する。これと $C_{3} (x, y)$ より $v (y, ◻ A) = 1$ であり、これと $C_{3} (y, z)$ より $v (z, ◻ A) = 1$ となるので、 $C_{3} (x, z)$ が成り立つ。
$⟨ W^{*}, R^{*}, v^{*} ⟩$ が濾過になること: $R$ が対称的・推移的であることを仮定する
- 定理の条件より、定義8の1,3は満たされている
- 定義8の2について:
  1. $x R y$ を仮定する。 $C_{1}$ ～ $C_{4}$ の成立を示せば、 $[x] R^{*} [y]$ がいえる。
    - $C_{1}$ : $◻ A \in Γ$ かつ $v (x, ◻ A) = 1$ を仮定する。後者と $x R y$ より $v (y, A) = 1$ となる。 $◊$ の方も同様。よって $C_{1} (x, y)$ が成り立つ。
    - $C_{2}$ : $◻ A \in Γ$ かつ $v (y, ◻ A) = 1$ を仮定する。 $x R y$ と $R$ の対称性から $y R x$ であるから、これと後者より $v (x, A) = 1$ となる。 $◊$ の方も同様。よって $C_{2} (x, y)$ が成り立つ。
    - $C_{3}$ : $◻ A \in Γ$ かつ $v (x, ◻ A) = 1$ を仮定する。 $x R y, y R z$ と $R$ の推移性から $x R z$ であるから、これと後者より $v (z, A) = 1$ となり、 $z$ の任意性より $v (y, ◻ A) = 1$ がいえる。 $◊$ の方も同様。よって $C_{3} (x, y)$ が成り立つ。
    - $C_{4}$ : $C_{2}$ と $C_{3}$ の議論を組み合わせることで、同様に示される。
  2. $[x] R^{*} [y]$ を仮定すると、 $C_{1} (x, y)$ が成り立つので、2-2の条件が満たされる。

有限モデル性の証明

まず、濾過によって確かに世界の個数を有限個までに抑えられていることを確認する。

$Γ \subseteq Fml$ が有限集合ならば、モデル $M$ の $Γ$ による任意の濾過 $M^{*} = ⟨ W^{*}, R^{*}, v^{*} ⟩$ に対して、 $| W^{*} | \leq 2^{| Γ |}$ が成り立つ(よって $M^{*}$ は有限のモデルである)。

ある関数 $π : W^{*} \to P (Γ)$ を構成し、 $π$ が単射になることを示せば、 $| W^{*} | \leq | P (Γ) | = 2^{| Γ |}$ が示される。 $π$ を以下のように定義する。
$π ([w]) \overset{def}{=} {A \in Γ ∣ \forall w^{'} \in [w] . v (w^{'}, A) = 1}$

$π$ が単射になることを示すために、 $[x], [y] \in W^{*}$ を任意にとり、 $[x] \neq [y]$ を仮定する。 $π ([x]) \neq π ([y])$ を示すために、 $π ([x]) = π ([y])$ を仮定すると、任意の $A \in Γ$ に対して以下が成り立つ。
$^{\forall} w \in [x] . v (w, A) = 1 ⟺^{\forall} w \in [y] . v (w, A) = 1$
このとき、同値関係 $\equiv_{Γ}$ の定義より $x \equiv_{Γ} y$ となる(任意の $A \in Γ$ に対して $v (x, A) = 1 ⟺ v (y, A) = 1$ となることは簡単に確かめられる)。よって $[x] = [y]$ となり、最初の仮定に反する。以上より $π$ は単射である。

この補題を用いると、有限モデル性は簡単に示せる。

$K$ は有限モデル性を満たす。

$A \in Fml$ に対して $K$ の反例モデル $M = ⟨ W, R, v ⟩$ が存在すると仮定する。このとき、ある $w_{0} \in W$ が存在して $v (w_{0}, A) = 0$ となる。

$Γ = sub (A)$ とする。 $M$ の $Γ$ による濾過 $M^{*} = ⟨ W^{*}, R^{*}, v^{*} ⟩$ として、(たとえば)最も細かい濾過を与えると、

$Γ$ は有限集合なので、上の補題より、 $M^{*}$ は有限のモデルである
$⟨ W^{*}, R^{*} ⟩ \in F_{K}$
- $F_{K}$ は全てのフレームのクラスであることに注意(よって、 $M^{*}$ として最も細かい濾過を与えていることに必然性はなく、何であれ1つ濾過を与えれば十分である)
定理1より $v^{*} ([w_{0}], A) = 0$ となるので、 $M^{*}$ は $A$ に対する反例モデルになっている

このようなモデル $M^{*}$ の存在より、 $K$ は有限モデル性を満たすことが分かる。

定理2より、対称性・継続性・普遍性はもとのモデルから濾過へと引き継がれるので、 $KT, KD, S 5$ の有限モデル性も同様に示される。

定理2が適用できないような論理に対しては、定理3を利用する。その例として $KB$ の有限モデル性を示す。

$KB$ は有限モデル性を満たす

$K$ の場合と濾過の与え方以外は同様である。濾過については、 $R^{*}$ を以下のように定める。
$[x] R^{*} [y] \overset{def}{⟺} C_{1} (x, y) and C_{2} (x, y)$
このとき、定理3より $R^{*}$ が対称的になるので、濾過 $M^{*}$ は $KB$ のモデルになる。

このように、 $C_{1}$ ～ $C_{4}$ をうまく使えば、 $K 4$ や $S 4$ などの有限モデル性も同様に示される。ただし、この手法では、 $K 5$ や $KD 5$ の有限モデル性は示せない(ユークリッド性の扱いが難しい)。

決定可能性

有限モデル性は、決定可能性の証明に利用できるという点で「嬉しい」性質である。ただし、決定可能である(decidable)とは、体系内での論理式の真偽を判定する計算可能な手続き(アルゴリズム)が存在することである。本当は適当な計算理論を仮定して計算可能性について論じるべきであるが、今回は非形式的な「アルゴリズム」の概念を利用した説明に留める。

$K$ は決定可能である。

$A \in Fml$ が $K$ で妥当であるかどうかを、以下2つの計算を並行して行うことで判定できる(一方が終了したら他方も終了することとする)。

$K$ に対して健全かつ完全な証明体系(e.g. シーケント計算)によって、妥当式を枚挙する。枚挙された論理式の中に $A$ が出現したら、yesを出力して停止する。
$A$ に出現する命題変項を $p_{1}, \dots, p_{k}$ と列挙する。そのうえで、 $n = 1, 2, \dots$ に対して以下を計算する。
- $W = {0, \dots, n - 1}$ とする
- $R \subseteq W \times W$ を全て列挙する( $n^{2}$ 個)
- $v : W \times PV \to {0, 1}$ として、 $p_{1}, \dots, p_{k}$ 以外には0を割り当てるようなものを全て列挙する( $2^{k}$ 個)
- それぞれの $v, R$ に対して、以下を計算する
  - 各 $w \in W$ に対して、 $v (w, A)$ を計算する(モデルの有限性より計算可能)。 $v (w, A) = 0$ であったら、noを出力して停止する。

このように定まるアルゴリズムは、確かに $A \in Fml$ が $K$ で妥当であるかどうかを判定している。実際、

$A$ が妥当である場合: 手続き1によって妥当であることが判明するので、このとき確かに停止してyesを出力する。
$A$ が妥当ではない場合: $A$ に対する反例モデルが存在するから、 $K$ の有限モデル性より、 $A$ に対する有限の反例モデルが存在する。手続き2によってこの反例モデルに相当する $W, R, v$ が見つかるので、このとき確かに停止してnoを出力する。