SnO₂WMaN
SnO₂WMaN
勘違いでなければ，~~その仮定から $D$ が computableであることは少なくとも形式化においてそれほど自明なことではないし同じ程度に面倒な気もする．~~ $D$ ってΣ₁-Predicateなのだろうか？Π₁ではなく？
いくつかは完全に自分の勘違いだったが，しかし結局のところ少なくとも私が思うに，普通の証明でこれを形式化するのは以下の事実が必要だと思われる． 1. 対角化補題が `𝐑₀` または `𝐐` または `𝐏𝐀⁻` の弱い体系でも成立する． 2. 強い表現定理． 3. 計算可能な述語は`𝚫₁`-述語と同値． あるいは，以下の証明もある． Gödel数を一列に並べてLindenbaum補題のように拡大理論を作っていって，その拡大列の極大理論が`T`となるように作っていけば，拡大理論に入るかどうかは計算可能であることから `T` が再帰的になり，かつ完全になる．これはG1と矛盾． この論法で示すなら，1.と2.は不要で，3.と「`T`の定理のGödel数が再帰的 → `T`は`Δ₁`」という事実が成り立てば良さそうに思える． どちらにせよ3.（と細々とした関係が`Δ₁`であるという事実）はほぼ必須だと思う．他もあればうれしいが，どれだけ難しいことなのかは全く想像はつかない．
いくつかの問題は切り出してIssueにメモとして書いておくと良いと思う．最終的にどのレベルでうまくまとめるかは自分には判断が難しい．
とりあえず > 2. 集合 $A$ , 関数 $f$ が computable ならば $\lbrace x \mid f(x) \in A \rbrace$ も computable は示した．それ移行の議論は煩雑なので一旦省略．
Sorry for lating to reply for reviewing. I'll fix
I can't spare time to fix this issue so I closed this PR.