2023.11.14
https://www.youtube.com/watch?v=MtTBqIAQ434
おめでとう！
https://s3.fedibird.com/cache/media_attachments/files/111/404/125/250/053/932/original/79e685f724597e1e.png
メモ
lake updateで走るpost update hookがバグっていて，空行が入れ込まれてしまっている．
これによってelanに上手く引数が渡ってくれない．
思った
もっと他に書くべきことがあった気がする．
一応工夫点もあって，命題論理の場合証明木の高さは高々自然数で押さえられるハズなので，そのことを陽に扱っている
木の高さについての帰納法が使えるハズという利点もある
が
カットの深さが2以上ならいいのだが，1と0の場合だけ上手く行ってない
多分おれが間違っていて何かをミスっている
高さを入れ込むようにしたはいいものの結局メチャクチャになって散々になっている
あってるのかはよくわからない．
特に書き換え系Rew系の扱いについては全く知らないので…
内容自体のメモ
$ Tの対角化関数$ \mathrm{diag}_T(\sigma)は，1個の自由変数を持つ部分文$ \sigmaを受け取って，$ T \vdash \sigma(\ulcorner \sigma \urcorner)かどうか？をBool値$ \lbrack T \vdash \sigma \rbrackとして計算する関数とする．
すなわち$ \mathrm{diag} : \mathrm{SubSentence_1 \to \mathtt{2}}
以下
$ \lbrack T \vdash \sigma \rbrack = \mathtt{t}であることは，そのまま普通に$ T \vdash \sigmaと書くことにし，
$ \lbrack T \vdash \sigma \rbrack = \mathtt{f}であることは，$ T \nvdash \sigmaと書くことにする
$ \mathrm{diag}(\sigma)は計算可能関数である．したがって（かなり一般化された）表現可能性定理/LO.FirstOrder.Arith.FirstIncompleteness.representationより$ \mathrm{diag}_Tのグラフが$ Tで表現可能であり，その表現された論理式を$ \gamma_{\mathrm{diag}_T}(x, y)とする． 部分文$ \rho(x) \equiv \gamma_{\mathrm{diag}_T}(x, \ulcorner \mathtt{f} \urcorner)とする．1個の自由変数を持つ部分文である．
$ \rho(x)の重要な性質．任意の$ \sigmaに対し，
$ T \vdash \rho(\ulcorner \sigma \urcorner)すなわち$ \lbrack T \vdash \rho(\ulcorner \sigma \urcorner) \rbrack = \tt tのとき
$ \iff$ T \vdash \gamma_{\mathrm{diag}_T}(\ulcorner \sigma \urcorner, \ulcorner \mathtt{f} \urcorner)
$ \iff$ \lbrack T \vdash \sigma(\ulcorner \sigma \urcorner) \rbrack = \mathtt{f}すなわち$ T \nvdash \sigma(\ulcorner \sigma \urcorner)
$ \rhoは自由変数を1個しか持たないから，$ \rho(x)を対角化関数に突っ込むことができる．$ \mathrm{diag}_T(\rho)を考える．
以下の議論は実際に証明されている形とは大幅に異なる．
$ T \vdash \sigmaかつ$ T \nvdash \sigmaであることはありえないとする．もしそうならLean的には¬p ↔ p → Falseと定義されている以上，Falseが得られてしまう．
もし$ T \vdash \mathrm{diag}_T(\rho)は$ T \vdash \rho(\ulcorner \rho \urcorner)を意味するが，これは性質より$ T \nvdash \rho(\ulcorner \rho \urcorner)が帰結してしまう．よって破綻する
もし$ T \nvdash \mathrm{diag}_T(\rho)なら$ T \nvdash \rho(\ulcorner \rho \urcorner)を意味するが，これも性質（の逆をたどれば）$ T \vdash \rho(\ulcorner \rho \urcorner)が帰結してしまう．よってこれも破綻する．
したがって，$ Tは完全（任意の文$ \sigmaに対し$ T \vdash \sigmaまたは$ T \nvdash \sigmaのどちらか）であることは出来ない．
逆にもし完全だった場合，$ Tは以下の条件のどれかを満たさない．
1. $ \sf PA^-の（拡張？）理論ではない
2. $ TはDecidablePredではない．（lean4-logicのTheoryにおいてこれが何を意味するかはよくわかってない．）
3. $ Tは$ \Sigma_1健全ではない
4. $ Tは計算可能ではない
書き換え系のメモ
$ \#0, \#1で自由変数を表すとする．
「$ \rho(\#0)の$ \#0を$ \ulcorner \sigma \urcornerで書き換える」を表すのが[→ ⸢σ⸣].hom ρである．
「1変数関数$ f(x)のグラフ（$ f(x) = y）の論理式$ \gamma_f(\#0, \#1)に対して，$ \#0,\#1をそれぞれ$ \ulcorner x \urcorner, \ulcorner y \urcornerで書き換える」は[→ ⸢y⸣, ⸢x⸣].hom (graph f)
疑問 / 感想
第1不完全性定理で実質的に最後LO.FirstOrder.Arith.FirstIncompleteness.contradに用いられているタクティクがexact Std.Logic.not_iff_self hρなのはちょっと最終回っぽくて良いなと思った． $ \Sigma_1健全性に掬い取られているから？$ Tが無矛盾であるという性質は陽には要請されていない
記憶があやふやになってきて覚えていない，このタイプの議論ってあまり和書では見ないと思うが，どこかで見たんだけどどこでだったっけ？
t特に
ところでそれではこのsettingで証明可能性述語$ \mathrm{Pr}_T(x)ってどうやって構成すればいいのだろうか？