Bounded theories for polyspace computability

Bianconi, Ricardo; Ferreira, Gilda; Silva, Emmanuel

http://hdl.handle.net/10400.2/10487

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
PSPACE.pdf		129.15 KB	Adobe PDF	Download

Send Feedback

Authors

Bianconi, Ricardo

Ferreira, Gilda

Silva, Emmanuel

Abstract(s)

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, Sigma^b_1-NIA and BTFA in the polytime framework, we propose analogue theories concerning polyspace computability. Since the techniques we employ in the characterization of 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 to PSPACE.