β 簡約の算術化

変数を $v_0,v_1,\ldots$ とし、（α 同値で同一視する前の）項に符号を $\ulcorner v_i\urcorner=\langle0,i\rangle$、$\ulcorner PQ\urcorner=\langle1,\ulcorner P\urcorner,\ulcorner Q\urcorner\rangle$、$\ulcorner\lambda v_i.P\urcorner=\langle2,i,\ulcorner P\urcorner\rangle$ で与える（$\langle x_0,\ldots,x_k\rangle=\prod_{j\le k}p_j^{x_j+1}$）。$\mathrm{Red}(a,b)$ を「$a$ は項の符号で、$b$ は、$a$ の項の部分項 1 つを、(α) $\lambda v_j.P$ と $\lambda v_k.P[v_j:=v_k]$（$v_k$ は $P$ に現れない変数）の一方から他方に付け替えるか、(β) β 基 $(\lambda v_i.M)N$ で $M$ のどの $\lambda v_j$（$v_j\in\mathrm{FV}(N)$）の作用域にも自由な $v_i$ がないものを、$M$ の自由な $v_i$ を $N$ に置き換えた項に縮約して得られる項の符号」とする。ここで §2 の α 同値（束縛変数の付け替えで移り合うこと）は、(α) の付け替えを部分項に有限回施して移り合うこと、と精密に読む（Barendregt の教科書の定義と同じ）。このとき

1. $\mathrm{Red}$ は原始再帰的である。
2. (i) 符号 $a$ から符号 $b$ まで $\mathrm{Red}$ の有限列でつながるならば、$a$ の表す項は $b$ の表す項に $\twoheadrightarrow_\beta$ で簡約される。(ii) $M\twoheadrightarrow_\beta N$ ならば、$M$ の任意の表し方の符号 $a$ から、$N$ のある表し方の符号まで $\mathrm{Red}$ の有限列でつながる。
3. $\mathrm{Num}(b)$「$b$ はあるチャーチ数と α 同値な項の符号」と、そのときの値 $\mathrm{val}(b)$（$\mathrm{Num}(b)$ でなければ $0$）は原始再帰的である。
4. 閉項 $F$ を固定すると、$\vec n\mapsto\ulcorner F\vec{\overline n}\urcorner$ は原始再帰的である。