Transactions of the American Mathematical Society

Author(s): Ulrich Kohlenbach
Journal: Trans. Amer. Math. Soc. 357 (2005), 89-128.
MSC (2000): Primary 03F10, 03F35, 47H09, 47H10
Posted: January 29, 2004
Retrieve article in: PDF DVI PostScript

Abstract: In previous papers we have developed proof-theoretic techniques for extracting effective uniform bounds from large classes of ineffective existence proofs in functional analysis. Here `uniform' means independence from parameters in compact spaces. A recent case study in fixed point theory systematically yielded uniformity even w.r.t. parameters in metrically bounded (but noncompact) subsets which had been known before only in special cases. In the present paper we prove general logical metatheorems which cover these applications to fixed point theory as special cases but are not restricted to this area at all. Our theorems guarantee under general logical conditions such strong uniform versions of non-uniform existence statements. Moreover, they provide algorithms for actually extracting effective uniform bounds and transforming the original proof into one for the stronger uniformity result. Our metatheorems deal with general classes of spaces like metric spaces, hyperbolic spaces, CAT(0)-spaces, normed linear spaces, uniformly convex spaces, as well as inner product spaces.

1.: Beeson, M., Foundations of constructive mathematics. Springer Verlag, Berlin, Heidelberg, New York (1985). MR 86k:03055
2.: Bellin, G., Ramsey interpreted: a parametric version of Ramsey's theorem. In: Logic and computation (Pittsburgh, PA, 1987), pp. 17-37, Contemp. Math., 106, Amer. Math. Soc., Providence, RI (1990). MR 91i:03106
3.: Bezem, M.A., Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals. J. Symb. Logic 50 pp. 652-660 (1985). MR 87c:03139
4.: Borwein, J., Reich, S., Shafrir, I., Krasnoselski-Mann iterations in normed spaces. Canad. Math. Bull. 35, pp. 21-28 (1992). MR 93e:47072
5.: Bridson, M.R., Haefliger, A., Metric spaces of non-positive curvature. Springer Verlag, Berlin (1999). MR 2000k:53038
6.: Browder, F.E., Petryshyn, W.V., The solution by iteration of nonlinear functional equations in Banach spaces. Bull. Amer. Math. Soc. 72, pp. 571-575 (1966). MR 32:8155b
7.: Bruhat, F., Tits, J., Groupes réductifs sur un corps local. I. Données radicielles valuées. Inst. Hautes Études Sci. Publ. Math. 41, pp. 5-251 (1972). MR 48:6265
8.: Delzell, C., Kreisel's unwinding of Artin's proof-Part I. In: Odifreddi, P., Kreiseliana, 113-246, A K Peters, Wellesley, MA (1996).
9.: Edelstein, M., O'Brien, R.C., Nonexpansive mappings, asymptotic regularity and successive approximations. J. London Math. Soc. 17, pp. 547-554 (1978). MR 80b:47074
10.: Friedrich, W., Spielquantorinterpretation unstetiger Funktionale der höheren Analysis. Arch. math. Logik 24, pp. 73-99 (1984). MR 86c:03052
11.: Friedrich, W., Gödelsche Funktionalinterpretation für eine Erweiterung der klassischen Analysis. Zeitschr. f. math. Logik und Grundl. d. Math. 31, pp. 3-29 (1985). MR 87b:03132
12.: Goebel, K., Kirk, W.A., Iteration processes for nonexpansive mappings. In: Singh, S.P., Thomeier, S., Watson, B., eds., Topological Methods in Nonlinear Functional Analysis. Contemporary Mathematics 21, AMS, pp. 115-123 (1983). MR 85a:47059
13.: Goebel, K., Reich, S., Uniform convexity, hyperbolic geometry, and nonexpansive mappings. Monographs and Textbooks in Pure and Applied Mathematics, 83. Marcel Dekker, Inc., New York, ix+170 pp. (1984). MR 86d:58012
14.: Gödel, K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12, pp. 280-287 (1958). MR 21:1275
15.: Gödel, K., Collected Work, Vol.2, S. Feferman et al. eds. Oxford University Press, New York (1990). MR 91b:01093
16.: Groetsch, C.W., A note on segmenting Mann iterates. J. of Math. Anal. Appl. 40, pp. 369-372 (1972). MR 49:5954
17.: Henson, C.W., Iovino, J., Ultraproducts in analysis. In: Analysis and Logic. London Mathematical Society LNS 262, pp. 1-112. Cambridge University Press (2002).
18.: Howard, W.A., Hereditarily majorizable functionals of finite type. In: Troelstra (ed.), Metamathematical investigation of intuitionistic arithmetic and analysis, pp. 454-461. Springer LNM 344 (1973). MR 57:9493
19.: Howard, W.A., Kreisel, G., Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. J. Symbolic Logic 31, pp. 325-358 (1966). MR 35:27
20.: Ishikawa, S., Fixed points and iterations of a nonexpansive mapping in a Banach space. Proc. Amer. Math. Soc. 59, pp. 65-71 (1976). MR 54:1030
21.: Itoh, S., Some fixed point theorems in metric spaces. Fund. Math. 102, pp. 109-117 (1979). MR 80h:54058
22.: Kirk, W.A., Krasnosel'skii iteration process in hyperbolic spaces, Numer. Funct. Anal. and Optimiz. 4, pp. 371-381 (1982). MR 84e:47067
23.: Kirk, W.A., Nonexpansive mappings and asymptotic regularity, Nonlinear Analysis, 40, pp. 323-332 (2000). MR 2001m:47116
24.: Kirk, W.A., Geodesic geometry and fixed point theory. Preprint 23pp. (2003).
25.: Kirk, W.A., Martinez-Yanez, C., Approximate fixed points for nonexpansive mappings in uniformly convex spaces. Annales Polonici Mathematici 51, pp. 189-193 (1990). MR 92a:47068
26.: Kohlenbach, U., Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: Effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Beweisen. Ph.D. Thesis, Frankfurt am Main, xxii+278pp. (1990).
27.: Kohlenbach, U., Pointwise hereditary majorization and some applications. Arch. Math. Logic 31, pp. 227-241 (1992). MR 93b:03106
28.: Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation. Ann. Pure Appl. Logic 64, pp. 27-94 (1993). MR 95b:03061
29.: Kohlenbach, U., New effective moduli of uniqueness and uniform a-priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Numer. Funct. Anal. and Optimiz. 14, pp. 581-606 (1993). MR 94k:41054
30.: Kohlenbach, U., Analysing proofs in analysis. In: W. Hodges, M. Hyland, C. Steinhorn, J. Truss, editors, Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993), pp. 225-260, Oxford University Press (1996). MR 98b:03085
31.: Kohlenbach, U., Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals. Arch. Math. Logic 36, pp. 31-71 (1996). MR 98h:03073
32.: Kohlenbach, U., Arithmetizing proofs in analysis. In: Larrazabal, J.M., Lascar, D., Mints, G. (eds.), Logic Colloquium '96, Springer Lecture Notes in Logic 12, pp. 115-158 (1998). MR 2000j:03085
33.: Kohlenbach, U., A note on Spector's quantifier-free rule of extensionality. Arch. Math. Logic 40, pp. 89-92 (2001). MR 2001m:03121
34.: Kohlenbach, U., On the computational content of the Krasnoselski and Ishikawa fixed point theorems. In: Proceedings of the Fourth Workshop on Computability and Complexity in Analysis, J. Blanck, V. Brattka, P. Hertling (eds.), Springer LNCS 2064, pp. 119-145 (2001). MR 2003b:47090
35.: Kohlenbach, U., A quantitative version of a theorem due to Borwein-Reich-Shafrir. Numer. Funct. Anal. and Optimiz. 22, pp. 641-656 (2001). MR 2002i:47076
36.: Kohlenbach, U., Uniform asymptotic regularity for Mann iterates. J. Math. Anal. Appl. 279, pp. 531-544 (2003).
37.: Kohlenbach, U., Leu¸stean, L., Mann iterates of directionally nonexpansive mappings in hyperbolic spaces. Abstract and Applied Analysis, vol. 2003, issue 8, pp. 449-477 (2003).
38.: Kohlenbach, U., Oliva, P., Effective bounds on strong unicity in -approximation. Ann. Pure Appl. Logic 121, pp. 1-38 (2003).
39.: Kohlenbach, U., Oliva, P., Proof mining: a systematic way of analysing proofs in mathematics. Proc. Steklov Inst. Math. 242, pp. 136-164 (2003).
40.: Krasnoselski, M. A., Two remarks on the method of successive approximation. Usp. Math. Nauk (N.S.) 10, pp. 123-127 (1955) (Russian). MR 16:833a
41.: Kreisel, G., Finiteness theorems in arithmetic: an application of Herbrand's theorem for $\Sigma_2$ -formulas. Proc. of the Herbrand symposium (Marseille, 1981), North-Holland (Amsterdam), pp. 39-55 (1982). MR 86b:03076
42.: Kreisel, G., Proof Theory and Synthesis of Programs: Potentials and Limitations. Eurocal '85 (Linz 1985), Springer LNCS 203, pp. 136-150 (1986). MR 87e:03156
43.: Kreisel, G., Macintyre, A., Constructive logic versus algebraization I. Proc. L.E.J. Brouwer Centenary Symposium (Noordwijkerhout 1981), North-Holland (Amsterdam), pp. 217-260 (1982). MR 85j:03108
44.: Luckhardt, H., Extensional Gödel Functional Interpretation. Springer Lecture Notes in Mathematics 306 (1973). MR 49:2281
45.: Luckhardt, H., Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. J. Symbolic Logic 54, pp. 234-263 (1989). MR 90k:03056
46.: Luckhardt, H., Bounds extracted by Kreisel from ineffective proofs. In: Odifreddi, P., Kreiseliana, 289-300, A K Peters, Wellesley, MA (1996).
47.: Machado, H.V., A characterization of convex subsets of normed spaces. Kodai Math. Sem. Rep. 25, pp. 307-320 (1973). MR 48:4703
48.: Mann, W.R., Mean value methods in iteration. Proc. Amer. Math. Soc. 4, pp. 506-510 (1953). MR 14:988f
49.: Reich, S., Shafrir, I., Nonexpansive iterations in hyperbolic spaces. Nonlinear Analysis, Theory, Methods and Applications 15, pp. 537-558 (1990). MR 91k:47135
50.: Reich, S., Zaslavski, A.J., Generic aspects of metric fixed point theory In: W. A. Kirk, B. Sims, editors, Handbook of Metric Fixed Point Theory, Kluwer Academic Publishers, pp. 557-576 (2001). MR 2003e:54048
51.: Simpson, S.G., Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag. xiv+445 pp. (1999). MR 2001i:03126
52.: Spector, C., Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In: Recursive function theory, Proceedings of Symposia in Pure Mathematics, vol. 5 (J.C.E. Dekker (ed.)), AMS, Providence, R.I., pp. 1-27 (1962). MR 27:4745
53.: Takahashi, W., A convexity in metric space and nonexpansive mappings, I. Kodai Math. Sem. Rep. 22, pp. 142-149 (1970). MR 42:2467
54.: Troelstra, A.S. (ed.), Metamathematical investigation of intuitionistic arithmetic and analysis. Springer Lecture Notes in Mathematics 344 (1973). MR 48:3699
55.: Weidmann, J., Linear operators in Hilbert spaces. Springer Graduate Texts in Mathematics 68, xii+402 pp. (1980). MR 81e:47001

Retrieve articles in Transactions of the American Mathematical Society with MSC (2000): 03F10, 03F35, 47H09, 47H10

Ulrich Kohlenbach
Affiliation: Department of Computer Science, University of Aarhus, Ny Munkegade, DK-8000 Aarhus C, Denmark
Email: kohlenb@brics.dk

DOI: 10.1090/S0002-9947-04-03515-9
PII: S 0002-9947(04)03515-9
Keywords: Proof mining, functionals of finite type, convex analysis, fixed point theory, nonexpansive mappings, hyperbolic spaces, CAT(0)-spaces
Received by editor(s): May 12, 2003
Posted: January 29, 2004
Additional Notes: The author was partially supported by the Danish Natural Science Research Council, Grant no. 21-02-0474, and BRICS, Basic Research in Computer Science, funded by the Danish National Research Foundation
Copyright of article: Copyright 2004, American Mathematical Society

			Journals Home Search Author Info Subscribe Tech Support Help
ISSN 1088-6850(e) ISSN 0002-9947(p)

Previous issue \| Table of contents \| Next issue Articles in press \| Recently posted articles \| Most recent issue \| All issues Previous Article \| Next Article


	Comments: webmaster@ams.org © Copyright 2008, American Mathematical Society Privacy Statement		Search the AMS