2025.08.07
https://gyazo.com/4e10e5ef1004a70d7647d41585153a11
前：2025.08.06
後：2025.08.08
#日報
やった
「Robinson算術$ \bf QはCobhamの最弱の算術理論$ \bf R_0（Cobhamの最弱の算術）よりは真に強く$ \bf PA^-よりは真に弱い」という事実を形式化した．
https://gyazo.com/d05af925616ed5effd025fe9a4da917c
https://gyazo.com/f9aaf000c730c9a53086f6f2ac7cfd19
要するにめちゃくちゃパズルをしました．もう二度としたくない類の面倒さではある．
$ \bf Q \vdash R_0
めっちゃ面倒だった．数項の処理が本当にダルく…
$ \bf PA^- \vdash Qの方は$ \bf \omega \cup \{\omega\}上に適当に演算をさだめると上手く反例モデルになる．
これLeanではOption Nでやっているからsome nとnoneまみれになってめっちゃ面倒だった．
思った
移り変わりが激しく，移り変わりが激しいということを指摘され，そうですね…となった．
メモ
まさか大学にJ.J.Zeman, "Modal Logic"があることは知らなかった（絶対に無いだろと思って探してもなかった）しかしどこにもなく，終わった
思った
最近ずっと眠いの何なんだろう
メモ
本質的決定不能性（無矛盾なRE拡大が決定不能）と本質的不完全性（無矛盾な拡大理論が決定不能）は互いに同値．
←の一番使う道具立てが少ない証明はLindenbaum補題っぽい技法を使う．
対偶を示す．決定可能な理論$ Uが存在するとする．
Gödel数順に論理式を並べ，拡大理論を膨らましていく．その極大理論を作ればそれは無矛盾かつ完全でかつ計算可能になる：与えられた論理式からGödel数を計算して$ T_{\ulcorner \varphi \urcorner}を見れば入るかは入らないかは計算可能になる．これはG1を満たさないので本質的不完全性を導く．