Δ₀関係
定義: 自然数
自然数$ \Nと自然数の関数についてはここで定義されるものとする. 定義: 算術の関数
次の$ \Nについての関数は算術の関数と呼ぶ.
以下の基本的な関数は算術の関数である.
$ \mathsf{zero}^n:\N^n\to\N($ nは任意の自然数)
$ \mathsf{zero}^n(\vec{x}) \coloneqq \mathtt{0}
$ \mathsf{succ}: \N\to\N
$ \mathsf{succ}(\mathtt{n}) \coloneqq \mathtt{s(n)}
$ \mathsf{add}: \N^2 \to \N
$ \mathsf{add}(\mathtt{x,0}) \coloneqq \mathtt{x}
$ \mathsf{add}(\mathtt{x,s(n)}) \coloneqq \mathsf{succ}(\mathsf{add}(\mathtt{x}, \mathtt{n}))
以下$ \mathtt{x + y} \coloneqq \mathsf{add}(\mathtt{x,y})
$ \mathtt{mul}:\N^2\to\N
$ \mathsf{mul}(\mathtt{x,0}) \coloneqq \mathtt{0}
$ \mathsf{mul}(\mathtt{x,s(n)}) \coloneqq \mathsf{add}(\mathtt{x},\mathsf{add}(\mathtt{x}, \mathtt{n}))
以下$ \mathtt{x \times y} \coloneqq \mathsf{mul}(\mathtt{x,y})
合成
$ f:\N^n\to\Nと$ g:\:\N \to \Nが算術の関数であり,次のように定義される関数の合成$ (f;g)も算術の関数である.
$ f(\mathtt{x}_1,\dots,\mathtt{x}_i,\dots,\mathtt{x}_n)であるとき,$ (f;g)(\mathtt{x}_1,\dots,g(\mathtt{x}_i),\dots,\mathtt{x}_n)
定義: $ \Delta_0関係
次の$ \Nについての関係は$ \Delta_0関係と呼ばれる.
1. 等号
$ f,gが算術の関数であるとする.
次の関係$ f(\vec{x}) = g(\vec{x})は$ \Delta_0関係である.
$ f(\vec{x}) = g(\vec{x})が成立$ \iff$ f(\vec{\mathtt{x}})と$ g(\vec{\mathtt{x}})は等しい.
2. 論理演算
$ R,Sが$ \Delta_0関係とすると,$ \lnot R,(R \land S), (R \lor S)は$ \Delta_0関係である.
$ \lnot R(\vec{\mathtt{x}})が成立$ \iff$ R(\vec{\mathtt{x}})が成立しない
$ (R \land S)(\vec{\mathtt{x}})が成立$ \iff$ R(\vec{\mathtt{x}})と$ S(\vec{\mathtt{x}})のどちらも成立
$ (R \lor S)(\vec{\mathtt{x}})が成立$ \iff$ R(\vec{\mathtt{x}})と$ S(\vec{\mathtt{x}})の少なくともどちらか一方が成立
以下の略記を定める
$ R \to S := \lnot R \lor S
$ fが$ n項の算術の関数であり,$ Rは$ n+1項の$ \Delta_0関係とする.
次の$ \forall_{\mathtt{y} < f(\vec{\mathtt{x}})} R(\vec{\mathtt{x}},\mathtt{y})及び$ \exists_{\mathtt{y} < f(\vec{\mathtt{x}})} R(\vec{\mathtt{x}},\mathtt{y})として表される$ n項関係は$ \Delta_0関係である.
$ \forall_{\mathtt{y} < f(\vec{\mathtt{x}})}.R(\vec{\mathtt{x}},\mathtt{y})が成立$ \iff$ f(\vec{\mathtt{x}})より小さな全ての$ \mathtt{i}に対して$ R(\vec{x},\mathtt{i})が成立
$ \exists_{\mathtt{y} < f(\vec{\mathtt{x}})}.R(\vec{\mathtt{x}},\mathtt{y})が成立$ \iff$ f(\vec{\mathtt{x}})より小さなある$ \mathtt{i}で$ R(\vec{x},\mathtt{i})が成立
ただし,$ \mathtt{y}は$ \vec{\mathtt{x}}の中に出現しない.
実際には$ <を$ \leqに拡張したものも定めておくと便利なので定める.
$ \forall_{\mathtt{y} \leq f(\vec{\mathtt{x}})}.R(\vec{\mathtt{x}},\mathtt{y}) \coloneqq \forall_{\mathtt{y} \leq f(\vec{\mathtt{x}})}.R(\vec{\mathtt{x}},\mathtt{y}) \land R(\vec{\mathtt{x}},f(\vec{\mathtt{x}}))
$ \exists_{\mathtt{y} \leq f(\vec{\mathtt{x}})}.R(\vec{\mathtt{x}},\mathtt{y}) \coloneqq \exists_{\mathtt{y} < f(\vec{\mathtt{x}})}.R(\vec{\mathtt{x}},\mathtt{y}) \lor R(\vec{\mathtt{x}},f(\vec{\mathtt{x}}))
定義: Cantorの対関数
一般の自然数$ \mathcal{N}について定義する.
$ \frac{(x+y)(x+y-1)}{2}+y
この関数は全射であり,2つの自然数を1つの自然数$ \lang x,y \rangに一意に割り当てる.
系
3項関係$ \lang \mathtt{x,y} \rang = \mathtt{z}は$ \Delta_0関係である.
証明: $ \tt 2 \times z = (x + y)(x + y - 1) + 2 \times y
TODO: 減算は存在しないので疑わしい.
系
2項関係$ \mathsf{div}(\mathtt{x,y}):「$ \mathtt{x}は$ \mathtt{y}を割り切る」は$ \Delta_0関係である.
証明:$ \exists_\mathtt{z \leq y}.\mathtt{(y = x \times z)}
2項関係$ \mathsf{power}_\mathtt{p}(\mathtt{x}): 「$ \mathtt{x}は素数$ \mathtt{p}の累乗である」は$ \Delta_0関係である.
証明:$ \forall_\mathtt{z \leq x}.((\mathsf{div}(\mathtt{z,x}) \land \mathtt{z} \neq 1)\to \mathsf{div}(\mathtt{p,z}))
一般の自然数$ xと素数$ pについて,$ xが$ pの冪乗である$ \iff$ xの1以外の約数が全て$ pで割り切れる
3項関係$ \mathtt{y} = \mathsf{lastpow}_\mathtt{p}(\mathtt{x}):「$ \mathtt{x}より大きな素数$ \mathtt{p}の累乗のうち最小のものと$ \mathtt{y}が等しい」は$ \Delta_0関係である.
証明:$ \mathtt{x} < \mathtt{y} \land \mathsf{power}_\mathtt{p}(\mathtt{y}) \land \lnot \exists_\mathtt{z \leq y}.(\mathtt{x} \leq \mathtt{z} \land \mathsf{power}_\mathtt{p}(\mathtt{x}) )
例
$ \mathsf{lastpow}_\mathtt{2}(\mathtt{17}) = \mathtt{32}:$ \mathtt{17}より大きい$ \mathtt{2}の累乗は$ \mathtt{32}である.
定義: 連結
一般の自然数$ \mathcal{N}について定義する.
$ pは素数とする.10進数の自然数$ xを$ p進数の数として書いたときに得られる文字列を$ x_pと書くとする.
例
$ 14_2 = \mathsf{1110}
$ 7_2 = \mathsf{110}
10進数の自然数$ x,yに対して文字列$ x_p,y_pが定まる.
これを連結した文字列$ x_py_pを$ p進数の数として解釈することで得られる10進数の自然数を「$ xと$ yの$ p進数での連結」と呼んで,$ x *_{p} yと表記する.
例
$ 14 *_2 7 = 118
$ 14と$ 7の2進数での文字列は↑で求めたように$ \mathsf{1110}と$ \mathsf{110}なので,連結すると$ \mathsf{1110110}.
$ \mathsf{1110110}は2進数の数として解釈すると$ 118.
連結は左結合であるとする.すなわち,$ x *_p y *_p z = (x *_p y) *_p zである.
以上の定義が形式的に定義された自然数$ \Nでも用いることが出来るとする.
系
4項関係$ \mathtt{x} *_\mathtt{p} \mathtt{y} = \mathtt{z}は$ \Delta_0関係である.
証明: $ \mathtt{x} \times \mathsf{lastpow}_\mathtt{p}(\mathtt{y}) + \mathtt{y} = \mathtt{z}
3項関係$ \mathsf{startsWith}_\mathtt{p}(\mathtt{x,y}): 「文字列$ \mathtt{y}_\mathtt{p}は文字列$ \mathtt{x}_\mathtt{p}で始まる」は$ \Delta_0関係である.
証明:$ \tt x = y \lor (x \neq y \land \exists_{z < y}.(x *_p z = y))
例: $ \tt \mathsf{startsWith}_2(14,118)
3項関係$ \mathsf{endsWith}_\mathtt{p}(\mathtt{x,y}): 「文字列$ \mathtt{y}_\mathtt{p}は文字列$ \mathtt{x}_\mathtt{p}で終わる」は$ \Delta_0関係である.
証明:$ \tt x = y \lor (x \neq y \land \exists_{z < y}.(z *_p x = y))
例: $ \tt \mathsf{endsWith}_2(7,118)
3項関係$ \mathsf{contains}_\mathtt{p}(\mathtt{x,y}): 「文字列$ \mathtt{y}_\mathtt{p}は文字列$ \mathtt{x}_\mathtt{p}を含む」は$ \Delta_0関係である.
証明:$ \tt \exists_{z < y}.(\mathsf{startsWith}(z,y) \land \mathsf{endsWith}(x,z))
例: $ \tt \mathsf{contains}_2(5,118)
$ \mathsf{1110110}は$ \mathsf{101}という文字列を含む.$ \mathsf{101}は2進数として解釈すると5である.
定義: フレーム
一般の自然数$ \mathcal{N}について定義する.
$ p>2は素数であるとする.
自然数$ xの文字列表記$ x_pが$ \mathsf{21\cdots12}であるとき,$ xは($ p進数での) フレームであると言う.
例: $ 68_3は$ \mathsf{2112}なので,3進数でフレームである.
$ xの文字列表記$ x_pが,自然数$ yの文字列表記$ y_pに現れる最も長いフレームと一致するとき,$ xは$ yの ($ p進数での)最大フレームと言う.
例
$ y_3が文字列$ \sf 11211112021120であったとき,フレーム$ \sf 211112と$ \sf 2112が存在する.
$ x_3が文字列$ \sf 211112であるなら,$ xは$ yの最大フレームである.
以上の定義が形式的に定義された自然数$ \Nでも用いることが出来るとする.
系
2項関係$ \tt \mathsf{1seq}_p(x): 「文字列$ \tt x_pは$ \mathsf{1\cdots1}である」は$ \Delta_0関係である.
証明:$ \tt x \neq 0 \land \forall_{y \leq x}.(\mathsf{contains}_p(y,x) \to \mathsf{contains}_p(1,y))
2項関係$ \tt \mathsf{frame}_p(x): 「$ \tt xは$ \tt p進数でフレームである」は$ \Delta_0関係である.
証明:$ \tt \exists_{z < x}.(x = 2 *_p z *_p 2 \land \mathsf{1seq}_p(z))
3項関係$ \tt x = \mathsf{maxframe}_p(y): 「$ \tt xは$ \tt yの$ \tt p進数での最大フレームである」は$ \Delta_0関係である.
証明:$ \tt \mathsf{frame}_p(x) \land \lnot \exists_{z \leq y}(\mathsf{frame}(z) \land x < z)
定義: 集合のコード
一般の自然数$ \mathcal{N}について定義する.
$ p>2は素数とする.
自然数の有限集合$ A = \{a_0,\dots,a_{n-1}\}とする.
$ Aのどの$ a_iにも含まれない$ p進数のフレームを$ f_pとする.
注意$ f_pは一意ではない.
次の連結された文字列を$ p進数の数として解釈した10進数の数は$ Aの($ p進数での)コードと呼ばれる.
$ f_p *_p {a_0}_p *_p f_p *_p {a_1}_p *_p f_p \cdots f_p *_p {a_{n-1}}_p *_p f_p
非常に煩雑なので添字$ _pと連結記号$ *_pを省略して見やすくすると以下の文字列である.
$ f a_0 f a_1 f \cdots f a_{n-1} f
注意
$ f_pが一意ではないことから,$ Aのコードも一意には定まらない.
命題
任意の自然数の有限列に対して,コードを構成することが出来る.
$ f_pは$ Aのコードの$ p進数の最大フレームと一致する.
以上の定義が形式的に定義された自然数$ \Nでも用いることが出来るとする.
系
$ n+2項関係$ \mathtt{x} = \mathsf{seqn}_\mathtt{p}(\mathtt{a}_0,\dots,\mathtt{a}_{n-1}): 「$ \tt xは自然数の有限集合$ (\mathtt{a}_1,\mathtt{a}_2,\dots,\mathtt{a}_n)の$ \mathtt p進数でのコードである」は$ \Delta_0関係である.
ある自然数の有限集合$ \mathtt{A} = \{\mathtt{a}_0,\dots,\mathtt{a}_{n-1}\}の$ \tt p進数でのコードを$ \tt yとする.
2項関係$ \tt x \in y:「$ \tt xは$ \tt Aの要素である」あるいは「$ \tt xは$ \mathtt{a}_1,\dots,\mathtt{a}_nのいずれかである.」は$ \Delta_0関係である.
証明:$ \tt \exists_{z<y}.(z = \mathsf{maxframe}_p(y) \land part_p(z *_P x *_p z))
定義: 有限列
任意の自然数の有限集合$ (a_0,a_1,\dots,a_{n-1})は,次の有限集合として表現することで有限列$ (a_0,a_1,\dots,a_{n-1})として扱うことが出来る.
$ \{ \lang 0,a_0 \rang,\lang 1,a_1 \rang,\dots,\lang n,a_{n-1} \rang \}
有限列$ (a_0,a_1,\dots,a_{n-1})のコードは,$ \{ \lang 0,a_0 \rang,\lang 1,a_1 \rang,\dots,\lang n,a_{n-1} \rang \}のコードとする.
定義: Gödelの$ \beta関数
一般の自然数$ \mathcal{N}について定義する.
任意の自然数の有限列$ ( a_0,\dots,a_{n-1} )について,次を満たす自然数$ wが存在するなら,2項関数$ \betaは$ \beta関数(Gödelのβ関数)と呼ぶ. $ \beta(w,0) = a_0,\beta(w,1) = a_1,\dots,\beta(w,n-1) = a_{n-1}
定理
証明
$ \tt \beta(w,x) = \mu_\mathtt{y < w}.\lang x,y \rang \in wと定義する.
ただし,$ \tt wは有限列の$ ( \mathtt{a}_0,\dots,\mathtt{a}_{n-1} )のコードとする.
このとき例えば$ \tt x = 0について
$ \tt \lang 0,y \rang \in w$ \iff$ \tt \lang 0,y \rangは$ \{ \lang \mathtt{0},\mathtt{a}_0 \rang,\lang \mathtt{1},\mathtt{a}_1 \rang,\dots,\lang \mathtt{n},\mathtt{a}_{n-1} \rang \}の要素である
もちろんそれは$ \lang \mathtt{0},\mathtt{a}_0 \rangに他ならない.
よって$ \mathtt{y} = \mathtt{a}_0として関数の出力とする.
このとき,$ \tt{x}が有限列の範囲外すなわち$ n以上であるなら有界最小化の定義にしたがって$ \mathtt{w}が返ってくる. すなわち,$ \beta(\tt{w},\tt{n}) = \tt{w}である.
定理
$ \betaが$ \beta関数であるとき,3項関係$ \beta(\mathtt{w,x}) = \mathtt{y}は$ \Delta_0関係である.
証明
$ \tt (\lang x,y \rang \in w \land \forall_{z < y}.\lang x,z\rang \notin w) \lor ((\lnot \exists_{z \leq w}. \lang x,z \rang \in w) \land y = w)
左は$ \tt \lang x,y \rangが$ \tt w(すなわち有限列$ \tt A)に存在すればにだた一つ存在することを表す
右は$ \tt \lang x,y\rangが$ \tt wに存在しないなら$ \tt yは$ \tt wであることを表す
すなわち,範囲外であることを表す
メモ
フレームを使って$ \tt x \in yが$ \Delta_0関係であることを証明する方法はQuineによる.
Quineのフレームを使わずに$ \tt x \in yが$ \Delta_0関係であることを証明することが出来る.
Gödelのβ関数という名称が一般的なのかはわからないが,とりえあず最初に現れたとされるGödelに由来する. メモ2
↓はかなり疑わしい.
算術的階層の$ \Delta_0論理式で定義可能な関係は$ \Delta_0関係という. 算術において有界量化だけが行われる論理式で表現可能な論理式は$ \Delta_0論理式という.