鹿島 亮; "コンピュータサイエンスにおける様相論理"
メモ
この本では次の論理を扱う
および
様相μ計算（便宜上\bold{C}_\muと表す）
論理\mathscr{L}
論理\mathscr{L}の論理式\varphiについて
1. \varphiが論理\mathscr{L}において恒真
2. \varphiは\mathcal{H}_\mathscr{L}で証明可能
健全性は1→2
完全性は2→1
様相論理\mathscr{L} = \bold{K},\bold{CTL},\bold{CTL*},\bold{C}_\mu,\bold{PDF}のKripkeモデルについて
KripkeモデルK = \lang S, \rightsquigarrow, f\rangとしたとき
Kが有限集合なとき特別に有限Kripkeモデルと呼ぶ
任意の有限Kripkeモデルとその任意の状態で常に真か？を判定する問題を恒真性判定問題と呼ぶ
任意の論理式\varphiについて次は同値である
\varphiが\mathscr{L}恒真ではない
\varphiを偽とするようなあるモデルMおよびそのモデルのある状態sが存在する
次のことが同値
\varphiが\mathscr{L}恒真でない
状態数がg({Lh}(\varphi))（ただしgは計算可能関数、g(x) = 2^xとか）以下のあるモデルMおよびその状態sで\varphiが偽
標準的な様相論理\bold{K}（以下正規様相論理K）
有限Kripkeモデルにおいてその論理式\varphiの真偽が決定可能
論理式\varphiが恒真でないことは次と同値である
状態数が2^{Lh(\varphi)}以下の有限Kripkeモデルのある状態で偽となるようなモデルが存在する
正規様相論理Kの論理式の集合\Gammaについて（有限，無限問わず）
\Gammaの\bold{K}充足可能
\Gammaの全ての要素\gammaについてM,s \models \gammaを満たすようなMおよびMの状態sが存在するとき
\Gammaが\mathcal{H}_\bold{K}矛盾
\Gammaの有限個の\gamma_1 \cdots \gamma_n，1 \leq nについて
\mathcal{H}_\bold{K} \vdash \lnot( \gamma_1 \land \cdots \land \gamma_n)
\Gammaが\mathcal{H}_\bold{K}無矛盾
\Gammaが\mathcal{H}_\bold{K}矛盾ではない
\Gammaが極大\mathcal{H}_\bold{K}無矛盾
\mathcal{H}_\bold{K}無矛盾かつ
任意の論理式\varphiについて\varphi \in \Gammaか\lnot \varphi \in \Gamma
\mathcal{H}_\bold{K}のカノニカルモデル
省略
定理1
任意の論理式集合について次のことは同値
1. \Gammaが\mathcal{H}_\bold{K}無矛盾
2. \Gammaが\bold{K}充足可能
証明
2→1: 対偶を示す
1→2: カノニカルモデルが\Gammaを充足することを示せば良いらしい（
なんで？）
\bold{K}の完全性の証明
任意の\bold{K}論理式\varphiについて
\varphiが\bold{K}恒真なら\mathcal{H}_\bold{K} \vdash \varphi
対偶を示す
\mathcal{H}_\bold{K} \not\vdash \varphiなら\varphiが\bold{K}恒真ではない
\mathcal{H}_\bold{K} \not\vdash \varphiから\{ \lnot \varphi \}は\mathcal{H}_\bold{K}無矛盾
仮に\{\lnot \varphi\}が\mathcal{H}_\bold{K}矛盾だった場合\lnot\lnot\varphi = \varphiとなって前提と矛盾する
よって\{ \lnot \varphi \}は\bold{K}充足可能
定理1より
よって\lnot \varphiは\bold{K}充足可能
論理式集合に関しての充足の定義より
よってM,s \models \lnot \varphi \iff M,s \not\models \varphiとなるようなモデルMとその状態sが存在することを示された
\bold{K}の意味論の定義より
つまり\varphiは\bold{K}恒真ではない
恒真の定義より
これ以上はコンパクト性定理に関するが特に使わなさそうなので省略