Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
From MaRDI portal
Publication:1354332
DOI10.1007/s001530050055zbMath0882.03050MaRDI QIDQ1354332
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
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
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
