The provably terminating operations of the subsystem PETJ of explicit mathematics
type: Item
instance of: scholarly article
title: The provably terminating operations of the subsystem PETJ of explicit mathematics
zbMATH Open document ID: 1238.03039
author: Juan-Miguel Gracia
published in: Annals of Pure and Applied Logic
publication date: 2011-09-22T00:00:00Z
review text: The paper is devoted to the study of a system PET of explicit mathematics introduced by \textit{D. Spescha} and \textit{T. Strahm} in [Math. Log. Q. 55, No. 3, 245--258 (2009; Zbl 1171.03036)] and of a system PETJ obtained by adding the join principle. In particular the author discusses the problem whether the provably terminating operations of PETJ with classical logic are the polytime functions on binary words (what is the case if the logic is intuitionistic). In the paper a proof of this is supplemented.
reviewed by: Roman Murawski
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 03D75
zbMATH DE Number: 5949202
zbMATH Keywords: explicit mathematics
zbMATH Keywords: polytime functions
zbMATH Keywords: nonstandard models
MaRDI profile type: Publication
full work available at URL: j.apal.2011.04.004
OpenAlex ID: W2044649998
cites work: Q3679172
cites work: Q3757915
cites work: Polytime, combinatory logic and positive safe induction
cites work: Q5702663
cites work: Q5586401
cites work: Q4128540
cites work: Generalized recursion theory II. Proceedings of the 1977 Oslo Symposium
cites work: Q3882452
cites work: Q3487327
cites work: Q3773876
cites work: Variation on a theme of Schütte
cites work: Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
cites work: Elementary explicit types and polynomial time operations
cites work: Realisability in weak systems of explicit mathematics
cites work: Theories with self-application and computational complexity.
cites work: A proof-theoretic characterization of the basic feasible functionals
DOI: 10.1016/J.APAL.2011.04.004
description: scientific article; zbMATH DE number 5949202