2025.09.19
https://gyazo.com/4d9f4976815ca751f33335efb203d5f8
メモ
今日やったことを図解してみましょう
https://gyazo.com/e926c377cf47f493dd4249e327236fa6
元のモデル$ Mの点$ aの前に$ k個の点列を差し込んだ（付値は$ aと同じとする）モデルを考える．これを骨延長モデル$ M_{a,k}とよぶことにする．
このとき図から明らかに
元のモデルの高さを$ h(M)とすると，骨延長モデルの高さは$ h(M) + k．
元のモデルを$ aで切って$ k-単純拡張したモデルと，骨延長モデル上に$ k - 1による点生成モデルは完全に同型になる．したがってここから様相同値が生える．
つまり$ a \preceq w \in Mに対して$ M, w \models \varphi \iff M_{a,k}, w \models \varphi．
これを形式化する．どうやって？ ←頑張るしかなく…
この他のことはほぼ終わった．上を仮定して，次のことは形式化済み．
定理 (Visser?)
証明可能性論理$ L = \mathrm{PrL}(T,U)のトレース$ \alphaとする．
1. $ \alphaが補無限のとき，$ L = \mathsf{GL}_\alpha
2. $ L \not\sube \mathsf{S}のとき，$ \alphaは補有限であり$ L = \mathsf{GL}^-_\alpha
残っているケースは$ L \sube \mathsf{S}かつ$ \alphaが補有限のとき．
次のことが知られている．
定理(Artemov)
$ L \sube \mathsf{S}かつ$ \alphaが補有限のとき，証明可能性論理$ L' := L + \{ F_n : n \notin \alpha \}として$ L = L' \cap \mathsf{GL}^-_\alpha．
このとき，$ L' \sube \mathsf{S}でありかつ$ \mathrm{tr}(L') = \omega．すなわち，$ \mathsf{GL}_\omega \sube L' \sube \mathsf{S}．
この$ L'の性格を調べると次のことがわかる．
定理(Beklemishev)
$ \mathsf{GL_\omega} \sub \mathsf{D}および$ \mathsf{D} \sub \mathsf{S}の間に証明可能性論理は存在しない．よって
$ L'は$ \mathsf{GL}_\omega, \mathsf{D}, \mathsf{S}のいずれか．
簡単な計算により$ \mathsf{GL}_\omega \cap \mathsf{GL}^-_\alpha = \mathsf{GL}^-_\alpha
系
$ L \sube \mathsf{S}かつ$ \alphaが補有限のとき，$ Lは$ \mathsf{GL}^-_\alpha，$ \mathsf{D} \cap \mathsf{GL}^-_\alpha，$ \mathsf{S} \cap \mathsf{GL}^-_\alphaのいずれか．
よって最終的に次のことがわかる．
1. $ L\sube \mathsf{S}かつ$ \alphaが補有限のとき，$ Lは$ \mathsf{GL}^-_\alpha，$ \mathsf{D} \cap \mathsf{GL}^-_\alpha，$ \mathsf{S} \cap \mathsf{GL}^-_\alphaのいずれか．
2. $ L \not\sube \mathsf{S}のとき，$ L = \mathsf{GL}^-_\alpha
3. それ以外のとき，$ L = \mathsf{GL}_\alpha
思った
open Classical使いまくり もはやおれの手は排中律で染まっており、何が実際には決定可能かそうでないかもよくわからない 幾何的な直感で明らかすぎる事実があり、紙とペンなりホワイトボードなりに書けば直ちにわかることだが、それを形式化してコードに落とし込むと300行かかるとかはザラにある 要するにKripkeフレームをLeanで扱うのは破滅的に面倒だということです ここは苦しい 皆さんもぜひお楽しみください
Leanの形式化された各補題で構成するKripkeフレームの到達関係が決定可能かどうかを排中律を使わずにきちんと構成的な証拠を与えることはおそらく可能だとは思うが，それを成し得た数ヶ月後には私はおそらく発狂していると思う．
いいね
https://nicothumb2img.vercel.app/image/sm45418474#.png https://nico.ms/sm45418474
神
思った
なんとなく思ったけど第1不完全性定理の主張そのものは完全性定理の完全性と意味が違うけども系として「正しい命題の集まりは証明できる命題のそれと一致しない」が出るからその意味では同じ完全性の用法ではないかと思ったがどうなのだろうか