\(RSUV\) isomorphisms.

*(English)*Zbl 0792.03041
Clote, Peter (ed.) et al., Arithmetic, proof theory, and computational complexity. Oxford: Clarendon Press. Oxf. Logic Guides. 23, 364-386 (1993).

In his book: Bounded arithmetic (1986; Zbl 0649.03042), S. Buss introduced the systems \(S^ i_ 3\), \(S^ i_ 2\), \(V^ i_ 2(BD)\), and \(U^ i_ 2(BD)\), where \(S^ 1_ 2\), \(V^ 1_ 2(BD)\) and \(U^ 1_ 2(BD)\) correspond to polynomial time computable functions, exponential time computable functions, and polynomial space computable functions, respectively, and \(S^ i_ 3\) is a generalization of \(S^ i_ 2\) by introducing \(\#_ 3\) with the intended property \(a\#_ 3 b= 2^{| a|\#| b|}\). In a previous paper [Arch. Math. Logic 29, No. 3, 149-169 (1990; Zbl 0681.03040)], the author established an interpretation of \(V^ i_ 2(BD)\) in \(S^ i_ 3\) and an inverse interpretation of \(S^ i_ 3\) in \(V^ i_ 2(BD)\). In the present paper the isomorphisms between \(V^ i_ 2(BD)\) and \(S^ i_ 3\) and between \(R^ i_ 3\) and \(U^ i_ 2(BD)\) are proved, where \(R^ i_ 3\) is obtained from \(R^ i_ 2\) by introducing \(\#_ 3\) and \(R^ 1_ 2\) is equivalent to the system of B. Allen [Ann. Pure Appl. Logic 53, No. 1, 1-50 (1991; Zbl 0741.03019)] and also to P. Clote’s system TNC [P. Clote and the author, Ann. Pure Appl. Logic 56, No. 1-3, 73-117 (1992; Zbl 0772.03028)], both of which correspond to NC.

These isomorphisms are also extended in the paper to the isomorphisms between \(R^ i_{k+1}\) and \(U^ i_ k(BD)\) and between \(S^ i_{k+1}\) and \(V^ i_ k(BD)\), where \(R^ i_{k+1}\), \(S^ i_{k+1}\), \(U^ i_{k+1}(BD)\), and \(V^ i_{k+1}(BD)\), respectively, by introducing \(\#_{k+1}\) with the intended property \(a\#_{k+1} b= 2^{a\#_ k b}\). The isomorphism between \(S^ i_{k+1}\) and \(V^ i_ k(BD)\) is also independently proved by A. A. Razborov [“An equivalence between second order bounded domain bounded arithmetic and first order bounded a arithmetic”, P. Clote (ed.) et. al.: Arithmetic, proof theory, and computational complexity, Oxford Logic Guides 23, 247- 277 (1993)]. In the paper the author also proved conservative rsults between \(U^ i_ 2(BD)\) and \(\overline U^ i_ 2(BD)\), where \(\overline U^ i_ 2(BD)\) is obtained from \(U^ i_ 2(BD)\) by introducing \(\Delta^{1,b}_ i\)-comprehension schema.

Finally it is shown that \(V^{i+1}_ 2\) proves \(\forall x\leq a \exists y(A(x,y)\land| y|\leq b)\to \exists t \forall x\leq a \exists y\leq t A(x,y)\), where \(A(x,y)\) is a \(\Sigma^ b_ i\)-formula and \(V^{i+1}_ 2\) is also Buss’ system closely related to \(V^{i+1}_ 2(BD)\).

For the entire collection see [Zbl 0777.00008].

These isomorphisms are also extended in the paper to the isomorphisms between \(R^ i_{k+1}\) and \(U^ i_ k(BD)\) and between \(S^ i_{k+1}\) and \(V^ i_ k(BD)\), where \(R^ i_{k+1}\), \(S^ i_{k+1}\), \(U^ i_{k+1}(BD)\), and \(V^ i_{k+1}(BD)\), respectively, by introducing \(\#_{k+1}\) with the intended property \(a\#_{k+1} b= 2^{a\#_ k b}\). The isomorphism between \(S^ i_{k+1}\) and \(V^ i_ k(BD)\) is also independently proved by A. A. Razborov [“An equivalence between second order bounded domain bounded arithmetic and first order bounded a arithmetic”, P. Clote (ed.) et. al.: Arithmetic, proof theory, and computational complexity, Oxford Logic Guides 23, 247- 277 (1993)]. In the paper the author also proved conservative rsults between \(U^ i_ 2(BD)\) and \(\overline U^ i_ 2(BD)\), where \(\overline U^ i_ 2(BD)\) is obtained from \(U^ i_ 2(BD)\) by introducing \(\Delta^{1,b}_ i\)-comprehension schema.

Finally it is shown that \(V^{i+1}_ 2\) proves \(\forall x\leq a \exists y(A(x,y)\land| y|\leq b)\to \exists t \forall x\leq a \exists y\leq t A(x,y)\), where \(A(x,y)\) is a \(\Sigma^ b_ i\)-formula and \(V^{i+1}_ 2\) is also Buss’ system closely related to \(V^{i+1}_ 2(BD)\).

For the entire collection see [Zbl 0777.00008].

Reviewer: G.Takeuti (Urbana, IL)

##### MSC:

03F30 | First-order arithmetic and fragments |