The provably terminating operations of the subsystem of explicit mathematics

Annals of Pure and Applied Logic 162 (11):934-947 (2011)
  Copy   BIBTEX

Abstract

In Spescha and Strahm [15], a system of explicit mathematics in the style of Feferman [6] and [7] is introduced, and in Spescha and Strahm [16] the addition of the join principle to is studied. Changing to intuitionistic logic, it could be shown that the provably terminating operations of are the polytime functions on binary words. However, although strongly conjectured, it remained open whether the same holds true for the corresponding theory with classical logic. This note supplements a proof of this conjecture

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2011.04.004

Links

PhilArchive



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

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

Elementary explicit types and polynomial time operations.Daria Spescha & Thomas Strahm - 2009 - Mathematical Logic Quarterly 55 (3):245-258.
Polynomial Time Operations in Explicit Mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
Polynomial time operations in explicit mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
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.
Thomas Strahm. Polynomial time operations in explicit mathematics. The journal of symbolic logic, vol. 62 , pp. 575–594. - Andrea Cantini. Feasible operations and applicative theories based on λη. Mathematical logic quarterly, vol. 46 , pp. 291–312. [REVIEW]Fernando Ferreira - 2002 - Bulletin of Symbolic Logic 8 (4):534-535.
Two papers by T. Strahm and by A. Cantini on explicit mathematics. [REVIEW]Fernando Ferreira - 2002 - Bulletin of Symbolic Logic 8 (4):534-534.
Systems of explicit mathematics with non-constructive μ-operator and join.Thomas Glaß & Thomas Strahm - 1996 - Annals of Pure and Applied Logic 82 (2):193-219.
Systems of explicit mathematics with non-constructive μ-operator. Part I.Solomon Feferman & Gerhard Jäger - 1993 - Annals of Pure and Applied Logic 65 (3):243-263.
On the impossibility of explicit upper bounds on lengths of some provably finite algorithms in computable analysis.Andre Scedrov - 1986 - Annals of Pure and Applied Logic 32:291-297.
On the proof-theoretic strength of monotone induction in explicit mathematics.Thomas Glass, Michael Rathjen & Andreas Schlüter - 1997 - Annals of Pure and Applied Logic 85 (1):1-46.

Analytics

Added to PP
2013-10-27

Downloads
168 (#23,393)

6 months
11 (#1,140,922)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

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

Add more citations

References found in this work

Elementary explicit types and polynomial time operations.Daria Spescha & Thomas Strahm - 2009 - Mathematical Logic Quarterly 55 (3):245-258.
Polytime, combinatory logic and positive safe induction.Cantini Andrea - 2002 - Archive for Mathematical Logic 41 (2):169-189.

View all 8 references / Add more references