GLのKripke完全性
$ \bf GLは非反射的かつ推移的な有限フレームのクラスに対して完全.
以下メモ.散発的に書く.
メモ
以下は古い!いずれ書き直す.
否定完全な部分論理式集合
$ \mathrm{Sub}(A)を$ Aの部分論理式集合とする.
明らかに有限集合.
$ Aの否定完全な部分論理式の集合$ \mathrm{Sub}^\lnot(A) := \mathrm{Sub}(A) \cup \{ \lnot B \mid B \in \mathrm{Sub}(A) \}と定める.
これは一般的な用語ではない.
もちろん$ \mathrm{Sub}^\lnot(A)も有限部分集合.
MEMO
$ \Lambda, X極大無矛盾集合
論理式の集合$ Yが$ \Lambda, X極大無矛盾集合とは,
$ Yが$ \Gamma無矛盾,すなわち$ Y \nvdash \botかつ,
$ Y \sube Xかつ,
任意の$ Xの部分集合$ S \sube Xに対して,$ Yが極大であることとする.
すなわち,$ Y \sub Sのとき,$ Sは$ \Lambda無矛盾ではない.
GLカノニカルモデル
$ \bf GLのカノニカルモデルは$ Aの部分論理式に依存して定義される.
$ \mathcal{M}_A = \lang W, \mathord{\prec}, V\rangを論理式$ Aに対しての$ \bf GLカノニカルモデルとする.
$ Wは$ \lang \mathbf{GL}, \mathrm{Sub}^\lnot (A) \rang極大無矛盾集合の集合
$ X \prec Y \iff ^\forall \Box B \in X. \lbrack B, \Box B \in Y \rbrack ~\&~ ^\exists \Box B \in Y ,\lnot \Box B \in X
ただし$ Aは今後自明なので省略する.
今$ \mathcal{M}は有限モデルである.
なぜなら$ \lang \mathbf{GL}, \mathrm{Sub}^\lnot (A) \rang極大無矛盾集合は高々$ 2^{|\mathrm{Sub}(A)|}のバリエーションしか存在しないため.
今$ Xを$ \lang \mathbf{GL}, \mathrm{Sub}^\lnot (A) \rang極大無矛盾集合とする.すなわち$ X \in \mathcal{M}.W
$ B \in \mathrm{Sub}(A)について,$ \mathcal{M}, X \vDash B \iff B \in X
証明
特に$ \Box B \in \mathrm{Sub}(A)について$ X \vDash \Box B \implies \Box B \in Xか?
対偶を示す.$ \Box B \notin Xとして$ X \nvDash \Box Bを示す.
$ X_0 := \{ C, \Box C \mid \Box C \in X \}とする.
すなわち,$ X_0 := \Box^{-1} X \cup \Box\Box^{-1} X.
今,$ \{ \Box B, \lnot B \} \cup X_0は$ \mathbf{GL}無矛盾である.
逆に$ \mathbf{GL}無矛盾だと仮定する.
このとき,何らかの$ \Gamma_0 \sube X_0が存在して$ \vdash_\mathbf{GL} \Box B \land \lnot B \land \bigwedge \Gamma_0 \to \botとなる.
すなわち,$ \Gamma_0 \vdash_\mathbf{GL} \Box B \to B.
文脈ありネセシテーションより$ \Box \Gamma_0 \vdash_\mathbf{GL} \Box (\Box B \to B). $ \bf GLの公理$ \sf Lより$ \Box \Gamma_0 \vdash_\mathbf{GL} \Box B.
今$ \Box \Gamma_0は$ \{ \Box C_1, \dots \Box C_n, \Box\Box D_1, \dots,\Box\Box D_n \}の形をしているから,$ \vdash_\mathbf{GL} \bigwedge \Box \Gamma_0 \iff \vdash_\mathbf{GL} \Box C_1 \land \Box C_n \land \cdots \land \Box \Box D_1 \land \Box\Box D_mである.
今,$ \vdash_\mathbf{GL} \mathsf{4}つまり$ \vdash_\mathbf{GL} \Box p \to \Box \Box pであることに注意すると,$ \Box\Box D_iは$ \Box D_iに還元しても良い.
すなわち,$ \Delta := \{ \Box C_i \mid \Box C_i \in \Box \Gamma_0 \} \cup \{ \Box D_i \mid \Box\Box D_i \in \Box \Gamma_0 \}とすると$ \vdash_\mathbf{GL} \bigwedge \Box \Gamma_0 \iff \vdash_\mathbf{GL} \bigwedge \Deltaになる.
このとき,$ \Delta \sube Xであるから,結局$ X \vdash_\mathbf{GL} \Box Bが言える.
$ Xの$ \lang \mathbf{GL}, \mathrm{Sub}^+ (A) \rang極大無矛盾性および$ \Box B \in \mathrm{Sub}(A)に注意すれば,$ \Box B \in Xが言える.しかしこれは前提に反する.
$ \{ \Box B, \lnot B \} \cup X_0に対してLindenbaum補題を通して$ \lang \mathbf{GL}, \mathrm{Sub}^+ (A) \rang極大無矛盾集合$ Y \supe \{ \Box B, \lnot B \} \cup X_0を得る. この$ Yに対し,$ X \prec Y,$ Y \nvDash Bが示される.よって$ X \nvDash \Box B.OK.