Elementary explicit types and polynomial time operations

&
Mathematical Logic Quarterly 55 (3):245-258 (2009)
  Copy   BIBTEX

Abstract

This paper studies systems of explicit mathematics as introduced by Feferman [9, 11]. In particular, we propose weak explicit type systems with a restricted form of elementary comprehension whose provably terminating operations coincide with the functions on binary words that are computable in polynomial time. The systems considered are natural extensions of the first-order applicative theories introduced in Strahm [19, 20]

Categories

Add categories

Keywords

Reprint years

DOI

10.1002/malq.200810004

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,127

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Review: Thomas Strahm, Polynomial Time Operations in Explicit Mathematics ; Andrea Cantini, Feasible Operations and Applicative Theories Based on $\lambda \eta $. [REVIEW]Fernando Ferreira - 2002 - Bulletin of Symbolic Logic 8 (4):534-535.
Realisability in weak systems of explicit mathematics.Daria Spescha & Thomas Strahm - 2011 - Mathematical Logic Quarterly 57 (6):551-565.
Polynomial time operations in explicit mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
The provably terminating operations of the subsystem of explicit mathematics.Dieter Probst - 2011 - Annals of Pure and Applied Logic 162 (11):934-947.
A theory of rules for enumerated classes of functions.Andreas Schlüter - 1995 - Archive for Mathematical Logic 34 (1):47-63.
Applicative theories for the polynomial hierarchy of time and its levels.Reinhard Kahle & Isabel Oitavem - 2013 - Annals of Pure and Applied Logic 164 (6):663-675.
On the proof theory of type two functionals based on primitive recursive operations.David Steiner & Thomas Strahm - 2006 - Mathematical Logic Quarterly 52 (3):237-252.
Power types in explicit mathematics?Gerhard Jäger - 1997 - Journal of Symbolic Logic 62 (4):1142-1146.
Systems of explicit mathematics with non-constructive μ-operator. Part II.Solomon Feferman & Gerhard Jäger - 1996 - Annals of Pure and Applied Logic 79 (1):37-52.
Extending the system T0 of explicit mathematics: the limit and Mahlo axioms.Gerhard Jäger & Thomas Studer - 2002 - Annals of Pure and Applied Logic 114 (1-3):79-101.

Analytics

Added to PP
2013-12-01

Downloads
26 (#631,520)

6 months
9 (#355,374)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

The provably terminating operations of the subsystem of explicit mathematics.Dieter Probst - 2011 - Annals of Pure and Applied Logic 162 (11):934-947.
Realisability in weak systems of explicit mathematics.Daria Spescha & Thomas Strahm - 2011 - Mathematical Logic Quarterly 57 (6):551-565.
A feasible theory of truth over combinatory algebra.Sebastian Eberhard - 2014 - Annals of Pure and Applied Logic 165 (5):1009-1033.
Admissible closures of polynomial time computable arithmetic.Dieter Probst & Thomas Strahm - 2011 - Archive for Mathematical Logic 50 (5):643-660.

Add more citations

References found in this work

Polytime, combinatory logic and positive safe induction.Cantini Andrea - 2002 - Archive for Mathematical Logic 41 (2):169-189.
Polynomial time operations in explicit mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
Feasible Operations and Applicative Theories Based on λη.Andrea Cantini - 2000 - Mathematical Logic Quarterly 46 (3):291-312.

Add more references