Arithmetizing proofs in analysis
Ulrich Kohlenbach · Cambridge University Press eBooks · 2017
this paper we continue our investigations started in [15] and [16] on the question: What is the impact on the growth of extractable uniform bounds the use of various analytical principles \\Gamma in a given proof of an 89--sentence might have? To be more specific, we are interested in analyzing proofs of sentences having the form (1) 8u 1 ; k 0 8v ae tuk9w 0 A 0 (u; k; v; w); where A 0 is a quantifier--free formula 1 (containing only u; k; v; w as free variables) in the language of a suitable subsystem T ! of arithmetic in all finite types, t is a closed term and ae is defined pointwise (ae being an arbitrary finite type). From a proof of (1) carried out in T ! one can extract an effective uniform bound \\Phiuk on 9w, i.e. (2) 8u 1 ; k 0 8v ae tuk9w 0 \\Phiuk A 0 (u; k; v; w); where the complexity (and in particular the growth) of \\Phi is limited by the complexity of the system T ! (see [13],[15]). By the predicate `uniform' we refer to the fact that the bound \\Phi does not depend on v ae tuk