Remote Access Transactions of the American Mathematical Society
Green Open Access

Transactions of the American Mathematical Society

ISSN 1088-6850(online) ISSN 0002-9947(print)



Some logical metatheorems with applications in functional analysis

Author: Ulrich Kohlenbach
Journal: Trans. Amer. Math. Soc. 357 (2005), 89-128
MSC (2000): Primary 03F10, 03F35, 47H09, 47H10
Published electronically: January 29, 2004
MathSciNet review: 2098088
Full-text PDF

Abstract | References | Similar Articles | Additional Information

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.

References [Enhancements On Off] (What's this?)

  • 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 $L_1$-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

Similar Articles

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

Retrieve articles in all journals with MSC (2000): 03F10, 03F35, 47H09, 47H10

Additional Information

Ulrich Kohlenbach
Affiliation: Department of Computer Science, University of Aarhus, Ny Munkegade, DK-8000 Aarhus C, Denmark

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
Published electronically: 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
Article copyright: © Copyright 2004 American Mathematical Society

American Mathematical Society