NuonはΣ₀論理式で定義可能. 帰納的性質はIΣ₀で証明可能
$ \frac{n}{2^i} \% 2を$ nの$ i桁目の数とする
定義
自然数の2進数列展開において, 含まれている$ 1の数を返す関数を$ \mathrm{nuon}とする すなわち以下を満たすような関数$ \mathrm{nuon} \colon \N \to \N
$ \mathrm{nuon}(0) \coloneqq 0
$ \mathrm{nuon}(2x) \coloneqq \mathrm{nuon}(x)
$ \mathrm{nuon}(2x + 1) \coloneqq \mathrm{nuon}(x) + 1
定理
$ \mathrm{nuon}は$ \Sigma_0論理式で定義可能
$ \N \models \mathrm{Nuon}(x, y) \iff \mathrm{nuon}(x) = y
基礎的な性質は$ \mathbf{I\Sigma_0}で証明可能
$ \mathbf{I\Sigma_0} \vdash (\forall x)(\exists! y)\mathrm{Nuon}(x, y)
$ \mathbf{I\Sigma_0} \vdash \mathrm{Nuon}(0, 0)
$ \mathbf{I\Sigma_0} \vdash (\forall x, y)[\mathrm{Nuon}(x, y) \to \mathrm{Nuon}(2x, y)]
$ \mathbf{I\Sigma_0} \vdash (\forall x, y)[\mathrm{Nuon}(x, y) \to \mathrm{Nuon}(2x + 1, y + 1)]
証明の方針
素朴に以下のように定義すると
$ \mathrm{Nuon}(A, n) \coloneqq (\exists z_0, ... z_{\|x\|})[z_0 = 0 \land n = z_{\|A\|} \land (\forall i < \|x\|)[z_{i+1} = z_i + \mathrm{fbit}(A, i)]]
$ \mathrm{fbit}(x, i)は$ xを二進展開したときの$ i+1桁目の数
$ z_i \le \|A\|であることに注意すると, $ \braket{z_0, ..., z_{\|A\|}} \ge 2^{\|\|A\|\| \cdot \|A\|} \ge A^{\|\|A\|\|}より$ \braket{z_0, ..., z_{\|x\|}}は多項式でboundできない
以下の$ U, L, Iは量化子の上限や量化範囲として使用されるもので, 十分大きく, ただし$ Aの多項式でboundされるものとする
定義
$ (T)^L_iは$ Tの$ i\|L\|桁から$ (i+1)\|L\|桁までで表される数
$ (T)^L_i \coloneqq \frac{T}{2^{i \|L\|}} \% 2^{\|L\|}
自然数$ Aの$ i桁から$ i + l桁に登場する$ 1の数を$ n_sに加えた数が$ n_eとなることを意味する論理式を$ \mathrm{Segment}_{U, L}(A, i, l, n_s, n_e)とする
$ \mathrm{Segment}_{U,L}(A, i, l, n_s, n_e) \coloneqq (\exists S < U)\left[(S)^L_0 = n_s \land (S)^L_l = n_e \land (\forall j < l)[(S)^L_{j + 1} = (S)^L_j + \mathrm{fbit}(A, i + j)]\right]
$ Aを$ 0の桁から$ \|I\|個ずつ分割した部分が$ m個あるとき, それらに現れる$ 1の数が$ nであることを意味する論理式を$ \mathrm{Series}_{U,I,L}(A, m, n)とする
$ \mathrm{Series}_{U, I, L}(A, m, n) \coloneqq (\exists T < U)\left[(T)^L_0 = 0 \land (T)^L_m = n \land (\forall l < m)[\mathrm{Segment}_{U, L}(A, l \cdot \|I\|, \|I\|, (T)^L_l, (T)^L_{l+1})]\right]
$ Aの下から$ k桁の部分$ A \upharpoonright kについて, $ \|I\|ごと区切った部分に現れる$ 1の数と残りの$ k \% \|I\|桁の部分に現れる$ 1の数の和が$ nであることを意味する論理式を$ \mathrm{SeriesSegment}_{U, I, L}(A, k, n)とする
$ \mathrm{SeriesSegment}_{U, I, L}(A, k, n) \coloneqq (\exists n_k \le n)\left[\mathrm{Series}_{U, I, L}\left(A, \frac{k}{\|I\|}, n_k\right) \land \mathrm{Segment}_{U, L}\left(A, \|I\| \cdot \frac{k}{\|I\|}, k \% \|I\|, n_k, n\right)\right]
$ A \upharpoonright k = \underbrace{1 \dots 011}_{k \% \|I\|}\overbrace{|\underbrace{101 \dots 110}_{\|I\|}| \dots |\underbrace{100 \dots 010}_{\|I\|}|\underbrace{111 \dots 001}_{\|I\|}|}^{\frac{k}{\|I\|}}
これは$ \mathrm{Nuon}(A \upharpoonright k, n)に等しい
$ \mathrm{Nuon}(A, n)を定義する
$ \mathrm{NuonAux}(A, k, n) \coloneqq \mathrm{SeriesSegment}_{U(A), I(A), L(A)}(A, k, n)
$ \mathrm{Nuon}(A, n) \coloneqq \mathrm{NuonAux}(A, \|A\|, n)
ここで$ U(A), I(A), L(A)は以下を満たす関数である
多項式でboundされる
$ 2^{2 \|I(A)\|\|L(A)\|} \le U(A)
$ \|\|I(A)\|^2\| \le \|L(A)\|
$ \|A\| < \|I(A)\|^2
例えば次のようにすればよい
$ I(A) \coloneqq 2^{\sqrt{\|A\|}}
$ L(A) \coloneqq \|I(A)\|^2
$ U(A) \coloneqq (2A + 1)^{128}
定理
$ k \le \|A\|について
$ \mathrm{NuonAux}(A, k, n)ならば$ \mathrm{NuonAux}(2A, k + 1, n), また$ \mathrm{NuonAux}(2A + 1, k + 1, n + 1)
$ \mathrm{NuonAux}(A, k, n)を満たす$ nが存在する