# zbMATH — the first resource for mathematics

$$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].

##### MSC:
 03F30 First-order arithmetic and fragments