補に閉じた論理式集合とそれを用いた様相論理の有限フレーム性証明
Motivation
$ \bf GLはこの方法でなくとも，濾過法による同値関係で通常の$ \bf GLのカノニカルモデルを割ったモデルを考えれば完全性(有限フレーム性)が示すことが出来る． しかし$ \bf Grzは少なくともこの方法でないと証明が出来ないと（思う．試したが出来なかった）
$ \bf Grzを同様に定義すると，well-definedにならない．
論理式$ Aの補complement$ -Aを以下のように定める．
$ A \equiv \lnot Bなら$ -A \equiv B
そうでないなら$ -A \equiv \lnot B
論理式の集合$ Xに対して相補的な集合$ \bar{X} \equiv X \cup \{ A \mid -A \in S \}とする．
もちろん，$ Xが有限集合なら$ \bar{X}も有限集合である．
論理式の集合$ X \sube \bar{S}に対して，$ Xが$ Sで補に閉じているとは
任意の$ A \in Sに対して$ A \in Xまたは$ -A \in X
Memo
なぜこれが否定$ \lnotではうまく行かないかは実際やってみると良いが，回らない $ --A \not\equiv Aではない．
$ --(\lnot\lnot A) \equiv -(\lnot A) \equiv A \not\equiv \lnot \lnot A．
$ Xが$ \Lambda無矛盾のとき，$ X \vdash_\Lambda Aかつ$ X \vdash_\Lambda -Aとなることはありえない，という事実が成り立つため，通常の方法によってLindenbaum補題と同じような主張が言える． すなわち，
任意の$ X \sube \bar{S}が$ \Lambda無矛盾なら，$ Sで補に閉じた$ \Lambda無矛盾な$ X \sube X' \sube \bar{S}が構成できる．
remark
特に，有限集合が$ \Lambda無矛盾であることが有限時間で判定できるのならば，この手続きは有限時間で終了する．
Prop: CCCSの性質
$ Xは$ \Lambda無矛盾かつ$ Sで補に閉じた有限集合（以下CCCS）とする．
以下の性質が成り立つ．
$ \bot \notin X
$ A \in Sとして
$ A \in X \iff X \vdash_\Lambda A
$ A \in Sなら$ A \in X \iff - A \notin X
$ A \to B,A,B \in Sとして
$ A \to B \in X \iff \lbrack A \in X \implies -B \notin X \rbrack
$ A \to B \notin X \iff \lbrack A \notin X ~\&~ -B \in X \rbrack
remark
$ Sが$ \mathrm{Sub}(A)のような部分論理式で閉じている集合とした場合，$ A \to B \in Sから$ A,B \in Sが直ちに成り立つことに注意せよ．
Def: コンプリートモデル
CCCSでカノニカルモデルのようなもの（名前がないのでとりあえずコンプリートモデルと呼ぶことにする）を考えると，これは$ \bf GLと$ \bf Grzの完全性を示すのに非常に便利な道具として使える．
$ \mathbf{GL}コンプリートモデル$ M_\mathbf{GL} := \lang W_\mathbf{GL}, R_\mathbf{GL},\Vdash_\mathbf{GL} \rang
$ W_\mathbf{GL}を$ \Lambda = \mathbf{GL}, S = \mathrm{Sub}(A)としたCCCSの集合とする．
$ \mathbf{Grz}コンプリートモデル$ M_\mathbf{GL} := \lang W_\mathbf{Grz}, R_\mathbf{Grz},\Vdash_\mathbf{Grz} \rang
$ W_\mathbf{Grz}を$ \Lambda = \mathbf{Grz}, S = \{ B, \Box(\Box B \to B) \mid B \in \mathrm{Sub(A)\}}としたCCCSの集合とする．
付値は$ X \Vdash_{\Lambda} p \iff p \in Xとする．