2025.07.10
https://gyazo.com/e0029ca884ce5d7bc2936cbd47ef5898
wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
観た
神
あっぱれすぎ
メモ
すいません誰か持ってたらマジでください．
https://nicothumb2img.vercel.app/image/sm12398475#.png https://nico.ms/sm12398475
メモ
$ \Gamma, \varphi \vdash_\mathbf{K} \psiが$ \varphiの長さに依存してネセシテーションを$ n回使うことによって証明できたとする．このとき$ \Gamma \vdash_\mathbf{K} \Box^{\leq n} \varphi \to \psi．
メモ
これ形式化している自分の体系だと成り立つのだけど，成り立ち方がなんかおかしい気がする．
$ \Gamma, \varphi \vdash_\mathbf{K} \psiなら$ \Gamma \vdash_\mathbf{K} \varphi \to \psi
これが言える．$ \bf Kでなくてもよい．もっといえば最小論理を含むなら成立する．
これは当たり前か．
よくわからなくなってきてしまった．証明を追えばいいか…
メモ
メモ
スケッチは上手く言ってる．あとは細かい議論が通ればよい．
本当に通るんですか？
…