2024.04.09
https://gyazo.com/d14e206e0f6bdb6eb3b33480be73540e
https://gyazo.com/04b711507d69ba83ac361999152fe7bc
思った
「様相論理に関する事実を定理証明支援系で形式化していまして…」と自己紹介したら「そもそもプログラムを書いて証明が出来る(証明が形式化できる)ってどういうことですか?」と訊かれて返答に困ってしまった(自分の中ではかなり自然なものとして受け入れていたので何を説明すればよいのか困った) やった
残すは↓みたいな細々とした補題が10個ぐらい残ってて気が狂う
メモ
$ \vdash \Diamond^n\bigwedge \Diamond^{-n} \Gamma \to \bigwedge \Gammaか?
ただし$ \Gamma \sube \Diamond^n\Omegaとする.すなわち$ \Gammaは$ \Diamond^n \varphiの形以外の論理式は含まれていない.
$ \Gamma = \{ \Diamond^n \gamma_1,\dots,\Diamond^n\gamma_m \}とする.
$ \Diamond^{-n}\Gamma = \{\gamma_1,\dots,\gamma_m\}
$ \bigwedge \Diamond^{-n}\Gamma \equiv \gamma_1 \land \cdots\land \gamma_m
$ \Diamond^n\bigwedge \Diamond^{-n}\Gamma \equiv \Diamond^n (\gamma_1 \land \cdots\land \gamma_m)
他方当然$ \bigwedge \Gamma \equiv \Diamond^n \gamma_1 \land \cdots \land \Diamond^n \gamma_nだから
この問題は結局こういう形に落ち着く
$ \vdash \Diamond^n (\gamma_1 \land \cdots\land \gamma_m) \to \Diamond^n \gamma_1 \land \cdots \land \Diamond^n \gamma_n
そしてこれは正しい.例↓
https://gyazo.com/202099f36160337849a71d2e3cd64e2b
しかしこの事実を形式化するには異常な労力がかかっている
いいね
https://nicothumb2img.vercel.app/image/sm43624032#.png https://nico.ms/sm43624032