算術化のメモ
Lem
次の関数たちは定義より原始再帰的関数である.
列のエンコード$ \lang x_0,x_1,\dots,x_{n-1} \rang
def
$ n番目の素数を$ p_n(ただし$ p_0 = 2 )とする.
$ \lang x_0,\dots,x_{n-1} \rang = \prod_{i < n} p_i^{1 + x_0}
ただし$ \lang \rang = 0とする.
列のデコード$ (e)_i
$ (\lang x_0,\dots,x_{n-1} \rang)_i = x_i($ 0 \leq i \leq n-1)
def
$ xを割り切る最大の$ p_iの冪を返す$ \mathrm{exp}(x,i) = \max_y\{ y \leq x \mid p^y_i | x \}と定める.
$ (e)_i = \mathrm{exp}(e,i) \mathop{\dot{-}} 1
列の長さ関数$ \mathrm{len}(x)(ただし引数は列のエンコードとする)
$ \mathrm{len}(\lang \rang) = 0
$ \mathrm{len}(\lang x_0,\dots,x_{n-1} \rang) = n
def
$ \mathrm{len}(x) = \min_i \{ i \leq x \mid \mathrm{exp}(x,y) = 0 \}
列の連結関数$ \cdot \frown \cdot(ただし引数は列のエンコード)
$ \lang x_0,\dots,x_{n-1} \rang \frown \lang y_0,\dots,y_{m-1} \rang = \lang x_0,\dots,x_{n-1}, y_1,\dots,y_{m-1} \rang
def
$ x \frown y = x \times \prod_{i < \mathrm{len}(y)} p^{1 + (y)_i}_{\mathrm{len}(x) + i}
Def
まず原始再帰的関数$ \lbrack e \rbrackとそのコード$ eを次のように定める. ゼロ関数$ \mathrm{zero}() = 0のコード$ e = \lang 0,0 \rang 後者関数$ \mathrm{succ}(x) = x + 1のコード$ e = \lang 1,1 \rang 射影関数$ \mathrm{proj}^n_i(x_0,\dots,x_{n-1}) = x_iのコード$ e = \lang 2,n,i \rang 関数合成$ \mathrm{comp}(\vec{x}) = \lbrack f \rbrack(\lbrack g_0 \rbrack(\vec{x}), \cdots, \lbrack g_{m-1} \rbrack(\vec{x}))のコード$ e = \lang 3,n,f,g_0,\dots,g_{m-1} \rang 原始再帰$ \begin{aligned} \mathrm{prec}(\vec{x},0) &= \lbrack f \rbrack(\vec{x}) \\ \mathrm{prec}(\vec{x},y+1) &= \lbrack g \rbrack(\vec{x},y,\mathrm{prec}(\vec{x},y)) \end{aligned}のコード$ e = \lang 4,n+1,f,g \rang remark
原始再帰関数のコード$ eに対し$ (e)_1は$ \lbrack e \rbrackのアリティを表している.
Memo
以下では,算術の言語は全ての原始再帰関数の関数記号を含むものとする. $ eをコードとする原始再帰関数$ \lbrack e \rbrackを表す関数記号を$ f_eとする.
また算術の言語として$ \mathbin{=}が導入されれているものとする. Def.1
まず算術の言語のアルファベットに対してGödel数を割り振る. $ \to,\bot,\exists,=,v,fにそれぞれ$ 0,1,2,3,4,5を割り振る.
すなわち,例えば$ \ulcorner v \urcorner = 4とする.
更に↓とする.
変項記号$ v_i = \lang \ulcorner v \urcorner,i \rang
関数記号$ f_e = \lang \ulcorner f \urcorner,e \rang
$ n変数関数$ \lbrack e \rbrackへの変項$ x_0,\dots,x_{n-1}の適用は以下のように表す.
$ \lbrack e \rbrack(x_0,\dots,x_{n-1}) = \lang \ulcorner f_e \urcorner, \lang \ulcorner x_0 \urcorner,\dots,\ulcorner x_{n-1} \urcorner \rang \rang
Def.2
「$ eは原始再帰関数のコードである」という述語$ e \in \mathrm{PRcode}について,原始再帰関数の定義を思い出せば
ゼロ関数$ e = \lang 0,0 \rang
後者関数$ e = \lang 1,1 \rang
射影関数$ e = \lang 2,(e)_1,(e)_2 \rangであり,かつ$ 0 \leq (e)_2 \leq(e)_1 - 1
関数合成は次の条件を全て満たす
$ (e)_0 = 3
$ \mathrm{len}(e) \ge 4
$ 2 \leq i < \mathrm{len}(e)のどんな$ (e)_i \in \mathrm{PRCode}
$ 3 \leq i < \mathrm{len}(e)のどんな$ (e)_{i,1} = (e)_1
関数$ \lbrack g_i \rbrackのアリティは$ \lbrack e \rbrackのアリティに等しい.
原始再帰は次の条件を満たす
$ e = \lang 4,(e)_1,(e)_2,(e)_3 \rang
$ (e)_2,(e)_3 \in \mathrm{PRCode}
$ (e)_{2,1} = (e)_1 - 1
関数$ \lbrack f \rbrackのアリティは$ \lbrack e \rbrackのアリティより1小さく
$ (e)_{3,1} = (e)_1 + 1
関数$ \lbrack g \rbrackのアリティは$ \lbrack e \rbrackのアリティより1大きい
Def.3
「$ nは何らかの変項記号のコードである」という述語$ n \in \mathrm{Ver}
$ n \in \mathrm{Ver} \iff \mathrm{len}(n) = 2 ~\&~ (n)_0 = 4
「$ nは何らかの関数記号のコードである」という述語$ n \in \mathrm{Fnc}
$ n \in \mathrm{Fn} \iff \mathrm{len}(n) = 2 ~\&~ (n)_0 = 5 ~\&~ (n)_1 \in \mathrm{PRcode}
Def.4
「$ nは何らかの項のコードである」:$ n \in \mathrm{Tm}
まず項の形式的定義はこのようであった.
1. 変項$ v_iは項
2. $ n変数関数記号$ f_eと$ n個の項$ t_0,\dots,t_{n-1}に対して関数適用$ f_n(t_0,\dots,t_{n-1})は項
この定義から考えると次の2条件のどちらかとすればよい.
1. 項の場合は$ n \in \mathrm{Ver}とすればよい.
2. 関数適用の場合は次の条件を満たす.
$ (n)_0 \in \mathrm{Fn}
$ \mathrm{len}((n)_1) = (n)_{0,1,1}
$ \ulcorner f_e \urcorner = (n)_0なら$ (n)_{0,1,1}は関数$ \lbrack e \rbrackのアリティを指す
これは関数適用の引数部分の長さがアリティと一致していることを表す.
任意の$ 0 \leq i < (n)_{0,1,1}について$ (n)_{1,i} \in \mathrm{Tm}
引数部分が全て項であることをチェック
これを素朴に翻訳すれば良い.やはり原始再帰的関係となる.
Def.5
数$ xに対して数項$ \overline{x}のGödel数(すなわち$ \ulcorner \overline{x} \urcorner)を返す関数$ \mathrm{num}(x)を次のように定める.
$ \mathrm{num}(0) = \ulcorner \mathrm{zero}() \urcorner = \lang \lang 5, \lang 0,0 \rang \rang, \lang \rang \rang
$ \mathrm{num}(x + 1) = \ulcorner \mathrm{succ}(x ) \urcorner = \lang \lang 5, \lang 1,1\rang \rang , \lang \mathrm{num}(x) \rang \rang
原始再帰的関数.
Def.6
項$ tに出現する変数$ v_nに対して項$ sを代入して得られる項を$ t{\lbrack v_n :=s \rbrack}と表す.
代入操作は次のように定義される.
1. $ t \equiv v_nだった場合,$ t{\lbrack v_n :=s \rbrack} \equiv s
2. $ t \equiv v_m \not\equiv v_nだった場合,$ t{\lbrack v_n :=s \rbrack} \equiv t
3. $ t \equiv f_n(t_0,\dots,t_{n-1})だった場合,$ t{\lbrack v_n :=s \rbrack} \equiv f_n(t_0{\lbrack v_n :=s \rbrack},\dots,t_{n-1}{\lbrack v_n :=s \rbrack})
項への代入結果のGödel数を返す$ \mathrm{substTm}(x,y,z)を考える.
すなわち,$ \mathrm{substTm}(\ulcorner t \urcorner,\ulcorner v_n \urcorner,\ulcorner s \urcorner) = \ulcorner t{\lbrack v_n :=s \rbrack} \urcornerとなる関数のことである.
定義から考える
まず次をチェックする$ x \in \mathrm{Tm}, y \in \mathrm{Var}, z \in \mathrm{Tm}
もしそうでない場合は$ \mathrm{substTm}(x,y,z) = 0とする.
1. $ x = yの場合$ \mathrm{substTm}(x,y,z) = z
2. $ x \in \mathrm{Ver}かつ$ x = yの場合$ \mathrm{substTm}(x,y,z) = x
3. $ x \notin \mathrm{Ver}の場合$ \mathrm{substTm}(x,y,z) = \lang (x)_0,u \rang
ただし$ uは次のようなコードとする.
$ \mathrm{len}(u) = (x)_{0,1,1}
任意の$ 0 \leq i < (x)_{0,1,1}に対して$ (u)_i = \mathrm{substTm}((x)_{1,i},y,z)
このとき$ \mathrm{substTm}(x,y,z) \in \mathrm{Tm}は$ xで帰納法を回すことで確認される.
原始再帰的関数.
Def.7
原子論理式を以下のように定義する.
1. $ \botは原子論理式.
2. $ t,sは項とする.$ t = sは原子論理式.
「$ nは何らかの原子論理式のコード」:$ n \in \mathrm{AtForm}
1. $ n = \ulcorner \bot \urcorner
2. 次の条件を満たす:すなわち$ \ulcorner t = s \urcorner = \lang \ulcorner = \urcorner, \lang \ulcorner t \urcorner, \ulcorner s \urcorner \rang \rang
$ \mathrm{len}(n) = 2
$ (n)_0 = \ulcorner = \urcorner
$ \mathrm{len}((n)_1) = 2
$ (n)_{1,0}, (n)_{1,1} \in \mathrm{Tm}
Def.8
論理式を以下のように定義する.
1. 原子論理式は論理式
2. 論理式$ A,Bに対して$ A \to Bは論理式
3. 論理式$ Aと変項$ v_nに対して$ \exists v_n Aは論理式
「$ nは何らかの論理式のコード」:$ n \in \mathrm{Form}
1. $ n \in \mathrm{AtForm}
2. 次の条件を満たす:すなわち$ \ulcorner A \to B \urcorner = \lang \ulcorner \to \urcorner, \lang \ulcorner A \urcorner, \ulcorner B \urcorner \rang \rang
$ \mathrm{len}(n) = 2
$ (n)_0 = \ulcorner \to \urcorner
$ \mathrm{len}((n)_1) = 2
$ (n)_{1,0}, (n)_{1,1} \in \mathrm{Form}
3. 次の条件を満たす:すなわち$ \ulcorner \exists v_n A \urcorner = \lang \lang \ulcorner \exists \urcorner, \ulcorner v_n \urcorner\rang, \ulcorner A \urcorner \rang
$ \mathrm{len}(n) = 2
$ \mathrm{len}((n)_0) = 2
$ (n)_{0,0} = \ulcorner \exists \urcorner
$ (n)_{0,1} \in \mathrm{Ver}
$ (n)_{1} \in \mathrm{Form}
Def.9
次の関数を定義する.
$ \mathrm{imp}(\ulcorner A \urcorner, \ulcorner B \urcorner) = \lang \ulcorner \to \urcorner, \lang \ulcorner A \urcorner,\ulcorner B \urcorner \rang \rang = \ulcorner A \to B \urcorner
$ \mathrm{not}(\ulcorner A \urcorner) = \mathrm{imp}(\ulcorner A \urcorner,\ulcorner\bot \urcorner) = \ulcorner A \to \bot \urcorner = \ulcorner \lnot A \urcorner
$ \mathrm{exists}(\ulcorner v \urcorner, \ulcorner A \urcorner) = \lang \lang \ulcorner \exists \urcorner, \ulcorner v \urcorner\rang, \ulcorner A \urcorner \rang = \ulcorner \exists vA \urcorner
$ \mathrm{forall}(\ulcorner v \urcorner, \ulcorner A \urcorner) = \mathrm{not}(\mathrm{exists}(\ulcorner v \urcorner, \mathrm{not}(\ulcorner A \urcorner))) = \ulcorner \lnot \exists v \lnot A \urcorner = \ulcorner \forall v A \urcorner
$ \mathrm{imp}(\ulcorner A \urcorner, \ulcorner B \urcorner, \ulcorner C \urcorner) = \lang \ulcorner \to \urcorner, \lang \ulcorner A \urcorner, \lang \ulcorner \to \urcorner, \lang \ulcorner B \urcorner, \ulcorner C \urcorner \rang \rang \rang \rang = \ulcorner A \to B \to C\urcorner