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

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

• $A=p\in\PV$の場合: 定義より明らか
• $A=\lnot B, A=B\land C$の場合: 複合式に対する付値の定義を用いて部分式の条件へと分解し、帰納法の仮定を適用すればよい(詳細は割愛)。
• $A=\Box B$の場合:
  $$ \begin{align*} v(w,\Box B)=1 &\iff \Forall x\in W.wRx\implies v(x,B)=1\\ &\iff \Forall [x]\in W^\ast.wRx\implies v(x,B)=1\\ &\stackrel{(\ast)}{\iff} \Forall [x]\in W^\ast.[w]R^\ast[x]\implies v(x,B)=1 \\ &\iff \Forall [x]\in W^\ast.[w]R^\ast[x]\implies v^\ast([x],B)=1 \quad(\because 帰納法の仮定)\\ &\iff v^\ast([w],\Box B)=1 \end{align*} $$

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

定義8の2-1($xRy\implies[x]R^\ast[y]$)より、明らかに成り立つ。

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

1. $R^\ast$の対称性・推移性

   • 対称性: $[x]R^\ast[y]$を仮定する。定義より$C_1(w,w')\iff C_2(w',w)$, $C_3(w,w')\iff C_4(w',w)$であるから、明らかに$[y]R^\ast[x]$が成り立つ。
   • 推移性: $[x]R^\ast[y],[y]R^\ast[z]$を仮定する。$[x]R^\ast[z]$を示すためには、上で示した対称性より、$C_1(x,z)$と$C_3(x,z)$を示せば十分である。
     • $C_1$: $v(x,\Box A)=1$を仮定する。これと$C_3(x,y)$より$v(y,\Box A)=1$であり、これと$C_1(y,z)$より$v(z,A)=1$となるので、$C_1(x,z)$が成り立つ。
     • $C_3$: $v(x,\Box A)=1$を仮定する。これと$C_3(x,y)$より$v(y,\Box A)=1$であり、これと$C_3(y,z)$より$v(z,\Box A)=1$となるので、$C_3(x,z)$が成り立つ。

2. $\tuple{W^\ast,R^\ast,v^\ast}$が濾過になること: $R$が対称的・推移的であることを仮定する

   • 定理の条件より、定義8の1,3は満たされている
   • 定義8の2について:
     1. $xRy$を仮定する。$C_1$～$C_4$の成立を示せば、$[x]R^\ast[y]$がいえる。
        • $C_1$: $\Box A\in\Gamma$かつ$v(x,\Box A)=1$を仮定する。後者と$xRy$より$v(y,A)=1$となる。$\Diamond$の方も同様。よって$C_1(x,y)$が成り立つ。
        • $C_2$: $\Box A\in\Gamma$かつ$v(y,\Box A)=1$を仮定する。$xRy$と$R$の対称性から$yRx$であるから、これと後者より$v(x,A)=1$となる。$\Diamond$の方も同様。よって$C_2(x,y)$が成り立つ。
        • $C_3$: $\Box A\in\Gamma$かつ$v(x,\Box A)=1$を仮定する。$xRy,yRz$と$R$の推移性から$xRz$であるから、これと後者より$v(z,A)=1$となり、$z$の任意性より$v(y,\Box A)=1$がいえる。$\Diamond$の方も同様。よって$C_3(x,y)$が成り立つ。
        • $C_4$: $C_2$と$C_3$の議論を組み合わせることで、同様に示される。
     2. $[x]R^\ast[y]$を仮定すると、$C_1(x,y)$が成り立つので、2-2の条件が満たされる。

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

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

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

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

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

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

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

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

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

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

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