2024.10.16
https://gyazo.com/7649b8a88609fb537520e4225e6a7d97
観た
面白すぎて聲出た
読んだ
ナイス
自分懐古風ラブコメいけますやらせてください
メモ
バスに乗り遅れてシッチャカメッチャカになってる
ゼミに出席不能になってしまった
思った
様相選言特性$ \vdash \Box A \lor \Box B \implies \vdash A ~\text{or}~ \vdash Bからデネセシテーションが出てくることに気づいてなかった $ \vdash \Box A \implies \vdash \Box A \lor \Box A \implies \vdash A
こういう自明な系に気付けないのをなんとかしたい…
形式化した（簡単すぎるので）
ただしこれを使う証明は問答無用でnoncomputableになる．
なぜか2回PR出してマージしてしまった…
読んだ
タブロー計算の停止可能性から健全性&完全性を証明するのおもしろいと思った．
帰ったらまた調べるけど$ \bf K以外の拡張論理に関しての規則は何を追加するんだろう？
思った
?!
https://gyazo.com/c4c8a53ee3cbf9b67539529666a16c6e
Memo
帰ったらやること
既存のModal.Formulaにもう一つ追加で，様相論理の否定標準形Modal.NegationNormalFormula(alias: Modal.NNFormula)を定義し，相互に翻訳可能かつ意味論上で同値であることを証明する
これをしないとタブロー計算が果てしなく面倒なことになる
直観主義論理で必要なはずのValuationのhereditaryを完全に無視して共通化してしまった． フレームレベルだけなら行けるのか？と思うが…
選言特性とかはもうこっちの意味論で形式化したほうが早いんじゃないか？と思う メモ
あと2週間で形式化についてのゼミ資料を作る必要が発生したのちょっと面白い
こういうの作ったことないからわからん…どうしたらいいんだ