2023.03.12
https://www.youtube.com/watch?v=LNYYlmCPTPY
いいね
面白い
7x7とかは完全にヒント無くなって一個試す以上のことしか出来ないけど…
思った
↓ちょっと怪しいかも
以下のメモより，
論理式が恒真式か自動で判定したい！と思ったとき
標準様相論理の判定計算機を最初に作り，
様相論理から直観主義命題論理への翻訳$ \tau_{\mathbf{K} \Rightarrow \mathbf{J}}
直観主義命題論理から命題論理への翻訳$ \tau_{\mathbf{J}\Rightarrow\mathbf{P}}
を用意すれば良い．
メモ
論理
命題論理$ \mathbf{P}
標準様相論理$ \mathbf{K}
$ \mathbf{P}の論理式の定義に$ \Box \varphiと$ \Diamond \varphiを足したもの．
直観主義命題論理$ \mathbf{J}
性質
論理$ \mathbf{L}は固定し，
$ \varphiは$ \mathbf{L}の論理式とする．
$ \mathcal{H}_\mathbf{L}は$ \mathbf{L}の適当なHilbert証明体系とする．
$ \mathcal{H}_\mathbf{L}で$ \varphiは証明できることを$ \mathcal{H}_\mathbf{L} \vdash \varphiと書く．
$ \mathcal{M}_\mathbf{L}は$ \mathbf{L}のモデルの一つとする．
$ \mathcal{M}_\mathbf{L}で$ \varphiが真であることを$ \mathcal{M}_\mathbf{L} \models \varphiと書く．
計算可能
$ \mathbf{L}のある性質が計算可能であるとは，
次の関数$ f:\Phi \mapsto \{0,1\}が存在することとする．
ただし，$ \mathbf{L}のすべての論理式の集合$ \Phiとする
$ \Phiの論理式$ \varphi \in \Phiが
ある性質を満たすなら0を返す
ある性質を満たさないなら1を返す
仮にある性質が計算可能でない，すなわち計算不能であるなら，
$ fは計算不能/未定義$ \botを返す部分関数であるとする．
ある$ \mathcal{M}_\mathbf{L}と$ \varphiが与えられて，$ \mathcal{M}_\mathbf{L} \models \varphiであるかを判定する
任意の$ \mathcal{M}_\mathbf{L}と$ \varphiについて真偽判定問題が計算可能なら，
$ \varphiが与えられて，任意の$ \mathcal{M}_\mathbf{L}で$ \mathcal{M}_\mathbf{L} \models \varphiであるかを判定する
任意の$ \mathcal{M}_\mathbf{L}で$ \mathcal{M}_\mathbf{L} \models \varphiな論理式$ \varphiは恒真式あるいはトートロジーと呼ぶ． 任意の$ \varphiについて恒真性判定問題が計算可能なら，
当然ながら
恒真性判定計算可能$ \implies真偽判定計算可能．
健全性，完全性
健全性
$ \mathcal{H}_\mathbf{L}が健全である/健全性があるとは，
任意の論理式$ \varphiについて次を満たす．
$ \mathcal{H}_\mathbf{L} \vdash \varphi$ \implies$ \varphiが恒真式
完全性
$ \mathcal{H}_\mathbf{L}が完全である/完全性があるとは，
任意の論理式$ \varphiについて次を満たす．
$ \varphiが恒真式$ \implies$ \mathcal{H}_\mathbf{L} \vdash \varphi
広義の完全性
$ \mathcal{H}_\mathbf{L}が健全かつ完全なとき，広義の完全性があるという．
帰結
命題論理$ \mathbf{P}及び標準様相論理$ \mathbf{K}は
広義の完全性を満たす．
直観主義命題論理は標準様相論理の特殊ケースであると考えることが出来る
すなわち，$ \mathbf{K}が満たす性質を満たす
真偽計算可能及び恒真性計算可能，広義の完全性を満たす．
命題論理は直観主義命題論理の特殊ケースと考えることも出来る