様相論理KHのKripke不完全性
メモ
に全ての証明を書いた．
$ \mathsf{H} \equiv \Box (\Box\Phi \leftrightarrow \Phi) \to \Box \Phi
Boolos 1993, p.148に記載あり
証明のスケッチ
$ \sf Hが成り立つフレームでは$ \sf Lが成り立つ．逆も成り立つ．
すなわち，$ F \vDash \Box(\Box A \leftrightarrow A) \to \Box A \iff F \vDash \Box(\Box A \to A) \to \Box A
$ \bf KHでは公理$ \sf 4のインスタンスが証明できないことが意味論的な議論によって示される．
$ \mathbf{KH} \nvdash \Box A \to \Box\Box A
しかし$ \bf GLでは公理$ \sf 4は証明出来る
$ \mathbf{GL} \vdash \Box A \to \Box\Box A
以上の議論より不完全．
↑の議論はミスだった．修正します
証明のスケッチ(2)
全体を通し，命題変項を$ pとして一つ固定する．
まず，$ \sf Hのためのフレームはある意味で$ \sf Lのそれと一致することを見る．
ただしこれは公理図式ではなく$ pによるインスタンスであることに注意せよ．一般には成り立たない．
Lem.1
$ \Box (\Box p \leftrightarrow p) \to \Box pを妥当にするフレーム$ \mathcal{F}は$ \Box (\Box p \to p) \to \Box pを妥当にする．逆も然り．
すなわち，$ \mathcal{F} \vDash \Box (\Box p \leftrightarrow p) \to \Box p \iff \mathcal{F} \vDash \Box (\Box p \to p) \to \Box p．
次に，意味論的な議論によって，公理$ \sf 4の$ pによるインスタンスは$ \bf KHでは証明不能であることを確かめる．
Lem.2
$ \mathbf{KH} \nvdash \Box p \to \Box\Box p．
Lem2より，直ちに$ \sf Lの$ pのインスタンスも$ \bf KHでは証明不能であることがわかる．
Cor.3
$ \mathbf{KH} \nvdash \Box(\Box p \to p) \to \Box p
proof
もし証明できると仮定する．そこから$ \bf GLでの証明と同じように，公理$ \sf 4の$ pインスタンスが証明出来る．しかしLem2でそれは不可能とわかったのでおかしい．
Thm.4
「$ \bf KHの定理を全て妥当にするフレームクラス$ \mathbb{F}があって．任意の論理式$ Aに対して，$ \mathbb{F} \vDash Aならば$ \mathbf{KH} \vdash A」とはならない．
proof
もし反して，なるとしよう．このとき，そのようなフレームクラスがあるので$ \mathbb{F}_\mathbf{KH}とする．
$ Aは任意だったから，$ \mathbb{F}_\mathbf{KH} \vDash \Box(\Box p \to p) \to \Box pならば$ \mathbf{KH} \vdash \Box(\Box p \to p) \to \Box pとしよう．
今Cor3より$ \mathbf{KH} \nvdash \Box(\Box p \to p) \to \Box pだったから$ \mathbb{F}_\mathbf{KH} \nvDash \Box(\Box p \to p) \to \Box pとなる．
フレームクラス上妥当性の定義より，何らかの$ \mathcal{F} \in \mathbb{F}_\mathbf{KH}が存在して，$ \mathcal{F} \nvDash \Box(\Box p \to p) \to \Box pとなる．
したがってLem1より，$ \mathcal{F} \nvDash \Box (\Box p \leftrightarrow p) \to \Box pとなる．
しかし，そもそも$ \mathcal{F}は$ \bf KHの定理を全て妥当にするフレームだったから，当然$ \mathcal{F} \vDash \Box(\Box p \to p) \to \Box pとならなければおかしい．
以上より破綻する．よって最初の仮定がおかしく，そのようなフレームクラスは存在し得ない．❏