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

In previous papers the author developed a method of extraction of primitive recursive bounds from ineffective analytic proofs. Here it is refined to obtain polynomial or Kalmar elementary bounds. A hierarchy \(G_nA^\omega\) of systems of classical arithmetic in all finite types is introduced whose definable objects of type \(0\to 0\) correspond to the Grzegorczyk hierarchy of primitive recursive functions. Main result: Bounds in corresponding Grzegorczyk classes can be extracted from proofs in \(G_nA^\omega+ (\text{quantifier-free choice})+\Gamma\), where \(\Gamma\) are suitable analytical axioms including a ``non-standard'' axiom \(F^-\) which does not hold in the full set-theoretical model but holds in strongly majorizable functionals. For \(n=2\) (corresponding to polynomial bounds) one can define sequences of real numbers, continuous functions, sin, cos etc., the supremum and Riemann integral of continuous functions of \([a,b]\), the restriction of the logarithm and exponential function on \([a,b]\). The system \(G_2A^\omega+\text{AC}-\text{QF}+ F^-\) allows short proofs of such theorems as: every continuous function on \([a,b]\) is uniformly continuous and attains its maximum sequential Heine-Borel property, Peano existence theorem for ordinary differential equations, Brouwer fixed point theorem, a generalization of binary König's lemma. The main tool for the extraction of bounds is a new monotone functional interpretation.