2024.02.11
https://gyazo.com/78e5bfba5d6a39d7b73a1a2310b5dfdf
観た
形式化した
正確には,公理$ \bf Lは推移的かつ逆整礎なフレームを規定することを. 健全性は公理集合に無関係に示されるので.
メモ
全ての煩雑さは
論理式$ \varphi,\psiでは素朴に$ \varphi \odot \psi \equiv \psi \odot \varphi($ \odot = \lor,\land)では無いことに起因する.$ \varphi \odot \psi \not\equiv \psi \odot \varphi
あくまで↓である
$ \Vdash \varphi \odot \psi \iff \Vdash \psi \odot \varphi
$ \vdash \varphi \odot \psi \iff \vdash \psi \odot \varphi
これによって$ \Gammaを論理式の集合としたとき$ \bigwedge \Gammaが一意に決まらず/noncomputableでシッチャカメッチャカになってしまう
メモ