表現可能性定理についてのメモ

参考文献

記法はΣ₁完全性定理に従う．

菊池誠; "不完全性定理"

数学における証明と真理様相論理と数学基礎論

y.; "再帰的関数"

ゲーデルと20世紀の論理学第3巻(本)

新井敏康『数学基礎論』増補版

TL;DR

$ TはPeano算術の$ \sf PAの再帰的可算な拡大理論とする．

なおCraigのトリックより$ Tは再帰的理論または原始再帰的理論としても別に構わない．

再帰的可算集合

$ A \sube \N^nが再帰的可算集合である

$ \iff$ Aは$ \Sigma_1定義可能 /$ \Sigma_1集合 / 再帰的枚挙可能である．(Thm4: 表現可能性定理#64b91ee613a1580000b66370)

$ \iff$ Aは$ T上で弱表現可能．

再帰的集合

$ A \sube \N^nが再帰的集合である

$ \iff$ Aは$ \Delta_1定義可能 / $ \Delta_1集合である /$ Aは計算可能である．(Thm5: 表現可能性定理#64b91f1813a1580000b66373)

$ \iff$ Aは$ T上で表現可能．

原始再帰的集合

$ A \sube \N^nが原始再帰的集合$ \iff$ Aは$ T上で$ \Delta_1表現可能．

再帰的関数

$ fが全域的な再帰関数$ \iff$ fは$ Tで表現可能．

原始再帰的関数

$ fが原始再帰的関数$ \iff$ fは$ Tで可証再帰的．(Thm8: 表現可能性定理#64b974df13a1580000b03e5e)

その他

$ \sf PAには任意の原始再帰的関数が最初から入っていると仮定しても本質的に問題がない．(Cor10: 表現可能性定理#64b97f5613a1580000b03e8c)

Def. 集合の定義可能性

集合$ A \sube \N^nとする．

論理式$ \varphi(\vec{x})が以下を満たすとき，$ \varphiは$ Aを定義すると呼ぶ．

$ \vec{a} \in A \iff \mathcal{N} \vDash \varphi(\vec{\underline{a}})

すなわち，$ A \coloneqq \{ \vec{a} \in \N \mid \mathcal{N} \vDash \varphi(\vec{\overline{a}}) \}

$ Aを定義する論理式が存在するとき，$ Aは定義可能と呼ぶ．

算術的階層について

$ Aが$ \Delta_k,\Sigma_k,\Pi_k論理式で定義可能であるとき，

$ Aは$ \Delta_k集合，$ \Sigma_k集合，$ \Pi_k集合と呼ぶ．

または，$ Aは$ \Delta_k定義可能，$ \Sigma_k定義可能，$ \Pi_k定義可能と呼ぶ．

remark:

明らかに，$ \Sigma_k定義可能かつ$ \Pi_k定義可能な集合は，$ \Delta_k集合である．

Cor 1

$ Aが$ \varphi(\vec{x})で定義されるとき，$ \N^n \setminus Aは$ \lnot\varphi(\vec{x})によって定義される．

proof:

1. 定義可能性の定義より$ \vec{a} \notin A \iff \mathcal{N} \nvDash \varphi(\vec{\overline{a}})

2. $ \vec{a} \notin A \iff \vec{a} \in \N^n \setminus A

3. $ \mathcal{N} \nvDash \varphi(\vec{\overline{a}}) \iff \mathcal{N} \vDash \lnot\varphi(\vec{\overline{a}})

4. したがって$ \vec{a} \in \N^n \setminus A \iff \mathcal{N} \vDash \lnot\varphi(\vec{\overline{a}})

Cor 2

$ \Delta_0集合は原始再帰的集合である．

proof:

1. $ \Delta_0文は量化子を含まない文に変形出来る．

Σ₁完全性定理#64b8f7e213a1580000e20000のLem3.3より

2. $ \vec{a} \in \N^nが与えられたとき，$ \varphi(\vec{\overline{a}})は文である．

3. 1,2より，$ \varphi(\vec{x})が$ \Delta_0論理式であるとき，$ \mathcal{N} \vDash \varphi(\vec{\overline{a}})かどうかは原始再帰的に判定できる．

量化子の含まない文は原始再帰的に判定できる．

4. $ A \coloneqq \{ \vec{a} \in \N \mid \mathcal{N} \vDash \varphi(\vec{\overline{a}}) \}より，$ Aは原始再帰的集合である．

Thm 3

部分関数$ f:\N^n\to\Nが再帰的関数である $ \iff$ fのグラフ$ G_fは$ \Sigma_1集合である．

ただし，$ fのグラフ$ G_fとは$ G_f \coloneqq \{ (\vec{a},b) \in \N^{n+1} \mid f(\vec{a}) = b \}として定義される．

proof

$ \impliedby

$ n = 1とする．任意の$ nについては適当に帰納法を回せば良い．

1. $ \varphi(x,y,z)を$ \Delta_0論理式とし，$ G_f \coloneqq \{ (x,y) \in \N^2 \mid \mathcal{N} \vDash \exists_z.\varphi(\overline{x},\overline{y},z) \}とする．

すなわち，$ G_fは$ \Sigma_1集合である．

2. $ a,b,c \in \Nが与えられたとき，$ \mathcal{N} \vDash \varphi(\overline{a},\overline{b},\overline{c})は有限回で計算できる．

$ \Delta_0論理式は有限量化しか含まないので．

3. $ fが部分関数で$ \exists_z.\varphi(x,y,z)

$ \implies

$ n = 1とする．任意の$ nについては適当に帰納法を回せば良い．

$ fが定数関数，後者関数，射影関数

自明．

$ fが関数の合成で作られる関数とする．

すなわち，

$ g_i:\N \to \N, h:\N^m \to \Nとし，

$ \mathrm{comp}_{g_1,\dots,g_m,h}(x) = h(g_1(x),\dots,g_m(x))である．

1. IHより，$ g_i,hのグラフは$ \Sigma_1集合である．

2. $ \Sigma_1論理式$ \varphi(x,y) \equiv \exists_{x_1,\dots,x_m}.\left\lbrack x_1 = \overline{g_1(x)} \land \dots \land x_m = \overline{g_m(x)} \land y = \overline{h(x_1,\dots,x_m)} \right\rbrackとする．

ここで$ g_i,hは関数$ g_i,hを表す演算子とする．

3. $ \varphi(x,y)は$ G_fを定義している．よって，$ G_fは$ \Sigma_1集合である．

$ fが原始再帰で作られる関数

すなわち，

$ g:\N, h:\N^2\to\N

$ \mathrm{prec}_{g,h}(0) = g

$ \mathrm{prec}_{g,h}(\mathrm{s}(x)) = h(x,\mathrm{prec}_{g,h}(x))

1. IHより，$ g,hのグラフは$ \Sigma_1集合である．

2. $ \Sigma_1論理式$ \varphi(x,y) \equiv \exists_e.\left\lbrack \beta(e,\overline{0}) = \overline{g} \land \forall_{u<x}.\exists_{v<x}.\left\lbrack v = \beta(e,u+\overline{1}) \land v = \overline{h(u,\beta(e,u))} \right\rbrack \land \beta(e,x) = y \right\rbrack

$ g,hは関数$ g,hを表す演算子とする．

$ \betaはThm3.1で存在が示されているデコード関数を表す演算子とする．

すなわち$ \beta(x,y) = zは$ \Delta_0論理式である．

次のような数列$ a_0,\dots,a_xのエンコード$ eが存在することを確認している．

$ a_0 = g

$ \beta(e,\overline{0}) = \overline{g}でチェック

$ a_1 = h(x, a_0), a_2 = h(x,a_1),\dots, a_x = h(x,a_{x-1})

$ \forall_{u<x}.\exists_{v<x}.\left\lbrack v = \beta(z,u+\overline{1}) \land v = h(u,\beta(z,u)) \right\rbrackでチェック

$ a_x = y

$ \beta(e,x) = yをチェック．

remark:

$ f(0),\dots,f(x-1)を計算しなければ$ f(x)の値は計算出来ないことに注意．

3. $ \varphiは$ G_fを定義している．$ G_fは$ \Sigma_1集合である．

$ fが最小化で作られる関数

すなわち

$ g:\N^2 \to \N

$ f(x) \simeq \mu_y.\lbrack g(x,y) = 0 \rbrackとする．

$ g(x,y) = 0となる$ yが存在すれば$ f(x) = y，しないなら$ f(x)は未定義．

1. IHより$ gのグラフは$ \Sigma_1集合とする．

2. $ \Sigma_1論理式$ \varphi(x,y) \equiv \exists_e.\left\lbrack \beta(e,x) = \overline{0} \land \forall_{u\leq x}.\exists_{v}.\left\lbrack v = \beta(e,u) \land v = \overline{g(x,u)}\right\rbrack \land \forall_{u<x}.\left\lbrack\beta(e,u) \neq \overline{0} \right\rbrack \right\rbrack

$ g,hは関数$ g,hを表す演算子とする．

$ \betaはThm3.1で存在が示されているデコード関数を表す演算子とする．

次のような数列$ a_0,\dots,a_xのエンコード$ eが存在することを確認している

$ a_x = 0

$ \beta(e,x) = \overline{0}でチェック

$ a_0 = g(x,0),\dots,a_x = g(x,x)

$ \forall_{u\leq x}.\exists_{v}.\left\lbrack v = \beta(e,u) \land v = \overline{g(x,u)}\right\rbrackでチェック

$ a_0,\dots,a_{x-1}が全て$ 0ではないこと

$ \forall_{u<x}.\left\lbrack\beta(e,u) \neq \overline{0} \right\rbrack

remark:

$ g(x,0),\dots,g(x,y)を計算を計算しなければ$ \mu_y.\lbrack g(x,y) = 0 \rbrackの値は計算出来ないことに注意．

3. $ \varphiは$ G_fを定義している．$ G_fは$ \Sigma_1集合である．

Thm 3.1: デコード関数

デコード関数と呼ばれる，以下を満たす原始再帰的関数$ \beta(x,y)が存在する．

1. 有限列$ a_0,\dots,a_{k} \in \Nとする．任意の$ i \leq kに対し$ \beta(e,i) = a_{i} となる$ e \in \Nが存在する．

2. $ \beta(x,y)のグラフ$ G_\betaは$ \Delta_0集合である．

proof:

y.; "再帰的関数"の補題2.2.参照．ただし$ G_\betaが$ \Delta_0かどうかは自分で埋めなければならない

http://iso.2022.jp/math/undecidable-problems/files/recursive-function.pdf

ゲーデルと20世紀の論理学第3巻(本)のI章参照．

Cor 10より，そもそもこの$ \betaが織り込み済みとして自明な事実として扱っても良い．

表現可能性定理#64b97f5613a1580000b03e8c

remark:

歴史的な経緯でこのような関数はGödelのβ関数とも呼ばれる

$ eを，数列$ a_0,\dots,a_kの（関数$ \betaに対する）エンコードと呼ぶ

Thm 4

$ A \sube \N^nが再帰的可算集合である$ \iff$ Aが$ \Sigma_1集合である．

remark:

再帰的可算集合は再帰的枚挙可能な集合であるとも言われるので，$ \Sigma_1定義可能性は再帰的枚挙可能性を表しているとも言える．

proof:

$ n = 1とする．任意の$ nについては適当に帰納法を回せば良い．

#TODO

Thm 5

$ A \sube \N^nが再帰的集合である$ \iff$ Aが$ \Delta_1集合である．

remark:

再帰的集合は計算可能な集合であるとも言われるので，$ \Delta_1定義可能性は計算可能性を表しているとも言える．

proof:

1. $ Aが再帰的集合なら$ A,\N^n\setminus Aが再帰的可算集合．

関数と集合の再帰性についてのメモ#64b65bdc13a1580000b71527

2. Thm4より$ A,\N^n \setminus Aは$ \Sigma_1集合である．

3. 2とCor1より，$ \N^n \setminus (\N^n \setminus A)は$ \Pi_1論理式$ \lnot\varphi(\vec{x})で定義可能．

4. $ \N^n \setminus (\N^n \setminus A) = A．

5. $ Aは$ \Pi_1集合である．

6. 2,5より$ Aは$ \Delta_1集合である．

Cor 6

$ f: \N \to \Nが全域的な再帰的関数$ \iff$ G_fは$ \Delta_1集合．

proof

$ f:\N\to\Nが全域的な再帰的関数$ \iff$ G_fが再帰的集合

関数と集合の再帰性についてのメモ#64b6a11813a1580000b715b1

上の事実とThm 5より．

Remark:

計算的枚挙可能性と$ \Sigma_1が同値であること(Thm4)

計算可能性と$ \Delta_1が同値であること(Thm5)

$ Tは$ \Sigma_1完全であること(Σ₁完全性定理)

以上より計算可能性は（少なくとも計算的枚挙可能性）は$ T上でも議論可能であることが以上の議論よりわかる．

今までは実際の算術上で構成していたことに注意

Def: 可証再帰性

$ f:\N \to \Nは部分関数とする．

以下を満たす$ \Sigma_1論理式$ \varphi(\vec{x},y)が存在するとき，$ fは$ T上で可証再帰的であるという．

1. $ \varphi(x,y)は（$ \mathcal{N}上）で$ G_fを定義する．

2. $ T \vdash \forall_{\vec{x}}.\exists!_y.\varphi(x,y)

remark:

一意存在量化$ \exists!_y.\varphi(x,y) \equiv \exists_y.\varphi(x,y) \land \forall_{y,y'}.\lbrack \varphi(x,y) \land \varphi(x,y') \to y=y' \rbrackのことである．

すなわち

2'. $ T \vdash \forall_{\vec{x}}.\left\lbrack \exists_y.\varphi(x,y) \land \forall_{y,y'}.\left\lbrack \varphi(x,y) \land \varphi(x,y') \to y=y' \right\rbrack \right\rbrack

remark

$ T上で全域的な再帰的関数を扱うために導入される概念である．

逆に言えば，実際に全域的な再帰的関数であっても，$ T上では全域性が扱えるとは限らない．

Prop 7

再帰的だが，$ \sf PA上で可証再帰的ではない全域的な再帰的関数が存在する．

remark

ヒドラゲームやGoodstein数列のあるステップにおける状態を表す関数は再帰的関数として記述出来る．

にも関わらず，以下の命題は$ \sf PAで証明できない．

ヒドラゲームでヘラクレスは常に勝てること

Goodstein数列が0に収束する

Goodsteinの定理

これらはKreiselの定理などを用いて証明される．