The EMS Publishing House is now EMS Press and has its new home at

Please find all EMS Press journals and articles on the new platform.

Portugaliae Mathematica

Full-Text PDF (193 KB) | Metadata | Table of Contents | PM summary
Online access to the full text of Portugaliae Mathematica is restricted to the subscribers of the journal, who are encouraged to communicate their IP-address(es) to their agent or directly to the publisher at
Volume 70, Issue 4, 2013, pp. 295–318
DOI: 10.4171/PM/1936

Published online: 2013-12-31

Bounded theories for polyspace computability

Ricardo Bianconi[1], Gilda Ferreira[2] and Emmanuel Silva[3]

(1) Universidade de São Paulo, Brazil
(2) Universidade Lusófona de Humanidades e Tecnologias, Lisboa, Portugal
(3) Tribunal Regional Federal da 5ª Região, 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