RSUV isomorphisms for TAC\(^ i\), TNC\(^ i\) and \(TLS\) (Q1345903)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | RSUV isomorphisms for TAC\(^ i\), TNC\(^ i\) and \(TLS\) |
scientific article |
Statements
RSUV isomorphisms for TAC\(^ i\), TNC\(^ i\) and \(TLS\) (English)
0 references
1 May 1995
0 references
\textit{P. Clote} and the author [``First order bounded arithmetic and small Boolean circuit complexity classes'', in: Feasible mathematics. II (to appear)], introduced the theories in Bounded Arithmetic \(\text{TAC}^ i\), \(\text{TNC}^ i\) and TLS which correspond to computational classes \(\text{AC}^ i\), \(\text{NC}^{i+1}\), and Logspace respectively. In the paper ``RSUV isomorphisms'' [Arithmetic, proof theory and computational complexity, Oxf. Logic Guides 23, 364-386 (1993; Zbl 0792.03041)], the author introduced the RSUV isomorphism. The basic idea of the RSUV isomorphism is that bounded second-order objects in the bounded second- order Bounded Arithmetic correspond to first-order objects in the first- order Bounded Arithmetic and that first-order objects in the second-order theory correspond to lengths of objects in the appropriate first-order theory. By a bounded second-order object we mean a predicate \(\alpha\) on the integers \(\leq a\) for some first-order object \(a\), which is denoted by \(\alpha^ a\). To make the correspondence between a bounded second- order \(\alpha^ a\) and a first-order object \(b\), we interpret the truth values of \(\alpha^ a (i)\) as the bits in the binary representation of \(b\). This makes a first-order interpretation of the second-order concept and an inverse second-order interpretation of the first-order concept. By this way, we can find isomorphism between a first-order theory and an appropriate second-order theory. This isomorphism is called the RSUV isomorphism between two theories in the previous paper. In this paper the following question was investigated and answered. What kind of second-order theories correspond to \(\text{TAC}^ i\), \(\text{TNC}^ i\) and TLS by the RSUV isomorphism? The central result of this paper is that \(\text{TAC}^ 0\) is isomorphic to \(\Delta_ 0^{1,b} (BD)\)-extension of \(T_ 1\), where \(T_ 1\) is \(\bigcup_ i T_ 1^ i\) and \(T_ 1^ i\) is obtained from Buss's system \(T_ 2^ i\) by deleting \(\#\). \(T_ 1\) is equivalent to \(I\Delta_ 0\) investigated by Wilkie and Paris and therefore \(\Delta_ 0^{1,b} (BD)\)-extension of \(T_ 1\) is equivalent to \(\Delta_ 0^{1,b} (BD)\)- extension of \(I\Delta_ 0\) which we denote by \(I\widetilde {\Delta}_ 0\). \(I\widetilde {\Delta}_ 0\) is a conservative extension of \(I\Delta_ 0\). Thus \(\text{TAC}^ 0\) and \(I\widetilde {\Delta}_ 0\) are isomorphic and this isomorphism makes our understanding of \(\text{TAC}^ 0\) and \(I\Delta_ 0\) much better.
0 references
bounded arithmetic
0 references
computational classes
0 references
RSUV isomorphism
0 references
bounded second-order object
0 references
conservative extension
0 references