べき乗のグラフはΣ₀定義可能, 帰納的性質はIΣ₀で証明可能
定理
指数関数のグラフを表現する$ \Sigma_0論理式$ \Psiが存在する
$ 2^n = m \iff \N \models \Psi(\bar n, \bar m)
その基礎的な性質は$ \mathsf I\Sigma_0で証明可能である
$ \mathsf I\Sigma_0 \vdash \Psi(0, 1)
$ \mathsf I\Sigma_0 \vdash (\forall x, y)[\Psi(x, y) \equiv \Psi(x + 1, 2 y)]
$ \mathsf I\Sigma_0 \vdash (\forall x, y_1, y_2)[\Psi(x, y_1) \to \Psi(x, y_2) \to y_1 = y_2]
全域性は$ \mathsf I\Sigma_1で証明可能である
$ \mathsf I\Sigma_1 \vdash (\forall x)(\exists! y)\Psi(x, y)
証明の方針
素朴に以下のような方法を考えると
$ \Psi(x, y) \coloneqq (\exists z_0, ..., z_{x})[z_0 = 1 \land z_x = y \land (\forall i < x)[z_{i + 1} = 2z_i]]
$ \|\braket{z_0, .., z_x}\| = \|\braket{2^0, 2^1, ..., 2^x}\| \ge 1 + 2 + ... + x = O(x^2)
なので$ \braket{z_0, ..., z_x}は$ 2^{O(x^2)}のオーダーになってしまい多項式でboundできない
そこで二進法展開を使った以下の方法を用いる
$ x = \sum_{i < K} b_i 2^i = [b_{K-1} \ ...\ b_2 b_1 b_0]
ただし$ b_{K-1} = 1
$ x の上から$ i 個の列が表す数を$ x^{(i)} = [b_{K-1}b_{K - 2}\ ...\ b_{K - i}] とする
また$ y^{(i)} = 2^{x^{(i)}}となるように$ y^{(i)}を定義する
$ x^{(1)} \coloneqq 1
$ x^{(i + 1)} \coloneqq 2 x^{(i)} + b_{K - 1 - i}
$ y^{1} \coloneqq 2
$ y^{(i + 1)} \coloneqq 2^{b_{K - 1 - i}}(y^{(i)})^2
このとき明らかに$ x^{(K)} = x, また$ y^{(K)} = 2^{x^{(K)}} = 2^x = y
ここで$ x^{(0)} = 0, y^{(0)} = 1スタートではないのは, そのようにすると$ X, Yが一意に定まらず面倒だからである
このとき、$ y^{(K)}の計算に用いたのは
$ X \coloneqq \braket{x^{(1)}, x^{(2)}, ..., x^{(K)}}, Y \coloneqq \braket{y^{(1)}, y^{(2)}, ..., y^{(K)}}
各$ i \le Kについて$ x^{(i)} < 2^{i}, $ y^{(i)} < 2^{2^i}であることに注意すると, 十分効率的にエンコードされているならば
$ X = O\left(\prod_{1 \le i \le K}2^i\right) = O(2^{\frac{1}{2}K(K+1)}) \le O(y)
$ Y = O\left(\prod_{1 \le i \le K} 2^{2^i}\right) = O(2^{2^{K+1}-1}) \le O(y^4)
のように$ yの多項式でboundされる！
よって$ \Sigma_0論理式で表現可能である.
ただし列$ X, Yのエンコードは若干面倒である
$ x^{(i)}, y^{(i)} < 2^{2^i}を使って次のエンコードを用いる
すなわち, 以下のように$ 2^iビットずつ分離し、各$ 2^i桁の領域に$ <2^{2^i}の情報を格納する
$ Y = [...\ \underbrace{1001110011101110}_{2^4}\ \underbrace{00100111}_{2^3}\ \underbrace{1010}_{2^2} \ \underbrace{01}_{2^1} \ 0\ {0}]
$ = ... + [1001110011101110]2^{2^4} + [00100111] 2^{2^3} + [1010]2^{2^2} + [01]2^{2^1}
$ = ... + y^{(4)}2^{2^4} + y^{(3)} 2^{2^3} + y^{(2)}2^{2^2} + y^{(1)}2^{2^1}
$ i番目の要素のアクセスには$ \mathrm{ext}(2^{2^i}, z) = z /2^{2^i}\ \mathrm{mod}\ 2^{2^i}を用いる
$ y^{(1)} = 2を格納するため1, 2桁目の数字は捨てる
補題
以下が$ \mathsf I \Sigma_0で証明可能な$ \Sigma_0論理式$ \mathrm{PPow2}(u)が存在する
P1: $ \lnot\mathrm{PPow2}(0), $ \lnot\mathrm{PPow2}(1)
P2: $ \mathrm{PPow2}(u) \iff u = 2^{2^0} \lor \exists v, u = v^2 \land \mathrm{PPow2}(v)
P3: $ \mathrm{PPow2}(x) \to \mathrm{Pow2}(x)
これはP1, P2から導出できる（$ \mathsf I\Sigma_0）
P4: $ \mathrm{PPow2}(u), \mathrm{PPow2}(v), v < uならば$ v^2 \le u
これはP2から導出できる（$ \mathsf I\Sigma_0）
これは$ \{2^{2^i} | i \in \N\}を想定している
Proof.
定義
次のように$ \Psi(x, y)を定義する。これは明らかに$ \Sigma_0論理式である
$ \Psi(x, y) \coloneqq (x = 0 \land y = 1) \lor (\exists X, Y \le y^4)\left[\Psi_\mathrm{zero}(X, Y) \land \Psi_\mathrm{succ}(y,X, Y) \land \Psi_\mathrm{mem}(x, y, X, Y)\right]
$ \Psi_\mathrm{zero}(X, Y) \coloneqq \left[\mathrm{ext} (2^{2^1}, X) = 1 \land \mathrm{ext} (2^{2^1}, Y) = 2\right]
$ \Psi_\mathrm{succ}(y,X, Y) \coloneqq (\forall u \le y)\left[\mathrm{PPow2}(u) \to \Phi_\mathrm{even}(X, Y, u) \lor \Phi_\mathrm{odd}(X, Y, u)\right]
$ \Phi_\mathrm{even}(X, Y, u) \coloneqq \left[ \mathrm{ext}(u^2, X) = 2\mathrm{ext}(u, X) \land \mathrm{ext}(u^2, Y) = (\mathrm{ext}(u, Y))^2 \right]
$ \Phi_\mathrm{odd}(X, Y, u) \coloneqq \left[ \mathrm{ext}(u^2, X) = 2\mathrm{ext}(u, X) + 1 \land \mathrm{ext}(u^2, Y) = 2(\mathrm{ext}(u, Y))^2 \right]
$ \Psi_\mathrm{mem}(x,y,X,Y) \coloneqq (\exists u \le y^2)[\mathrm{PPow2}(u) \land \mathrm{ext}(u, X) = x \land \mathrm{ext}(u, Y) = y]
補助的な定義をする
$ \mathrm{append}(u, X, z) \coloneqq X \ \mathrm{mod}\ u + zu
$ u = 2^{2^i},$ z < 2^{2^i}であったときに$ zを$ i番目に格納した列を返す関数
$ \mathrm{PPow2}(u), $ z < uとする。以下が成り立つ
$ \mathrm{ext}(u,\mathrm{append}(u, X, z)) = z
$ v < uについて$ \mathrm{ext}(v, \mathrm{append}(u, X, z)) = \mathrm{ext}(v, X)
P3, P4による
$ \mathrm{append}(u, X, z) \le u + zu \le u^2
補題：$ \mathsf I \Sigma_0 \vdash \Psi(0, 1)
$ X \coloneqq 0, $ Y \coloneqq 2
$ \mathrm{ext}(2^{2^0}, 0) = 0, $ \mathrm{ext}(2^{2^0}, 2) = 1より$ \Psi_\mathrm{zero}(X, Y), $ \Psi_\mathrm{mem}(0,1,X,Y)
P1:$ \lnot\mathrm{PPow2}(0), \lnot\mathrm{PPow2}(1)より$ \Psi_\mathrm{succ}(X, Y)
よって成り立つ
$ \mathsf I \Sigma_0 \vdash (\forall x, y)[\Psi(x, y) \equiv \Psi(x + 1, 2 y)\rbrack
次を示す
$ \Psi(2x, y) \iff (\exists y')\lbrack y = y'^2 \land \Psi(x, y')\rbrack
$ \Longrightarrow
$ \Psi_\mathrm{zero}(X, Y), \Psi_\mathrm{succ}(X, Y), \Psi_\mathrm{mem}(2x, y, X, Y)を満たす$ X, Yを固定する。$ \Psi_\mathrm{mem}(x, y, X, Y)を示す
$ u \le y^2 + 1, \mathrm{PPow2}(u), \mathrm{ext}(u, X) = 2x, \mathrm{ext}(u, Y) = yを満たす$ uをとる
$ u = 2^{2^0}ならば$ \Psi_\mathrm{zero}(X, Y)より$ 2x = 0, $ y = 1なので成り立つ
$ 2^{2^0} < uと仮定する。P2より$ u = v^2かつ$ \mathrm{PPow2}(v)を満たす$ vが存在する
$ \Psi_\mathrm{succ}(X, Y)より$ 2x = 2\mathrm{ext}(v, X), $ y = \mathrm{ext}(v, Y)^2
よって$ y' \coloneqq \mathrm{ext}(v, Y)とすると$ y = y'^2
よって$ \Psi_\mathrm{mem}(x, y', X, Y)
$ \Longleftarrow
$ \Psi(x, y) \implies \Psi(2x, y^2)を示す
$ \Psi_\mathrm{zero}(X, Y), \Psi_\mathrm{succ}(X, Y), \Psi_\mathrm{mem}(x, y, X, Y)を満たす$ X, Yを固定する
$ u \le y^2, \mathrm{PPow2}(u), \mathrm{ext}(u, X) = x, \mathrm{ext}(u, Y) = yを満たす$ uをとる
$ X' \coloneqq \mathrm{append}(u^2, X, 2x)
$ Y' \coloneqq \mathrm{append}(u^2, Y, y^2)とする
このとき
$ X', Y' \le u^4 \le y^8
$ \Psi_\mathrm{zero}(X',Y')：$ 2^{2^0} < uより
$ \Psi_\mathrm{succ}(X',Y')：
$ y < u \le y^2となる$ uの一意性より$ \Phi_\mathrm{even}(X', Y', u) \lor \Phi_\mathrm{odd}(X', Y', u)を確かめればよい
一意性について
$ y < u, u' \le y^2, \mathrm{PPow2}(u), \mathrm{PPow2}(u')と仮定する
$ u < u'として一般性を失わない. P4より$ y^2 < u^2 \le u' \le y^2, 矛盾.
特に$ \Phi_\mathrm{even}(X', Y', u)が成立する
$ \mathrm{ext}(u, X') = \mathrm{ext}(u, X) = x, $ \mathrm{ext}(u^2, X') = 2x
$ \mathrm{ext}(u, Y') = \mathrm{ext}(u, Y) = y, $ \mathrm{ext}(u^2, Y') = y^2より
$ \Psi_\mathrm{mem}(2x, y^2, X', Y')：
$ u^2 \le (2y)^2より
よって$ \Psi(2x, y^2)
$ \Psi(2x + 1, y) \iff (\exists y')\lbrack y = 2y'^2 \land \Psi(x, y') \rbrack
上と同様に示す
$ \Psi(x, y) \iff \Psi(x + 1, 2y)
$ (\forall x \le y)[\Psi(x, y) \equiv \Psi(x + 1, 2y)]
$ xを固定する
$ x = 2x'のとき
$ \Psi(2x', y) \iff \Psi(x', \sqrt{y}) \iff \Psi(2x' + 1, 2y)
$ x = 2x' + 1のとき
$ \Psi(2x' + 1, y) \iff \Psi(x', \sqrt{y/2}) \iff \Psi(x' + 1, 2\sqrt{y/2}) \iff \Psi(2x' + 2, 2y)
2番目の$ \iffは帰納法の仮定による
$ \mathsf I\Sigma_0 \vdash (\forall x, y_1, y_2) \lbrack\Psi(x, y_1) \to \Psi(x, y_2) \to y_1 = y_2\rbrack