×

Some logical metatheorems with applications in functional analysis. (English) Zbl 1079.03046

Summary: 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.

MSC:

03F07 Structure of proofs
03F10 Functionals in proof theory
47H10 Fixed-point theorems
03F35 Second- and higher-order arithmetic and fragments
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Michael J. Beeson, Foundations of constructive mathematics, Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas (3)], vol. 6, Springer-Verlag, Berlin, 1985. Metamathematical studies. · Zbl 0565.03028
[2] Gianluigi Bellin, Ramsey interpreted: a parametric version of Ramsey’s theorem, Logic and computation (Pittsburgh, PA, 1987) Contemp. Math., vol. 106, Amer. Math. Soc., Providence, RI, 1990, pp. 17 – 37. · Zbl 0693.03035 · doi:10.1090/conm/106/1057813
[3] Marc Bezem, Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals, J. Symbolic Logic 50 (1985), no. 3, 652 – 660. · Zbl 0578.03030 · doi:10.2307/2274319
[4] Jonathan Borwein, Simeon Reich, and Itai Shafrir, Krasnosel\(^{\prime}\)ski-Mann iterations in normed spaces, Canad. Math. Bull. 35 (1992), no. 1, 21 – 28. · Zbl 0712.47050 · doi:10.4153/CMB-1992-003-0
[5] Martin R. Bridson and André Haefliger, Metric spaces of non-positive curvature, Grundlehren der Mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences], vol. 319, Springer-Verlag, Berlin, 1999. · Zbl 0988.53001
[6] F. E. Browder and W. V. Petryshyn, The solution by iteration of linear functional equations in Banach spaces, Bull. Amer. Math. Soc. 72 (1966), 566 – 570. , https://doi.org/10.1090/S0002-9904-1966-11543-4 F. E. Browder and W. V. Petryshyn, The solution by iteration of nonlinear functional equations in Banach spaces, Bull. Amer. Math. Soc. 72 (1966), 571 – 575. · Zbl 0138.08201
[7] F. Bruhat and J. Tits, Groupes réductifs sur un corps local, Inst. Hautes Études Sci. Publ. Math. 41 (1972), 5 – 251 (French). · Zbl 0254.14017
[8] Delzell, C., Kreisel’s unwinding of Artin’s proof-Part I. In: Odifreddi, P., Kreiseliana, 113-246, A K Peters, Wellesley, MA (1996). · Zbl 0876.12002
[9] Michael Edelstein and Richard C. O’Brien, Nonexpansive mappings, asymptotic regularity and successive approximations, J. London Math. Soc. (2) 17 (1978), no. 3, 547 – 554. · Zbl 0421.47031 · doi:10.1112/jlms/s2-17.3.547
[10] Wolfgang Friedrich, Spielquantorinterpretation unstetiger Funktionale der höheren Analysis, Arch. Math. Logik Grundlag. 24 (1984), no. 1-2, 73 – 99 (German). · Zbl 0544.03021 · doi:10.1007/BF02007142
[11] Wolfgang Friedrich, Gödelsche Funktionalinterpretation für eine Erweiterung der klassischen Analysis, Z. Math. Logik Grundlag. Math. 31 (1985), no. 1, 3 – 29 (German). · Zbl 0565.03021 · doi:10.1002/malq.19850310102
[12] Kazimierz Goebel and W. A. Kirk, Iteration processes for nonexpansive mappings, Topological methods in nonlinear functional analysis (Toronto, Ont., 1982) Contemp. Math., vol. 21, Amer. Math. Soc., Providence, RI, 1983, pp. 115 – 123. · Zbl 0525.47040 · doi:10.1090/conm/021/729507
[13] Kazimierz Goebel and Simeon Reich, Uniform convexity, hyperbolic geometry, and nonexpansive mappings, Monographs and Textbooks in Pure and Applied Mathematics, vol. 83, Marcel Dekker, Inc., New York, 1984. · Zbl 0537.46001
[14] Kurt Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica 12 (1958), 280 – 287 (German, with English summary). · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x
[15] Kurt Gödel, Collected works. Vol. II, The Clarendon Press, Oxford University Press, New York, 1990. Publications 1938 – 1974; Edited and with a preface by Solomon Feferman. · JFM 64.0020.05
[16] C. W. Groetsch, A note on segmenting Mann iterates, J. Math. Anal. Appl. 40 (1972), 369 – 372. · Zbl 0244.47042 · doi:10.1016/0022-247X(72)90056-X
[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). · Zbl 1026.46007
[18] W. A. Howard, Appendix: Hereditarily majorizable function of finite type, Metamathematical investigation of intuitionistic arithmetic and analysis, Springer, Berlin, 1973, pp. 454 – 461. Lecture Notes in Math., Vol. 344.
[19] W. A. Howard and G. Kreisel, Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis, J. Symbolic Logic 31 (1966), 325 – 358. · Zbl 0156.00804 · doi:10.2307/2270450
[20] Shiro Ishikawa, Fixed points and iteration of a nonexpansive mapping in a Banach space, Proc. Amer. Math. Soc. 59 (1976), no. 1, 65 – 71. · Zbl 0352.47024
[21] Shigeru Itoh, Some fixed-point theorems in metric spaces, Fund. Math. 102 (1979), no. 2, 109 – 117. · Zbl 0412.54054
[22] W. A. Kirk, Krasnosel\(^{\prime}\)skiĭ’s iteration process in hyperbolic space, Numer. Funct. Anal. Optim. 4 (1981/82), no. 4, 371 – 381. · Zbl 0505.47046 · doi:10.1080/01630568208816123
[23] W. A. Kirk, Nonexpansive mappings and asymptotic regularity, Nonlinear Anal. 40 (2000), no. 1-8, Ser. A: Theory Methods, 323 – 332. Lakshmikantham’s legacy: a tribute on his 75th birthday. · Zbl 1018.47040 · doi:10.1016/S0362-546X(00)85019-1
[24] Kirk, W.A., Geodesic geometry and fixed point theory. Preprint 23pp. (2003). · Zbl 1058.53061
[25] W. A. Kirk and Carlos Martínez-Yañez, Approximate fixed points for nonexpansive mappings in uniformly convex spaces, Ann. Polon. Math. 51 (1990), 189 – 193. · Zbl 0734.47032
[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). · Zbl 0744.03056
[27] Ulrich Kohlenbach, Pointwise hereditary majorization and some applications, Arch. Math. Logic 31 (1992), no. 4, 227 – 241. · Zbl 0729.03031 · doi:10.1007/BF01794980
[28] Ulrich Kohlenbach, Effective moduli from ineffective uniqueness proofs. An unwinding of de la Vallée Poussin’s proof for Chebycheff approximation, Ann. Pure Appl. Logic 64 (1993), no. 1, 27 – 94. · Zbl 0795.03086 · doi:10.1016/0168-0072(93)90213-W
[29] Ulrich Kohlenbach, 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. Optim. 14 (1993), no. 5-6, 581 – 606. · Zbl 0795.41020 · doi:10.1080/01630569308816541
[30] Ulrich Kohlenbach, Analysing proofs in analysis, Logic: from foundations to applications (Staffordshire, 1993) Oxford Sci. Publ., Oxford Univ. Press, New York, 1996, pp. 225 – 260. · Zbl 0881.03032
[31] Ulrich Kohlenbach, Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals, Arch. Math. Logic 36 (1996), no. 1, 31 – 71. · Zbl 0882.03050 · doi:10.1007/s001530050055
[32] Ulrich Kohlenbach, Arithmetizing proofs in analysis, Logic Colloquium ’96 (San Sebastián), Lecture Notes Logic, vol. 12, Springer, Berlin, 1998, pp. 115 – 158. · Zbl 0919.03046 · doi:10.1007/978-3-662-22110-5_5
[33] Ulrich Kohlenbach, A note on Spector’s quantifier-free rule of extensionality, Arch. Math. Logic 40 (2001), no. 2, 89 – 92. · Zbl 0980.03058 · doi:10.1007/s001530000048
[34] Ulrich Kohlenbach, On the computational content of the Krasnoselski and Ishikawa fixed point theorems, Computability and complexity in analysis (Swansea, 2000) Lecture Notes in Comput. Sci., vol. 2064, Springer, Berlin, 2001, pp. 119 – 145. · Zbl 0985.03048 · doi:10.1007/3-540-45335-0_9
[35] Ulrich Kohlenbach, A quantitative version of a theorem due to Borwein-Reich-Shafrir, Numer. Funct. Anal. Optim. 22 (2001), no. 5-6, 641 – 656. · Zbl 1001.47035 · doi:10.1081/NFA-100105311
[36] Kohlenbach, U., Uniform asymptotic regularity for Mann iterates. J. Math. Anal. Appl. 279, pp. 531-544 (2003). · Zbl 1043.47045
[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). · Zbl 1038.47037
[38] Kohlenbach, U., Oliva, P., Effective bounds on strong unicity in \(L_1\)-approximation. Ann. Pure Appl. Logic 121, pp. 1-38 (2003). · Zbl 1026.03040
[39] Kohlenbach, U., Oliva, P., Proof mining: a systematic way of analysing proofs in mathematics. Proc. Steklov Inst. Math. 242, pp. 136-164 (2003). · Zbl 1079.03045
[40] Krasnoselski, M. A., Two remarks on the method of successive approximation. Usp. Math. Nauk (N.S.) 10, pp. 123-127 (1955) (Russian).
[41] G. Kreisel, Finiteness theorems in arithmetic: an application of Herbrand’s theorem for \Sigma \(_{2}\)-formulas, Proceedings of the Herbrand symposium (Marseilles, 1981) Stud. Logic Found. Math., vol. 107, North-Holland, Amsterdam, 1982, pp. 39 – 55. · doi:10.1016/S0049-237X(08)71876-7
[42] G. Kreisel, Proof theory and the synthesis of programs: potential and limitations, EUROCAL ’85, Vol. 1 (Linz, 1985) Lecture Notes in Comput. Sci., vol. 203, Springer, Berlin, 1985, pp. 136 – 150. · doi:10.1007/3-540-15983-5_12
[43] G. Kreisel and A. Macintyre, Constructive logic versus algebraization. I, The L. E. J. Brouwer Centenary Symposium (Noordwijkerhout, 1981) Stud. Logic Found. Math., vol. 110, North-Holland, Amsterdam, 1982, pp. 217 – 260. · Zbl 0522.03046 · doi:10.1016/S0049-237X(09)70130-2
[44] Horst Luckhardt, Extensional Gödel functional interpretation. A consistency proof of classical analysis, Lecture Notes in Mathematics, Vol. 306, Springer-Verlag, Berlin-New York, 1973. · Zbl 0262.02031
[45] H. Luckhardt, Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken, J. Symbolic Logic 54 (1989), no. 1, 234 – 263 (German, with English summary). · Zbl 0669.03024 · doi:10.2307/2275028
[46] Luckhardt, H., Bounds extracted by Kreisel from ineffective proofs. In: Odifreddi, P., Kreiseliana, 289-300, A K Peters, Wellesley, MA (1996). · Zbl 0896.03005
[47] Hilton Vieira Machado, A characterization of convex subsets of normed spaces, Kōdai Math. Sem. Rep. 25 (1973), 307 – 320. · Zbl 0271.54021
[48] Mann, W.R., Mean value methods in iteration. Proc. Amer. Math. Soc. 4, pp. 506-510 (1953). · Zbl 0050.11603
[49] Simeon Reich and Itai Shafrir, Nonexpansive iterations in hyperbolic spaces, Nonlinear Anal. 15 (1990), no. 6, 537 – 558. · Zbl 0728.47043 · doi:10.1016/0362-546X(90)90058-O
[50] Simeon Reich and Alexander J. Zaslavski, Generic aspects of metric fixed point theory, Handbook of metric fixed point theory, Kluwer Acad. Publ., Dordrecht, 2001, pp. 557 – 575. · Zbl 1016.54021 · doi:10.1007/978-94-017-1748-9_16
[51] Stephen G. Simpson, Subsystems of second order arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1999. · Zbl 0909.03048
[52] Clifford Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, Proc. Sympos. Pure Math., Vol. V, American Mathematical Society, Providence, R.I., 1962, pp. 1 – 27. · Zbl 0143.25502
[53] Wataru Takahashi, A convexity in metric space and nonexpansive mappings. I, Kōdai Math. Sem. Rep. 22 (1970), 142 – 149. · Zbl 0268.54048
[54] A. S. Troelstra , Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, Vol. 344, Springer-Verlag, Berlin-New York, 1973. · Zbl 0275.02025
[55] Joachim Weidmann, Linear operators in Hilbert spaces, Graduate Texts in Mathematics, vol. 68, Springer-Verlag, New York-Berlin, 1980. Translated from the German by Joseph Szücs. · Zbl 0434.47001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.