Portugaliae Mathematica
Full-Text PDF (193 KB) | Metadata |
Table of Contents | PM summary
Bounded theories for polyspace computability
Ricardo Bianconi[1], Gilda Ferreira[2] and Emmanuel Silva[3] (1) Instituto de Matemática e Estatística, Universidade de São Paulo, Rua do Matão, 1010, SP 05508-900, São Paulo, Brazil(2) Departamento de Matemática, Universidade Lusófona de Humanidades e Tecnologias, Av. do Campo Grande, 376, 1749-024, Lisboa, Portugal
(3) Tribunal Regional Federal da 5ª Região, Cais do Apolo, s/n – Bairro do Recife, CEP 50030-908, Recife, Brazil
We present theories of bounded arithmetic and weak analysis whose provably total functions (with appropriate graphs) are the polyspace computable functions. More precisely, inspired in Ferreira’s systems $\mathsf{PTCA}$, $\mathsf{\Sigma^{b}_1}\textbf{-}\mathsf{NIA}$ and $\mathsf{BTFA}$ in the polytime framework, we propose analogue theories concerning polyspace computability. Since the techniques we employ in the characterization of $\mathsf{PSPACE}$ via formal systems (e.g. Herbrand’s theorem, cut-elimination theorem and the expansion of models) are similar to the ones involved in the polytime setting, we focus on what is specific of polyspace and explains the lift from $\mathsf{PTIME}$ to $\mathsf{PSPACE}$.
Keywords: Bounded arithmetic, weak analysis, polyspace computability, conservation results, cut-elimination
Bianconi Ricardo, Ferreira Gilda, Silva Emmanuel: Bounded theories for polyspace computability. Port. Math. 70 (2013), 295-318. doi: 10.4171/PM/1936