2024.06.07
https://gyazo.com/bc4ac52207f1bf0fd6bbbd2b06a6360d
思った
ドキュメントを書きたくないという強い意志
メモ
補題がガリガリかけて本当に楽しい状態へ入ってきた
主に2つのことを証明した．
$ \mathbf{S4} \vdash \varphi \iff \mathbf{K4} \vdash \varphi^b
技術的要請によって形式化においては変換は様相論理から様相論理の論理式への写像としているが，実際には変換するとどちらの変換でも$ \Boxは消える，すなわち命題論理の論理式として良い．
このとき，まず次の補題が得られる．
$ \mathbf{Triv} \vdash \varphi \iff \mathbf{Cl} \vdash \varphi^\top
$ \mathbf{Ver} \vdash \varphi \iff \mathbf{Cl} \vdash \varphi^V
その他，特定の論理については次の含意が成り立つ．
$ \mathbf {K4} \vdash \varphi \implies \mathbf{Cl} \vdash \varphi^\top
$ \mathbf{GL} \vdash \varphi \implies \mathbf{Cl} \vdash \varphi^V
今，公理$ \mathsf{L}のTriv変換$ \sf L^\topを考えるとこれが古典論理のトートロジーとならないものが存在するため，$ \bf K4 \nvdash \mathsf{L}であり，$ \bf K4 < GLである（$ \bf GLは$ \bf K4より真に強い．）
また公理$ \sf TのVer変換$ \mathsf{T}^Vを考えるとこれも古典論理のトートロジーとならないものが存在するため，$ \bf S4 \not\leq GLである．（$ \bf GLは$ \bf S4より強くない）
いいね
ナイス