S₂でnuon(x)はΔᵇ₁定義可能
定理
$ \mathsf S_2^1において$ \mathrm{nuon}(x)は$ \Delta^b_1論理式で定義可能.またその帰納的性質も証明可能 Proof.
$ \mathrm{nuon}(x, y) \coloneqq (\exists s \le x \# x)[\mathrm{seq^b}(s) \land (s)_0 = 0 \land (\forall i < \mathrm{lh^b}(s))[(s)_{i+1} = (s)_i + \mathrm{fbit}(x, i)] \land (s)_{|x|} = y]
$ \equiv (\forall s \le x \# x)[(\mathrm{seq^b}(s) \land (s)_0 = 0 \land (\forall i < \mathrm{lh^b}(s))[(s)_{i+1} = (s)_i + \mathrm{fbit}(x, i)]) \to (s)_{|x|} = y]
$ \mathrm{lh^b}(s) < |s|に注意