IΣ₀の計算可能な超準モデルは存在しない
定理
証明の概要
$ Mが可算で$ +^Mや$ \cdot^Mが計算可能ならその超準数を使って分離集合の特性関数を計算できる Proof.
ある$ \Sigma_0論理式$ \phi_1, \phi_2が存在して以下を満たす $ n \in A_1 \iff \N \models (\exists s)\phi_1(\overline n, s)
$ n \in A_2 \iff \N \models (\exists s)\phi_2(\overline n, s)
$ A_1, A_2を分離するような集合$ Bを定義する
$ A_1, A_2は非交叉であるから以下が成り立つ $ \N \models (\forall x, s_1, s_2)\lnot[\phi_1(x, s_1) \land \phi_2(x, s_2)]
よって任意の$ k \in \N について
$ M \models (\forall x, s_1, s_2 \le k)\lnot[\phi_1(x, s_1) \land \phi_2(x, s_2)]
$ \Sigma_0 論理式$ \psi(z) := (\forall x, s_1, s_2 \le z)\lnot[\phi_1(x, s_1) \land \phi_2(x, s_2)] は正規切断$ \N^Mの上で成り立つのでoverspillより$ Mの超準数$ a \in M\backslash \N^Mが存在して $ M \models (\forall x, s_1, s_2 \le a)\lnot[\phi_1(x, s_1) \land \phi_2(x, s_2)]
$ Bを以下のように定義する
$ B := \{n \in \N | M \models (\exists s \le a)\phi_1(\overline n, s)\}
$ B \upharpoonright nを$ c_n := \prod_{m \in B\upharpoonright n} p_mにコードする
$ p_mは$ m番目の素数
$ m \in B \upharpoonright n \iff p_m | c_n
すなわち任意の$ n \in \N^Mについて
$ M \models \theta(a, n)
$ \theta(a, z) := (\exists c \le a)[(\forall x < z)[(\exists s \le a)\phi_1(x, s) \leftrightarrow p_x | c] \land (\forall x \le c)(\exists w \le a)[2^x = w]]
$ yは$ x番目の素数で割り切れること$ \pi(x, y) \equiv p_x|yは$ \Sigma_0定義可能
?
$ \thetaは$ \Sigma_0論理式なのでoverspillより超準数$ b \in M\backslash \N^Mが存在して$ M \models \theta(a, b) よって$ c \in Mが存在して任意の$ n \in \Nについて
$ M \models (\exists s \le a)\phi_1(\overline n, s) \leftrightarrow p_{\overline n} | c
$ n \in B \iff M \models p_{\overline n}|c
$ 2^c \in M
剰余定理より任意の$ n \in \Nについて以下を満たす$ s, r \in M, $ s >^M rを探索する関数は計算可能 $ M \models c = \underbrace{s + ... + s}_{p_{\overline n}} + r
$ r = 0^Mのとき$ M \models p_{\overline n}|cより$ n \in B
$ r \ne 0^Mのとき$ M \models \lnot p_{\overline n}|cより$ n \notin B
剰余定理より任意の$ n \in \Nについて以下を満たす$ s, r \in M, $ s >^M rを探索する関数は計算可能 $ M \models 2^c = \underbrace{s \cdot ... \cdot s}_{p_{\overline n}} \cdot r
$ r = 1^Mのとき$ M \models p_{\overline n}|cより$ n \in B
$ r \ne 1^Mのとき$ M \models \lnot p_{\overline n}|cより$ n \notin B