The provably terminating operations of the subsystem PETJ of explicit mathematics (Q639690)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The provably terminating operations of the subsystem PETJ of explicit mathematics |
scientific article |
Statements
The provably terminating operations of the subsystem PETJ of explicit mathematics (English)
0 references
22 September 2011
0 references
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.
0 references
explicit mathematics
0 references
polytime functions
0 references
nonstandard models
0 references
0 references