Harropの補題
主張
論理式の有限集合$ \Sigmaとする
正規様相論理$ \mathbf{K}\Sigmaが有限フレーム性を持つなら，$ \mathbf{K}\Sigmaは決定可能． 定義
正規様相論理$ \Lambda
Kripkeフレーム$ \mathcal{F} = \lang W, R \rangに対し$ Wが有限集合なら$ \mathcal{F}を有限フレームという． $ \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を出力する実効的な（有限時間で計算可能な）手続き$ Pが存在することである．
解説
すなわち，正規様相論理が有限公理化可能であるなら，その決定可能性は有限フレーム性に還元される．
証明
1.
「与えられた論理式が$ \Sigmaに含まれるか？」判定手続きは実効的に構成可能．（$ \Sigmaが有限だから）
よって「$ \vdash_{\mathbf{K}\Sigma} \varphiか？」を判定する手続き$ Pも実効的に構成可能
2.
「$ \not\vdash_{\mathbf{K}\Sigma} \varphiか？」を判定する手続き$ Qを以下のように構成する．
$ Q_1: 有限フレームをすべて枚挙する手続き
$ Q_2: 有限フレーム$ \mathcal{F}と入力の論理式$ \psiに対し「$ \mathcal{F}で$ \psiが妥当か？($ \mathcal{F} \models \psi?)」を判定する手続き
$ Q_1,Q_2は実効的に存在する．ここから$ Q_3を実効的に構成する．
$ Q_3: $ Q_1で列挙されるフレームに対し$ \bigwedge\Sigmaが妥当になるかを$ Q_2で判定することでフィルターする．
すなわち，$ Q_3は$ \Sigmaを妥当にするフレームをすべて枚挙する．
$ \not\vdash_{\mathbf{K}\Sigma} \varphiであるとき，$ \Sigmaを妥当にするフレーム$ \mathcal{F}で$ \varphiが非妥当になる．
したがって
$ Q: $ Q_3で列挙されるフレームを$ \varphiを$ Q_2に入れていき，Noを出力したときYesを出力するように反転させた手続き
3. あとは，$ P,Qを並列に走らせれば決定可能となる．
系
任意の有限集合$ \Sigma \sube \{\mathsf{T,B,4,D}\}に対し$ \mathbf{K}\Sigmaは有限フレーム性を持つ．
したがって，$ \bf K,KT,S4,S5などはすべて決定可能である．
参考文献