Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals (Q1354332): Difference between revisions
From MaRDI portal
Changed an Item |
Set OpenAlex properties. |
||
(One intermediate revision by one other user not shown) | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/s001530050055 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1973185693 / rank | |||
Normal rank |
Latest revision as of 00:22, 20 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals |
scientific article |
Statements
Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals (English)
0 references
12 March 1998
0 references
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.
0 references
extraction of bounds from ineffective analytic proofs
0 references
hierarchy of systems of classical arithmetic
0 references
Kalmar elementary bounds
0 references
Grzegorczyk hierarchy
0 references
polynomial bounds
0 references
short proofs
0 references
monotone functional interpretation
0 references