End extensions of models of linearly bounded arithmetic (Q1377910)

The paper is about the end extension problem for bounded second order arithmetic, linear arithmetic LA and \(\Sigma^{p}_{0}\) first-order recursion schema, denoted \(\Sigma^{p}_{0}\)-rec -- both subsystems (the second one possibly not proper) of second order bounded arithmetic BA. \(\Sigma^{p}_{0}\) is the class of bounded polynomial formulas (no second order quantifiers). Axioms of LA consist of the usual ordered semiring axioms plus statements expressing that every set is bounded and has a least upper bound, and the comprehension schema for formulas of the language of bounded Presburger arithmetic (no multiplication). \(\Sigma^{p}_{0}\)-rec is axiomatized by \(\Sigma^{p}_{0}\)-comprehension schema and the recursion schema \[ \forall<a\exists a\varphi(x,y)\rightarrow\exists Z \forall w<b\varphi(Z(w),Z(w+1)), \] where \(\varphi\in\Sigma^{p}_{0}\) and \(Z(x)\) is the value at \(x\) of the function coded by \(Z\). In section 2 an argument is offered to show that functions computable in polynomial time are provably total in \(\Sigma^{p}_{0}\)-rec. The rest of the paper is devoted to the proof of the main result: every model of LA has an end extension to a model of \(\Sigma^{p}_{0}\). The article concludes with results concerning the relative strength of \(\Sigma^{p}_{0}\)-rec and \(\Sigma^{p}_{0}\)-(rec+choice).