2025.08.05
https://gyazo.com/5546bb7ae572a38ac1e459143538dd17
観た
マジでいいな
和田めっちゃいい 表情豊かすぎる
来週で終わりか…
スキルツリーが幻視できるアニメうれしすぎる
マインクラフトすぎるよ
萌え やれすぎてる
一番おもしろいやつが登場
やった/やっている
$ \mathbb{N}に超準元$ \omegaを入れたモデルに自然な$ +,\timesを定義した（ただし$ 0 \times \omega = 0とする）モデルはRobinson算術$ \bf Qのモデルになるが，$ \forall x. (x + 1 \neq x)を証明できない．当然$ \bf PA^-では証明できる．よって真に弱い． 勘違いで$ \Sigma_1完全性を使って明示的に議論すると思ってたけど普通に不完全性から出てくる．
思った
思った
排中律をとりあえず大雑把に一律禁止ではなくて，「これは排中律を使って良い命題です」みたいな様相が明示的に上手く扱える体系を考えたらどうなんだろう，みたいなことは思っているがこの試みが正しいものなのかはよくわかっていない
「排中律を適用しても良いです」という様相が何か別の全然関係ない命題から導かれるとは思えないし結局は命題変数レベルに潰れてしまう気がする．排中律適用可能命題と直ちにそうではない命題で多ソートにするとかなのだろうか？
例えば$ \mathrm{Prop} = \{p,q,...\}と$ \mathrm{DProp} = \{\bar{p},\bar{q},...\}を使って
$ \bar{p} \to p，$ \bar{p} \lor \lnot \bar{p}，みたいな感じで扱えば…
$ \mathbf{Int}_\mathrm{Prop} + \mathbf{Cl}_\mathrm{DProp} + \{\bar{p_i} \to p_i\}_{i \in \N}
あるいは$ \Boxの中では直観主義論理を，外側では古典をやってよい：カプセル化された論理，みたいなものを考えれば…
そんなこと可能なのか？
最小論理+爆発律では排中律と二重否定除去は同値になる．しかし二重否定除去はまあまあ自然だが排中律はちょっと疑わしい．では爆発律が良くないのではという気もするし，実際かなり強い前提のように思える．少なくとも日常の論理で「何でも」言えたらおかしいよな～という直感がある．