2024.03.21
https://gyazo.com/3367dbb33e6a1ea70d10db0d1772cc4e
やっぱりEDのテンションだけがおかしいと思う.
やった
証明を手伝ってくれた両名,ありがとう!
自然言語で書かれた証明を頑張ってLean 4(またはその他の定理証明支援系)で書き直すことで元の証明の細かなミスやギャップに気付くといった事態がここ数日よくあって、いい傾向だと思う ところで形式化された証明をおれが普通の人間用に自然言語に書き直すところでミスが頻発しているのですが…(泣) 知った
思った
学生ライセンスが切れてGitHub Copilotが今日から切れた結果、「適当に補完してくれないかな〜」と思いながら無の時間を待つ場面が頻発してメチャクチャになってる 誰か払ってほしい.深刻に
思った
様相論理の健全性定理(強バージョン:すなわち$ \Gamma \vdash \varphi \implies \Gamma \vDash_{\mathbb{F}(\Lambda)} \varphi )を示すのが破滅的に出来ないという問題が合ったが,これは盛大に勘違いだったことが判明した. $ \bigwedge \Gamma,\bigvee \Gammaの取り扱いが面倒だと思っていたが,全然しなくても良いことが判明した.
結局,強健全性定理が示せたのでこれで様相論理の強弱を形式化出来るように…
とりあえず↓だけ示した.
$ \mathbf{S4} <^\Lambda \mathbf{S5}:$ \mathbf{S5}は$ \mathbf{S4}より真に強い
次の$ \varphiが存在する:$ \nvdash_\mathbf{S4} \varphiかつ$ \vdash_\mathbf{S5} \varphi
$ \mathbf{S5} =^\Lambda \mathbf{KT4B}
$ \vdash_\mathbf{S5} \varphi \iff \vdash_\mathbf{KT4B} \varphi
いいね
https://nicothumb2img.vercel.app/image/sm43553422#.png https://nico.ms/sm43553422
思った
思ったほど日報が見られているということがわかった.
形式化した事実は頻繁にツイートしたほうが良い気がした.
メモ
メモ
現在のAT-Xの取締役のプロデューサーの名前が「東不可止」ですごかった アンストッパブルすぎる