2025.09.16
https://www.youtube.com/watch?v=DXvjwv_9yHU
神
メモ
一般化されたトレースの扱い面倒すぎる
メモ
証明可能性論理$ \sf \mathrm{PrL}(T,U)のトレース$ \mathrm{tr}(\mathrm{PrL}(T,U))がcoinfiniteのとき，$ \mathsf{L} = \mathsf{GL}_{\alpha = \mathrm{tr}(\mathrm{PrL}(T,U))}，
片方の包含は前の補題から明らか．
もう片方は$ \mathsf{L} \vdash F_n : n \in \mathrm{tr}(\mathrm{PrL}(T,U))から帰結する，と書かれているが，$ \sf GLを含むのかは明らかではなく，算術的健全性を経由するならおそらく$ T \leq Uとなっていないと通らない気がする．
$ Uには任意性があるが，ここはこれを仮定しないとおかしい気がする．
メモ
制作時間2分