Arithmetizing uniform \(NC\) (Q1176198)

The characterization of classes of polynomially bounded functions by means of bounded arithmetic is the central theme of this paper. The three concepts: 1) Boolean circuit definable, 2) (mathematically) recursion definable and 3) representable in bounded arithmetic are analyzed and compared. The paper contains many interesting results about polynomial complexity and induction in bounded arithmetic. Of particular interest is the comparison of different induction schemata for bounded arithmetic, where special emphasis is laid on a recursion schema modelling the divide and conquer technique. We shall describe some of the concepts and results in more detail: NC describes the functions computable in polylogarithmic depth and polynomial size by families of Boolean circuits (the family has to be log-space uniform). BL denotes a class of functions containing some basic functions (among them are lading functions) which are closed under the map operator, under composition and under polynomially bounded branching recursion; polynomially bounded branching recursion is an abstraction of the divide and conquer technique. The first main result is that BL is equal to (logspace uniform) NC. The second part starts with a presentation of bounded arithmetic (quantifiers are term-bounded), where different kinds of induction schemata are analyzed:\parindent=8mm\smallskip\begin{itemize}\item[(1)] the ``usual'' schema: \(\Phi(0)\land(\forall x)(\Phi(x)\to\Phi(x+1))\to(\forall x)\Phi(x)\qquad(\Phi\hbox{-IND})\);\smallskip\item[(2)] \(\Phi(0)\land(\forall x)(\Phi([{1\over 2}x])\to\Phi(x))\to(\forall x)\Phi(x)\qquad(\Phi\hbox{-PIND})\);\smallskip\item[(3)] \(\Phi(0)\land(\forall x)(\Phi(x)\to\Phi(x+1))\to(\forall x)\Phi(| x|)\qquad(\Phi\hbox{-LIND})\) \((| x|\) is the length of the binary representation of \(x\));\smallskip\item[(4)] \(\Phi(0)\land\Phi(1)\land(\forall x)(\Phi(Fh(x))\land\Phi(Bh(x))\to\Phi(x))\to(\forall x)\Phi(x)\qquad(\Phi\hbox{-DCI}\) ``divide and conquer induction'', here \(Fh\) is a function describing a front half, \(Bh\) a function describing a back half via the binary coding);\smallskip\item[(5)] \(\Phi(0)\land(\forall x)(\Phi([{1\over 2}x])\to\Phi(x))\to(\forall x)\Phi(| x|)\quad(\Phi\hbox{-LPIND})\) (combining features of 2 and 3);\smallskip\item[(6)] \(\Phi(0)\land(\forall x)(\Phi(x)\to\Phi(x+1))\to(\forall x)\Phi(\| x\|)\qquad(\Phi\hbox{- LLIND})\).\smallskip\parindent=0pt In their further application the induction schemata are restricted to instances of the form \(\Sigma^ b_ i\) (bounded \(\Sigma_ i\)-forms). A key role play the systems \(D^ i_ 2\), where the induction axioms are of the form DCI with instances of the form \(\Sigma^ b_ i\). It is shown that the \(\Sigma^ b_ i\)- LPIND and \(\Sigma\)-LLIND induction axioms are derivable in \(D^ i_ 2\). If the \(\Sigma^ b_ i\)-DCI schema is available, then \(\Sigma^ b_ i\)-LP induction, \(\Sigma^ b_ i\)-LL induction and \(\Sigma^ b_ i\)- DC induction systems are all equivalent. It is shown how arithmetical definability corresponds to the class NC (and thus to BL): Uniform NC can be defined via \(\Sigma^ b_ 1\)-DCI induction. On the other hand, \(\Sigma^ b_ 1\)-DCI induction definable functions in \(\Sigma^ b_ 1\)-form are contained in uniform NC and thus in BL. Technically the last results were obtained by complexity analysis in a bounded sequent calculus (i.e. a sequent calculus containing rules for DCI induction and bounded quantifier introduction).\end{itemize}