Switch to: Citations

References in:

Realisability in weak systems of explicit mathematics

Daria Spescha & Thomas Strahm

Mathematical Logic Quarterly 57 (6):551-565 (2011)

Add references

You must login to add references.

The provably terminating operations of the subsystem of explicit mathematics.Dieter Probst - 2011 - Annals of Pure and Applied Logic 162 (11):934-947.details 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. (shrink) Download Export citation Bookmark 4 citations
Polytime, combinatory logic and positive safe induction.Cantini Andrea - 2002 - Archive for Mathematical Logic 41 (2):169-189.details We characterize the polynomial time operations as those which are provably total in a first order system, which comprises (untyped) combinatory logic with extensionality, together with positive “safe induction” on the set of binary strings. The formalization of safe induction is inspired by Leivants idea of ramification. We also show how to replace ramification by means of modal logic. Download Export citation Bookmark 6 citations
Elementary explicit types and polynomial time operations.Daria Spescha & Thomas Strahm - 2009 - Mathematical Logic Quarterly 55 (3):245-258.details 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]. Download Export citation Bookmark 5 citations
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.details This paper is mainly concerned with proof-theoretic analysis of some second-order systems of explicit mathematics with a non-constructive minimum operator. By introducing axioms for variable types we extend our first-order theory BON to the elementary explicit type theory EET and add several forms of induction as well as axioms for μ. The principal results then state: EET plus set induction is proof-theoretically equivalent to Peano arithmetic PA <0). Download Export citation Bookmark 28 citations

1