正規様相論理Kは決定可能である
参考文献
正規様相論理$ \Lambda
$ \Lambdaが有限フレームのクラス$ \mathbb{F}に対して有限フレーム性を持つとは， $ \Lambdaが$ \mathbb{F}に対して健全かつ弱完全
すなわち，
$ \mathbb{F} \models \Lambda（健全性）
任意の論理式$ \varphiに対し$ \vdash_\Lambda \varphiなら$ \mathbb{F} \models \varphi
任意の論理式$ \varphiに対し$ \mathbb{F} \models \varphi \implies \vdash_\Lambda \varphi（弱完全性）
ある有限フレームのクラス$ \mathbb{F}が存在し，$ \Lambdaが$ \mathbb{F}に対して有限フレーム性を持つことである．
$ \Lambdaの任意の論理式$ \varphiに対し，$ \vdash_\Lambda \varphiならYesを，$ \not\vdash_\Lambda \varphiならNoを出力する実効的な（有限時間で計算可能な）手続き$ \mathscr{P}が存在することである．
論理式の有限集合を$ \Sigmaとする．
正規様相論理$ \mathbf{K}\Sigmaが有限フレーム性を持つ$ \implies$ \mathbf{K}\Sigmaは決定可能．
Def: 部分論理式集合$ \mathrm{Sub}(\varphi)
様相論理式$ \varphiの構造に基づき，$ \varphiの部分論理式の集合を以下のように定める．
1. $ \mathrm{Sub}(p) \coloneqq \{p\}
2. $ \mathrm{Sub}(\bot) \coloneqq \{\bot\}
3. $ \mathrm{Sub}(\varphi \to \psi) \coloneqq \mathrm{Sub}(\varphi) \cup \mathrm{Sub}(\psi) \cup \{\varphi \to \psi\}
4. $ \mathrm{Sub(\Box\varphi)} \coloneqq \mathrm{Sub}(\varphi) \cup \{\Box \varphi\}
注意
$ \mathrm{Sub}(\varphi)は必ず$ \varphiを含む．
Def: 論理式の集合に対する部分論理式集合
論理式の集合$ \Sigmaに対し，$ \mathrm{Sub}(\Sigma)を↓のように定義する．
$ \mathrm{Sub}(\Sigma) \coloneqq \bigcup_{\varphi \in \Sigma} \mathrm{Sub}(\varphi)
Def: 部分論理式に閉じる
論理式の集合$ \Sigmaが部分論理式に閉じているとは，↓を満たしていることとする．
任意の$ \varphi \in \Sigmaに対し$ \mathrm{Sub}(\varphi) \sube \Sigma
Def: 同値関係
Kripkeモデル$ \mathcal{M} \coloneqq \lang W,R,V\rang，$ \Sigmaは部分論理式に閉じた論理式の集合とする． $ W上の同値関係$ \sim_\Sigmaを以下のように定める．
$ w \sim_\Sigma v$ \iff任意の$ \varphi \in \Sigmaに対し$ \mathcal{M},w \models \varphi \iff \mathcal{M},v \models \varphi
$ wによる定まる同値類を$ \lbrack w\rbrack_\Sigmaと書く．
すなわち，$ \lbrack w \rbrack_\Sigma \coloneqq \{ v \in W \mid w \sim_\Sigma v\}
ただし，あまりにも煩雑なので，以降は$ \Sigmaを省略し，単に$ \lbrack w\rbrackと書く．
Kripkeモデル$ \mathcal{M} \coloneqq \lang W,R,V\rang，$ \Sigmaは部分論理式に閉じた論理式の集合とする． 次の要件を満たすKripkeモデル$ \mathcal{M}^f_\Sigma \coloneqq \lang W_\Sigma, R^f, V_\Sigma \rangを，$ \mathcal{M}に対しての$ \Sigma濾過モデルと呼ぶ．（$ \Sigma-filtered model） $ W_\Sigma \coloneqq W / \sim_\Sigma = \{ \lbrack w\rbrack_\Sigma \mid w \in W \}
$ R^fは次の条件を満たす
1: $ wRv \implies \lbrack w \rbrack R^f \lbrack v \rbrack
2: $ \lbrack w \rbrack R^f \lbrack v \rbrack$ \implies任意の$ \Box\varphi \in \Sigmaに対し（$ \mathcal{M},w \models \Box \varphi \implies \mathcal{M},v \models \varphi）
$ V_\Sigma(p) \coloneqq \{ \lbrack w\rbrack_\Sigma \mid w \in V(p) \}．$ p \in \Sigmaとする．
Remark
濾過モデルが必ず存在する保証はない．つまり，条件を満たす$ R^fを必ずしも取ってこれるとは限らない．
Prop 2.1.6
Kripkeモデル$ \mathcal{M} \coloneqq \lang W,R,V\rang，$ \Sigmaは部分論理式に閉じた論理式の集合とする． $ \mathcal{M}の濾過モデルを$ \mathcal{M}^f_\Sigmaとする．
任意の$ \varphi \in \Sigma, w \in Wに対し
$ \mathcal{M},w \models \varphi \iff \mathcal{M}^f_\Sigma, \lbrack w \rbrack_\Sigma \models \varphi
Def 2.1.7
$ W_\Sigma上の二項関係$ R^s, R^lを以下のように定める．
$ \lbrack w \rbrack R^s \lbrack v \rbrack$ \iffある$ w' \in \lbrack w\rbrack, v' \in \lbrack v \rbrackが存在し，$ w'Rv'
$ \lbrack w \rbrack R^s \lbrack v \rbrack$ \iff任意の$ \Box\varphi \in \Sigmaに対し，（$ \mathcal{M},w\models \Box\varphi \implies \mathcal{M},v\models\varphi）
Thm 2.1.8: 最も細かい濾過モデル，最も粗い濾過モデル
$ R^s,R^lによるモデル$ \mathcal{M}^s_\Sigma \coloneqq \lang W_\Sigma, R^s, V_\Sigma \rangと$ \mathcal{M}^l_\Sigma \coloneqq \lang W_\Sigma, R^l, V_\Sigma \rangはそれぞれ$ \mathcal{M}の濾過モデルである．
任意の$ \mathcal{M}の濾過モデル$ \mathcal{M}^f_\Sigma \coloneqq \lang W_\Sigma,R^f,V_\Sigma \rangに対して$ R^s \sube R^f \sube R^l
Remark
元々の$ Rが持っていた性質を無視してもよいなら，任意のモデルに対して濾過モデルが存在する．
Thm 2.1.9: $ \mathbf{K}の有限フレーム性
最小の正規様相論理$ \mathbf{K}は，すべての有限フレームによるフレームクラス$ \mathbb{F}に対して有限フレーム性がある．
proof
$ \mathbf{K}の健全性と$ \mathbb{F}に対しての弱完全性を言えば良い．
I. $ \mathbf{K}の健全性はすでに証明済み．
II.
1. $ \mathbf{K}が$ \mathbb{F}に対して弱完全
$ \iff任意の$ \mathbf{K}無矛盾論理式$ \varphiに対し，$ \varphiは$ \mathbb{F}で充足可能
$ \iff任意の$ \mathbf{K}無矛盾論理式$ \varphiに対し，$ \varphiはある有限フレーム$ \mathcal{F} \in \mathbb{F}で$ \mathcal{F} \models \varphi
これを示す．
2. $ \varphiを$ \mathbf{K}無矛盾論理式とする
3. $ \mathbf{K}は$ \mathbb{F}_\mathbf{K}に対して強完全(証明済み)
$ \iffあるフレーム$ \mathcal{F} \coloneqq \lang W,R\rang \in \mathbb{F}_\mathbf{K}で$ \mathcal{F} \models \varphi
$ \iffある$ V,w \in Wで$ \mathcal{M} \coloneqq \lang \mathcal{F},V\rangとしたとき，$ \mathcal{M},w \models \varphi
4. この$ \mathcal{M}に対して，$ \mathrm{Sub}(\varphi)による濾過モデル$ \mathcal{M}^f_{\mathrm{Sub}(\varphi)}を構成する．
例えば最も細かい濾過モデルを取ってくることが出来る．
5. $ \mathcal{M},w \models \varphi \iff \mathcal{M}^f_{\mathrm{Sub}(\varphi)}, \lbrack w \rbrack_{\mathrm{Sub}(\varphi)} \models \varphi
Prop 2.1.6
6. 2,5より$ \mathcal{M}^f_{\mathrm{Sub}(\varphi)}, \lbrack w \rbrack_{\mathrm{Sub}(\varphi)} \models \varphi
7. $ \mathcal{M}^f_{\mathrm{Sub}(\varphi)}のフレームは有限フレームである．よって1は示された．
I,IIより$ \mathbf{K}は有限フレーム性を持つ．
Cor
$ \mathbf{K}は決定可能である．
$ \mathbf{K}の拡張した論理の決定可能性はあとで示す．