JournalspmVol. 70, No. 4pp. 295–318

Bounded theories for polyspace computability

  • Ricardo Bianconi

    Universidade de São Paulo, Brazil
  • Gilda Ferreira

    Universidade Lusófona de Humanidades e Tecnologias, Lisboa, Portugal
  • Emmanuel Silva

    Tribunal Regional Federal da 5ª Região, Recife, Brazil
Bounded theories for polyspace computability cover
Download PDF


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 PTCA\mathsf{PTCA}, Σ1b-NIA\mathsf{\Sigma^{b}_1}\textbf{-}\mathsf{NIA} and BTFA\mathsf{BTFA} in the polytime framework, we propose analogue theories concerning polyspace computability. Since the techniques we employ in the characterization of PSPACE\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 PTIME\mathsf{PTIME} to PSPACE\mathsf{PSPACE}.

Cite this article

Ricardo Bianconi, Gilda Ferreira, Emmanuel Silva, Bounded theories for polyspace computability. Port. Math. 70 (2013), no. 4, pp. 295–318

DOI 10.4171/PM/1936