Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
type: Item
instance of: scholarly article
title: Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
zbMATH Open document ID: 0882.03050
author: Ulrich Kohlenbach
published in: Archive for Mathematical Logic
publication date: 1998-03-12T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03D65
Mathematics Subject Classification ID: 03F10
Mathematics Subject Classification ID: 03F35
zbMATH DE Number: 1006568
zbMATH Keywords: extraction of bounds from ineffective analytic proofs
zbMATH Keywords: hierarchy of systems of classical arithmetic
zbMATH Keywords: Kalmar elementary bounds
zbMATH Keywords: Grzegorczyk hierarchy
zbMATH Keywords: polynomial bounds
zbMATH Keywords: short proofs
zbMATH Keywords: monotone functional interpretation
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: s001530050055
OpenAlex ID: W1973185693
DOI: 10.1007/S001530050055
Recommended article: On the weak convergence of subordinated systems
Recommended article: Strong differential subordination and superordination of analytic functions
Recommended article: Q4536867
Recommended article: Iterated function systems of finite type and the weak separation property
Recommended article: Strongly subharmonic functions, graphs, and their asymptotic growth
Recommended article: Strong submeasures and applications to non-compact dynamical systems
Recommended article: Growth and Asymptotic Sets of Subharmonic Functions
Recommended article: Subexponential growth rates in functional differential equations
Recommended article: Q4876432
description: scientific article; zbMATH DE number 1006568