様相論理GL
$ \mathsf{GL}の公理及び推論規則
公理
$ \mathsf{K}: \Box(\varphi \to \psi) \to (\Box \varphi \to \Box \psi): 様相論理の公理K $ \mathsf{G}: \Box(\Box \varphi \to \varphi) \to \Box\varphi: 様相論理の公理L 推論規則
ここでは，命題変数をある算術の文に移す写像$ fを変換という．
すなわち，命題変数$ p,q,\dotsとは何らかの算術の文を表すとする．
あくまでも，定義域は命題変数だけである．
ある$ fに対し，次のように全ての様相論理の論理式に対して拡張した$ f_TをT解釈という．$ Tは$ \mathsf{PA}の再帰的加算な拡大理論とする．
1. $ f_T(p) \equiv f(p)
2. $ f_T(\bot) \equiv \bot
3. $ f_T(\varphi \to \psi) \equiv f_T(\varphi) \to f_T(\psi)
4. $ f_T(\Box \varphi) \equiv \mathsf{Pr}_T(\ulcorner f_T(\varphi) \urcorner)
$ T解釈$ f_Tによって，様相論理の論理式$ \varphiの真偽を$ T \vdash f_T(\varphi)かどうかで定めることで，様相論理の意味論を与えることが出来る．
様相論理の論理式$ \varphiとする．$ \vdash_\mathsf{GL} \varphi$ \implies任意の$ fに対し$ T \vdash f_T(\varphi)
proof: 証明の長さの帰納法で．
$ \mathsf{Con}_T \equiv \lnot \mathsf{Pr}_T(\ulcorner \bot \urcorner)として定義したことを考えると
$ \mathsf{Con}_T \equiv \lnot\Box\botという様相論理式で表される．
Gödel文とは$ \vdash \pi \leftrightarrow \lnot \mathsf{Pr}_T(\ulcorner \pi \urcorner)なる文$ \piであった．
よって形式化すれば様相論理式としては$ \lnot\Box\bot \leftrightarrow \lnot\Box\lnot\Box\botである．
これは$ \mathsf{GL}で証明可能である．すなわち
$ \vdash_\mathsf{GL} \lnot\Box\bot \leftrightarrow \lnot\Box\lnot\Box\bot
proof:
$ \to
1. $ \vdash_\mathsf{K} \bot \to (\Box\bot \to \bot)
2. $ \vdash_\mathsf{K} \bot \to \lnot\Box\bot（$ \lnotdef）
3. $ \vdash_\mathsf{K} \Box \bot \to \Box\lnot\Box\bot（Nec）
4. $ \vdash_\mathsf{K} \lnot\Box\bot \to \lnot\Box\lnot\Box\bot
5. $ \vdash_\mathsf{GL} \lnot\Box\bot \to \lnot\Box\lnot\Box\bot（$ \vdash_\mathsf{K} \varphi \implies \vdash_\mathsf{GL} \varphi）
$ \leftarrow
1. $ \vdash_\mathsf{K} \lnot\Box\bot \to \lnot\Box\bot
2. $ \vdash_\mathsf{K} \lnot\Box\bot \to (\Box \bot \to \bot)
3. $ \vdash_\mathsf{K} \Box\lnot\Box\bot \to \Box(\Box \bot \to \bot)（Nec）
4. $ \vdash_\mathsf{GL} \Box\lnot\Box\bot \to \Box \bot（公理$ \mathsf{G}）
5. $ \vdash_\mathsf{GL} \lnot\Box\lnot\Box\bot \to \lnot\Box\bot
纏めて$ \vdash_\mathsf{GL} \lnot\Box\bot \leftrightarrow \lnot\Box\lnot\Box\bot
様相論理の論理式$ \varphi,\psiとする．
$ \varphiに現れる命題変数$ pを$ \psiで置き換えた論理式を$ \varphi_{\lbrack p \mapsto \psi \rbrack}で表すとする．
命題2は
$ \vdash_\mathsf{GL} \lnot\Box\bot \leftrightarrow (\lnot\Box p)_{\lbrack p \mapsto \lnot\Box\bot\rbrack}
すなわち，$ \lnot \Box pの不動点は$ \lnot\Box\botであることを主張している．
全ての様相論理式が不動点を持つわけではない．
$ \lnot pの不動点は存在しない．
$ \varphiとして存在すれば$ \vdash_\mathsf{GL} \varphi \leftrightarrow (\lnot p)_{\lbrack p \mapsto \varphi \rbrack}，すなわち$ \vdash_\mathsf{GL} \varphi \leftrightarrow \lnot\varphiで矛盾する．
定義: 箱入り
命題変数$ pが様相論理式$ \varphiにおいて箱入りである
$ \iff$ \varphiに含まれる$ pが全て$ \Boxの中にある
例
$ \Box(\Box p \to p)で$ pは箱入りである．
$ \Box p \to pで$ pは箱入りではない．右の$ pが$ \Boxの中ではない
定義: $ \mathsf{At}(\varphi)
様相論理式$ \varphiの全ての命題変数の集合を$ \mathsf{At}(\varphi)で表す．
定義: $ \boxdot
$ \varphiは様相論理式とする．
$ \boxdot \varphi \equiv \varphi \land \Box\varphi
定理.1: $ \mathsf{GL}の不動点定理 様相論理式$ \varphi，命題変数$ pとし，$ pは$ \varphiで箱入りとする．
次を満たす様相論理式$ \psiが存在する．
$ \mathsf{At}(\psi) \sube \mathsf{At}(\varphi) - \{p\}かつ$ \vdash_\mathsf{GL}\boxdot(p \leftrightarrow \varphi) \leftrightarrow \boxdot(p \leftrightarrow \psi)
系.1
様相論理式$ \varphi，命題変数$ pとし，$ pは$ \varphiで箱入りとする．
次を満たす様相論理式$ \psiが存在する．
$ \mathsf{At}(\psi) \sube \mathsf{At}(\varphi) - \{p\}かつ$ \vdash_\mathsf{GL} \psi \leftrightarrow \varphi_{\lbrack p \mapsto \psi \rbrack}
定理1から導かれる．実際には逆だが．
系.2
様相論理式$ \varphi，命題変数$ p,qとし，$ pは$ \varphiで箱入り，$ q \notin \mathsf{At}(\varphi)とする．
次を満たす様相論理式$ \psiが存在する．
$ \vdash_\mathsf{GL} (\boxdot(p \leftrightarrow \varphi) \leftrightarrow \boxdot(q \leftrightarrow \varphi_{\lbrack p \mapsto q \rbrack})) \to (p \leftrightarrow q)
参考文献