Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
From MaRDI portal
Publication:1354332
DOI10.1007/s001530050055zbMath0882.03050OpenAlexW1973185693MaRDI 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 interpretationpolynomial boundsGrzegorczyk hierarchyextraction of bounds from ineffective analytic proofshierarchy of systems of classical arithmeticKalmar elementary boundsshort proofs
Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Proof theory in general (including proof-theoretic semantics) (03F03) Higher-type and set recursion theory (03D65)
Related Items
Relative constructivity, Light monotone Dialectica methods for proof mining, Term extraction and Ramsey's theorem for pairs, Some logical metatheorems with applications in functional analysis, Bounded functional interpretation and feasible analysis, Fluctuations, effective learnability and metastability in analysis, Primitive recursion and the chain antichain principle, Things that can and things that cannot be done in PRA, A Logical Uniform Boundedness Principle for Abstract Metric and Hyperbolic Spaces, Bounded functional interpretation, A complexity analysis of functional interpretations, On Tao's “finitary” infinite pigeonhole principle, On uniform weak König's lemma, Injecting uniformities into Peano arithmetic, Bounded modified realizability, On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness, Classical provability of uniform versions and intuitionistic provability, Nonstandardness and the bounded functional interpretation, Saturated models of universal theories, Groundwork for weak analysis