add(FirstOrder): Church's Undecidability Theorem

[SnO2WMaN]

現行の形式化ではいくつかの事実が弱く，示せないような気がする．

[SnO2WMaN]

明らかだとは思うがどうやればいいのかはわからない．

[SnO2WMaN]

いくつかコメントをつけておいた．表現可能性や対角線補題に関しては大掛かりな変更がいるような気もするので早急に取り掛かるかは任せる．

[iehality]

ところで，強い表現定理や対角化は使用しなくても証明できると思う：

$\lbrace \sigma | T \vdash \sigma \rbrace$ が computable であると仮定する．よって $D := \lbrace \sigma(x) | T \nvdash \sigma(\ulcorner \sigma \urcorner) \rbrace$ とすると $D$ は computable．とくに r.e. なので，半表現定理よりある $\delta(x)$ について $\forall n, [n \in D \iff T \vdash \delta(\overline n)]$. よって $T \nvdash \delta(\ulcorner \delta \urcorner) \iff T \vdash \delta(\ulcorner \delta \urcorner)$ ↯

上の結果は $\mathsf{R_0}$ より強い理論についての主張だが， $\lbrace \sigma | \mathsf{PA^-} \vdash \sigma \rbrace$ が computable であることは $\lbrace \sigma | \emptyset \vdash \sigma \rbrace$ が computable であることから従うので， $T = \emptyset$ の結果は $T = \mathsf{PA^-}$ のときの上の結果から従う．

[SnO2WMaN]

勘違いでなければ，その仮定から $D$ が computableであることは少なくとも形式化においてそれほど自明なことではないし同じ程度に面倒な気もする． $D$ ってΣ₁-Predicateなのだろうか？Π₁ではなく？

[SnO2WMaN]

ComputablePred fun n ↦ ∃ σ, n = ⌜σ⌝ ∧ ∅ ⊢!. σ から ComputablePred fun n ↦ ∃ σ, n = ⌜σ⌝ ∧ 𝐏𝐀⁻ ⊢!. σ．
firstorder_provable_of_finite_provable で ∅ ⊢!. に落としてから 𝚫₁-predicateで議論すればいいような気がする．

[SnO2WMaN]

（強い）表現定理から従う．

[SnO2WMaN]

いくつかは完全に自分の勘違いだったが，しかし結局のところ少なくとも私が思うに，普通の証明でこれを形式化するのは以下の事実が必要だと思われる．

1. 対角化補題が 𝐑₀ または 𝐐 または 𝐏𝐀⁻ の弱い体系でも成立する．
2. 強い表現定理．
3. 計算可能な述語は𝚫₁-述語と同値．

あるいは，以下の証明もある．
Gödel数を一列に並べてLindenbaum補題のように拡大理論を作っていって，その拡大列の極大理論がTとなるように作っていけば，拡大理論に入るかどうかは計算可能であることから T が再帰的になり，かつ完全になる．これはG1と矛盾．
この論法で示すなら，1.と2.は不要で，3.と「Tの定理のGödel数が再帰的 → TはΔ₁」という事実が成り立てば良さそうに思える．

どちらにせよ3.（と細々とした関係がΔ₁であるという事実）はほぼ必須だと思う．他もあればうれしいが，どれだけ難しいことなのかは全く想像はつかない．

[iehality]

勘違いでなければ，その仮定から D が computableであることは少なくとも形式化においてそれほど自明なことではないし同じ程度に面倒な気もする． D ってΣ₁-Predicateなのだろうか？Π₁ではなく？

一般に次が言える：

1. 集合 $A$ が computable ならば $A^c$ も computable.

• ComputablePred.not

2. 集合 $A$ , 関数 $f$ が computable ならば $\lbrace x \mid f(x) \in A \rbrace$ も computable

• mathlib には証明はなさそうだが，そんなに難しくないと思う．

$P := \lbrace \sigma \mid T \vdash \sigma \rbrace$, $f(\sigma) := \sigma(\ulcorner \sigma \urcorner)$ とする． $P$ が computable と仮定するならば，1. より $P^c$ は computable. $f$ は computable なので（これを示すのが技術的に若干面倒かもしれない），2. より $\lbrace \sigma \mid f(\sigma) \in P^c \rbrace = D$ が computable であることがわかる． （実際には論理式の集合を考える代わりにコードした自然数の集合だけを考えるので， $f(n)$ は論理式のコードでない $n$ については $0$ を返すとか，そういった処理が必要になる．いずれにしろ computable ではある）．

[iehality]

3. 計算可能な述語は𝚫₁-述語と同値．

これは「 $\Delta_1$ 述語」の定義が理論に依存することによる問題がある．標準モデル上で計算可能な述語であるならば，それを表現する $\Sigma_1$, $\Pi_1$ 述語 $\varphi(x), \psi(x)$ が存在するが， $\forall x, [\varphi(x) \leftrightarrow \psi(x)]$ が理論で証明できるかはわからない（実際，Theory.Δ₁ は $\mathsf I \Sigma_1$ で同値性が証明できることと定義している（つまり理論の特徴関数が原始再帰的であることを本質的には要求している））．

[iehality]

最終的な主張の形について，Primcodable (Sentence ℒₒᵣ) が示せたならば，主張が ¬ComputablePred {σ | ∅ ⊢!. σ} となってわかりやすくなるので嬉しい．またコーディング周りの煩わしさからも開放されるが，示すのはとてもむずかしいと思うので，示さなくてもいいとは思う．

[SnO2WMaN]

いくつかの問題は切り出してIssueにメモとして書いておくと良いと思う．最終的にどのレベルでうまくまとめるかは自分には判断が難しい．

[SnO2WMaN]

とりあえず

2. 集合 $A$ , 関数 $f$ が computable ならば $\lbrace x \mid f(x) \in A \rbrace$ も computable

は示した．それ移行の議論は煩雑なので一旦省略．