形式化された有限列（限定算術）

定義

有限列$ sは次の三つ組みで表される：

$ s = (u, \max, \mathrm{lh})

$ \maxは$ sに含まれる最大の数，$ \mathrm{lh}は$ sの長さを表す

$ (s)_i = x \iff x \le \max \land (\forall j \le \|\mathrm{max}\|)[\mathrm{bit}(u, \|\mathrm{max}\| i + j) = \mathrm{bit}(x, j)]

よってグラフは$ \Delta^b_1論理式で定義可能

またこのとき$ \|u\| \le \|\mathrm{max}\| \mathrm{lh}より

最大値$ m, 長さ$ lの有限列$ sはある項$ boundによって

$ s \le bound(m, 2^l)

と押さえられる

#Metamathematics_of_First-Order_Arithmetic p.325

ここではこの意味での有限列の判定を$ \mathrm{Seq^b}(x), 長さを$ \mathrm{lh^b}(x)と書く．

性質

補題

$ \mathsf{S}_2^1 \vdash (\exists w_\mathrm{empty})[\mathrm{Seq}(w_\mathrm{empty}) \land \mathrm{lh}(w_\mathrm{empty}) = 0]

$ \mathsf{S}_2^1 \vdash (\forall w, x)[\mathrm{Seq}(w) \to (\exists w_\mathrm{concat})[\mathrm{Seq}^b(w_\mathrm{concat}) \land (w_\mathrm{concat})_{\mathrm{lh}(w)} = x \land (\forall i < \mathrm{lh})[(w)_i = (w_\mathrm{concat})_i]]]