2022.08.07
https://tableauxive.vercel.app/api/image?width=900&height=640&inference=(P∧(P→Q))→Q#.png
前：2022.08.06
後：2022.08.08
#日報
やった
Deno deploy & Vercelで証明図画像生成器
出来た！
モーダス・ポネンス$ (P \land (P \to Q)) \to Q
https://tableauxive.vercel.app/api/image?width=900&height=640&inference=(P∧(P→Q))→Q#.png
構成的ジレンマ$ (P \to R) \to (Q \to R) \to (P \lor Q \to R)
https://tableauxive.vercel.app/api/image?width=900&height=640&inference=(P→R)→(Q→R)→(P∨Q→R)#.png
観た
ローリング☆ガールズ 第8話『』
リコリス・リコイル 第6話
Extreme Hearts 第1話
Extreme Hearts 第2話
なんか奇妙だ…
スペース☆ダンディ 第1話
いいね
https://tweet-card.now.sh/1555894362625740800.jpg?lang=ja https://twitter.com/Reijibnuy2/status/1555894362625740800
Moetron好きすぎる
思った
物語の公理自体が奇妙、非直感的だがそこから導かれるあらゆる事象が正しいようなアニメをキテレツアニメとする
鹿島 亮; "コンピュータサイエンスにおける様相論理"は到達可能性関係(様相論理)を$ \rightsquigarrowで表しているけど本当にこの記号しかなかったのか？と思ってしまう
戸次 大介; "数理論理学"をちゃんと読むとそもそもタブローで$ \timesとなるのは論理式$ \varphiについて$ \varphi, \lnot \varphiであった
便宜的に$ \varphi, \lnot \varphi \implies \botと書く
つまり例えば$ (P\to Q), \lnot(P \to Q)という2式が登場した瞬間問答無用でアウトで，これを$ P, \lnot Qとバラす必要とかは一切なかった
まあ毎回やってたら重いか？そんなこともないか
述語論理の論理式が証明可能か判定する関数
述語論理のタブロー量化子変換規則，外側から当てれば良いのか？
$ N(0)∧\forall i.(N(i)→N(s(i)))→N(s(s(0)))みたいなものは外側から当てれば確かに成立したけど…