Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals

DOI10.1007/s001530050055zbMath0882.03050MaRDI QIDQ1354332

Ulrich Kohlenbach

Publication date: 12 March 1998

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s001530050055

zbMATH Keywords

monotone functional interpretation; polynomial bounds; Grzegorczyk hierarchy; extraction of bounds from ineffective analytic proofs; hierarchy of systems of classical arithmetic; Kalmar elementary bounds; short proofs

Mathematics Subject Classification ID

03F10: Functionals in proof theory

03F35: Second- and higher-order arithmetic and fragments

03F03: Proof theory in general (including proof-theoretic semantics)

03D65: Higher-type and set recursion theory

Related Items

Some logical metatheorems with applications in functional analysis, A Logical Uniform Boundedness Principle for Abstract Metric and Hyperbolic Spaces, On Tao's “finitary” infinite pigeonhole principle, Classical provability of uniform versions and intuitionistic provability, Bounded modified realizability, On uniform weak König's lemma, Fluctuations, effective learnability and metastability in analysis, Primitive recursion and the chain antichain principle, A complexity analysis of functional interpretations, Bounded functional interpretation and feasible analysis, Injecting uniformities into Peano arithmetic, On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness, Saturated models of universal theories, Things that can and things that cannot be done in PRA, Nonstandardness and the bounded functional interpretation, Bounded functional interpretation, Term extraction and Ramsey's theorem for pairs, Groundwork for weak analysis, Light monotone Dialectica methods for proof mining, Relative constructivity