Proof Mining: A~Systematic Way of Analyzing Proofs in Mathematics

U. Kohlenbach ; P. Oliva

Trudy Matematicheskogo Instituta imeni V.A. Steklova, Mathematical logic and algebra, Tome 242 (2003), pp. 147-175.

Résumé

Proof mining is the process of logically analyzing proofs in mathematics with the aim of obtaining new information. In this survey paper, we discuss, by means of examples from mathematics, some of the main techniques used in proof mining. We show that these techniques apply not only to proofs based on classical logic but also to proofs that involve noneffective principles such as the attainment of the infimum of $f\in C[0,1]$ and the convergence for bounded monotone sequences of reals. We also report on recent case studies in approximation theory and fixed point theory where new results were obtained.

Bibliographie

[1] Angelos J. R., Henry M. S., Kaufman E. H., Lenker T. D., Kroó A., “Local and global Lipschitz constants”, J. Approx. Theory, 46 (1986), 137–156 | DOI | MR | Zbl

[2] Angelos J. R., Kroó A., “The equivalence of the moduli of continuity of the best approximation operator and of strong unicity in $L^1$”, J. Approx. Theory, 46 (1986), 129–136 | DOI | MR | Zbl

[3] Avigad J., Feferman S., “Gödel's functional (“Dialectica”) interpretation”, Handbook of proof theory, Stud. Logic and Found. Math., 137, ed. S. R. Buss, North-Holland, Amsterdam, 1998, 337–405 | MR

[4] Baillon J., Bruck R. E., “The rate of asymptotic regularity is $O(\frac{1}{\sqrt{n}})$”, Theory and applications of nonlinear operators of accretive and monotone type, Lect. Notes Pure and Appl. Math., 178, M. Dekker, New York, 1996, 51–81 | MR | Zbl

[5] Bartelt M. W., Li W., “Error estimates and Lipschitz constants for best approximation in continuous function spaces”, Comput. and Math. Appl., 30:3–6 (1995), 255–268 | DOI | MR | Zbl

[6] Bartelt M. W., Schmidt D., “Lipschitz conditions, strong uniqueness, and almost Chebyshev subspaces of $C(x)$”, J. Approx. Theory, 40 (1984), 202–215 | DOI | MR | Zbl

[7] Beeson M. J., Foundations of constructive mathematics. Metamathematical studies, Springer, Berlin, 1985 | MR | Zbl

[8] Bellin G., “Ramsey interpreted: a parametric version of Ramsey's theorem”, Logic and computation (Pittsburgh, PA, 1987), Contemp. Math., 106, Amer. Math. Soc., Providence, RI, 1990, 17–37 | MR

[9] Berger U., Schwichtenberg H., Buchholz W., “Refined program extraction from classical proofs”, Ann. Pure and Appl. Logic, 114 (2002), 3–25 | DOI | MR | Zbl

[10] Bezem M., “Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals”, J. Symb. Logic, 50 (1985), 652–660 | DOI | MR | Zbl

[11] Bishop E., Foundations of constructive analysis, McGraw-Hill, New York, 1967 | MR | Zbl

[12] Bishop E., “Mathematics as a numerical language”, Intuitionism and proof theory, eds. A. Kino, J. Myhill, R. E. Vesley, North-Holland, Amsterdam, 1970, 53–71 | MR

[13] Björnestål B. O., Continuity of the metric projection operator. I–III, Prepr. Ser. Dept. Math., Roy. Inst. Technol. No 17, TRITA-MAT, Stockholm, 1975 | Zbl

[14] Björnestål B. O., “Local Lipschitz continuity of the metric projection operator”, Approximation theory, Banach Center Publ., 4, PWN, Warsaw, 1979, 43–53 | MR

[15] Borwein J., Reich S., Shafrir I., “Krasnoselski–Mann iterations in normed spaces”, Canad. Math. Bull., 35 (1992), 21–28 | MR | Zbl

[16] Bridges D. S., Richman F., Julian W. H., Mines R., “Extensions and fixed points of contractive maps in $R^n$”, J. Math. Anal. and Appl., 165:2 (1992), 438–456 | DOI | MR | Zbl

[17] Browder F. E., “Nonexpansive nonlinear operators in a Banach space”, Proc. Nat. Acad. Sci. USA, 54, 1965, 1041–1044 | MR | Zbl

[18] Browder F. E., Petryshyn W. V., “The solution by iteration of nonlinear functional equations in Banach spaces”, Bull. Amer. Math. Soc., 72 (1966), 571–575 | DOI | MR | Zbl

[19] Cheney E. W., “An elementary proof of Jackson's theorem on mean-approximations”, Math. Mag., 38 (1965), 189–191 | MR | Zbl

[20] Clarkson J. A., “Uniformly convex spaces”, Trans. Amer. Math. Soc., 40 (1936), 396–414 | DOI | MR | Zbl

[21] Collaço P., Carvalho e Silva J., “A complete comparison of 25 contraction conditions”, Nonlin. Anal., 30 (1997), 471–476 | DOI | MR | Zbl

[22] Delzell C., “Kreisel's unwinding of Artin's proof”, Kreiseliana: About and around Georg Kreisel, ed. P. Odifreddi, A. K. Peters, Wellesley, MA, 1996, 113–246 | MR | Zbl

[23] Edelstein M., “On fixed and periodic points under contractive mappings”, J. London Math. Soc., 37 (1962), 74–79 | DOI | MR | Zbl

[24] Edelstein M., O'Brien R. C., “Nonexpansive mappings, asymptotic regularity and successive approximations”, J. London Math. Soc., 17 (1978), 547–554 | DOI | MR | Zbl

[25] Engl H. W., Leitão A., “A Mann iterative regularization method for elliptic Cauchy problems”, Numer. Funct. Anal. and Optim., 22 (2001), 861–884 | DOI | MR | Zbl

[26] Feferman S., “Kreisel's ‘Unwinding Program’”, Kreiseliana: About and around Georg Kreisel, ed. P. Odifreddi, A. K. Peters, Wellesley, MA, 1996, 247–273 | MR | Zbl

[27] Girard J.-Y., Proof theory and logical complexity, Studies in Proof Theory, Bibliopolis, Naples, 1987 | MR | Zbl

[28] Gödel K., “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes”, Dialectica, 12 (1958), 280–287 | DOI | MR | Zbl

[29] Goebel K., Kirk W. A., “Iteration processes for nonexpansive mappings”, Topological methods in nonlinear functional analysis, Contemp. Math., 21, Amer. Math. Soc., Providence, RI, 1983, 115–123 | MR

[30] Goebel K., Kirk W. A., Topics in metric fixed point theory, Cambridge Stud. Adv. Math., 28, Cambridge Univ. Press, Cambridge, 1990 | MR | Zbl

[31] Goebel K., Reich S., Uniform convexity, hyperbolic geometry, and nonexpansive mappings, Monogr. and Textbooks Pure and Appl. Math., 83, M. Dekker, New York, 1984 | MR | Zbl

[32] Groetsch C. W., “A note on segmenting Mann iterates”, J. Math. Anal. and Appl., 40 (1972), 369–372 | DOI | MR | Zbl

[33] Howard W. A., “Hereditarily majorizable functionals of finite type”, Metamathematical investigation of intuitionistic arithmetic and analysis, Lect. Notes Math., 344, ed. A. S. Troelstra, Springer, Berlin, 1973, 454–461 | MR

[34] Howard W. A., “Ordinal analysis of simple cases of bar recursion”, J. Symb. Logic, 46 (1981), 17–30 | DOI | MR | Zbl

[35] Huotari R., Sahab S., “Strong unicity versus modulus of convexity”, Bull. Austral. Math. Soc., 49 (1994), 305–310 | DOI | MR | Zbl

[36] Ishikawa S., “Fixed points and iterations of a nonexpansive mapping in a Banach space”, Proc. Amer. Math. Soc., 59 (1976), 65–71 | DOI | MR | Zbl

[37] Jackson D., “Note on a class of polynomials of approximation”, Trans. Amer. Math. Soc., 22 (1921), 320–326 | DOI | MR | Zbl

[38] Kirk W. A., “Krasnoselski's iteration process in hyperbolic space”, Numer. Funct. Anal. and Optim., 4 (1982), 371–381 | DOI | MR | Zbl

[39] Kirk W. A., “Nonexpansive mappings and asymptotic regularity”, Nonlin. Anal., 40 (2000), 323–332 | DOI | MR | Zbl

[40] Kirk W. A., Martinez-Yañez C., “Approximate fixed points for nonexpansive mappings in uniformly convex spaces”, Ann. Pol. Math., 51 (1990), 189–193 | MR | Zbl

[41] Handbook of metric fixed point theory, eds. W.A. Kirk, B. Sims, Kluwer, Dordrecht, 2001 | MR

[42] Ko K.-I., Complexity theory of real functions, Birkhäuser, Boston, Basel, Berlin, 1991 | MR

[43] Kohlenbach U., Theory of majorizable and continuous functionals and their use for the extraction of bounds from nonconstructive proofs: effective moduli of uniqueness for best approximations from ineffective proofs of uniqueness, Ph.D. Thes., Univ. Frankfurt, Frankfurt, 1990, German, xxii+278 p | Zbl

[44] Kohlenbach U., “Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization”, J. Symb. Logic, 57 (1992), 1239–1273 | DOI | MR | Zbl

[45] Kohlenbach U., “Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation”, Ann. Pure and Appl. Logic, 64 (1993), 27–94 | DOI | MR | Zbl

[46] 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 Optim., 14 (1993), 581–606 | DOI | MR | Zbl

[47] Kohlenbach U., “Analysing proofs in analysis”, Logic: from foundations to applications, Europ. Logic Colloq. (Keele, 1993), eds. W. Hodges, M. Hyland, C. Steinhorn, J. Truss, Oxford Univ. Press, Oxford, 1996, 225–260 | MR | Zbl

[48] Kohlenbach U., “Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals”, Arch. Math. Logic, 36 (1996), 31–71 | DOI | MR | Zbl

[49] Kohlenbach U., “Arithmetizing proofs in analysis”, Lect. Notes Logic, 12, 1998, 115–158 | MR | Zbl

[50] Kohlenbach U., Proof theory and computational analysis, El. Notes Theor. Comput. Sci., 13, Elsevier, Amsterdam, 1998, 34 pp. | MR

[51] Kohlenbach U., “Relative constructivity”, J. Symb. Logic, 63 (1998), 1218–1238 | DOI | MR | Zbl

[52] Kohlenbach U., “On the no-counterexample interpretation”, J. Symb. Logic, 64 (1999), 1491–1511 | DOI | MR | Zbl

[53] Kohlenbach U., “The use of a logical principle of uniform boundedness in analysis”, Logic and foundations of mathematics, Synthese Library, 280, eds. A. Cantini, E. Casari, P. Minari, Kluwer, Dordrecht, 1999, 93–106 | MR | Zbl

[54] Kohlenbach U., “Things that can and things that can't be done in PRA”, Ann. Pure and Appl. Logic, 102 (2000), 223–245 | DOI | MR | Zbl

[55] Kohlenbach U., “On the computational content of the Krasnoselski and Ishikawa fixed point theorems”, Computability and complexity in analysis (CCA'2000), Lect. Notes Comput. Sci., 2064, eds. J. Blanck, V. Brattka, P. Hertling, Springer, Berlin, 2001, 119–145 | MR | Zbl

[56] Kohlenbach U., “A quantitative version of a theorem due to Borwein–Reich–Shafrir”, Numer. Funct. Anal. and Optim., 22 (2001), 641–656 | DOI | MR | Zbl

[57] Kohlenbach U., “Foundational and mathematical uses of higher types”, Reflections on the foundations of mathematics: Essay in honor of Solomon Feferman, Lect. Notes Logic, 15, A. K. Peters, Natick, 2002, 92–116 | MR | Zbl

[58] Kohlenbach U., “Uniform asymptotic regularity for Mann iterates”, J. Math. Anal. and Appl., 279 (2003), 531–544 | DOI | MR | Zbl

[59] Kohlenbach U., “Some logical metatheorems with applications in functional analysis”, Trans. Amer. Math. Soc. (to appear) | MR

[60] Kohlenbach U., Leuştean L., “Mann iterates of directionally nonexpansive mappings in hyperbolic spaces”, Abstr. and Appl. Anal., 2003, no. 8, 449–477 | DOI | MR | Zbl

[61] Kohlenbach U., Oliva P., “Proof mining in $L_1$-approximation”, Ann. Pure and Appl. Logic, 121 (2003), 1–38 | DOI | MR | Zbl

[62] Köthe G., Topoplogische lineare Räume, Springer, Berlin, 1960 | MR | Zbl

[63] Krasnoselskii M. A., “Dva zamechaniya o metode posledovatelnykh priblizhenii”, UMN, 10:1 (1955), 123–127 | MR

[64] Kroó A., “On the continuity of best approximations in the space of integrable functions”, Acta Math. Acad. Sci. Hung., 32 (1978), 331–348 | DOI | MR | Zbl

[65] Kroó A., “On the uniform modulus of continuity of the operator of best approximation in the space of periodic functions”, Acta Math. Acad. Sci. Hung., 34 (1979), 185–203 | DOI | MR

[66] Kroó A., “On strong unicity of $L_1$-approximation”, Proc. Amer. Math. Soc., 83:4 (1981), 725–729 | DOI | MR | Zbl

[67] Lin P.-K., “Strongly unique best approximation in uniformly convex Banach spaces”, J. Approx. Theory, 56 (1989), 101–107 | DOI | MR | Zbl

[68] Luckhardt H., Extensional Gödel functional interpretation: A consistency proof of classical analysis, Lect. Notes Math., 306, Springer, Berlin, 1973 | MR | Zbl

[69] Luckhardt H., “Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken”, J. Symb. Logic, 54 (1989), 234–263 | DOI | MR | Zbl

[70] Luckhardt H., “Bounds extracted by Kreisel from ineffective proofs”, Kreiseliana: About and around Georg Kreisel, ed. P. Odifreddi, A. K. Peters, Wellesley, MA, 1996, 289–300 | MR | Zbl

[71] Mann W. R., “Mean value methods in iteration”, Proc. Amer. Math. Soc., 4 (1953), 506–510 | DOI | MR | Zbl

[72] Martin K., Unique fixed points in domain theory, El. Notes Theor. Comput. Sci., 45, Elsevier, Amsterdam, 2001, 11 pp. | Zbl

[73] Meszáros J., “A comparison of various definitions of contractive type mappings”, Bull. Calcutta Math. Soc., 84 (1992), 167–194 | MR | Zbl

[74] Newman D. J., Shapiro H. S., “Some theorems on Chebycheff approximation”, Duke Math. J., 30 (1963), 673–681 | DOI | MR | Zbl

[75] Oliva P., “On the computational complexity of best $L_1$-approximation”, Math. Logic Quart., 48 (2002), 66–77, Suppl. 1 | 3.0.CO;2-Y class='badge bg-secondary rounded-pill ref-badge extid-badge'>DOI | MR | Zbl

[76] Pour-El M., Richards J. I., Computability in analysis and physics, Perspectives in Math. Logic, Springer, Berlin, 1989 | MR | Zbl

[77] Prus B., Smarzewski R., “Strongly unique best approximations and centers in uniformly convex spaces”, J. Math. Anal. and Appl., 121 (1987), 10–21 | DOI | MR | Zbl

[78] Rakotch E., “A note on contractive mappings”, Proc. Amer. Math. Soc., 13 (1962), 459–465 | DOI | MR | Zbl

[79] Reich S., Shafrir I., “Nonexpansive iterations in hyperbolic spaces”, Nonlin. Anal., 15 (1990), 537–558 | DOI | MR | Zbl

[80] Rhoades B. E., “Fixed point iterations using infinite matrices”, Trans. Amer. Math. Soc., 196 (1974), 161–176 | DOI | MR | Zbl

[81] Rhoades B. E., “A comparison of various definitions of contractive mappings”, Trans. Amer. Math. Soc., 226 (1977), 257–290 | DOI | MR | Zbl

[82] Rhoades B. E., “Contractive definitions”, Nonlinear analysis, ed. Th. M. Rassias, World Sci., Singapore, 1987, 513–526 | MR

[83] Simpson S. G., Subsystems of second order arithmetic, Perspectives in Math. Logic, Springer, Berlin, 1999 | MR

[84] Spector C., “Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics”, Recursive function theory, Proc. Symp. Pure Math., 5, eds. F. D. E. Dekker, Amer. Math. Soc., Providence, RI, 1962, 1–27 | DOI | MR | Zbl

[85] Takahashi W., “A convexity in metric space and nonexpansive mappings, I”, Kodai Math. Sem. Repts., 22 (1970), 142–149 | DOI | MR | Zbl

[86] A. S. Troelstra, Metamathematical investigation of intuitionistic arithmetic and analysis, Lect. Notes Math., 344, Springer, Berlin, 1973 | MR | Zbl

[87] Troelstra A. S., “Realizability”, Handbook of proof theory, Stud. Logic and Found. Math., 137, ed. S. R. Buss, North-Holland, Amsterdam, 1998, 408–473 | MR

[88] Weihrauch K., Computable analysis, Springer, Berlin, 2000 | MR | Zbl

[89] Kohlenbach U., “Proof mining in functional analysis”, New computational paradigms, First conference on computability in Europe, CiE 2005 (Amsterdam, The Netherlands, June 8–12, 2005), Proceedings, Lecture Notes in Comput. Sci., 3526, Springer, Berlin, 2005, 233–234 | DOI | Zbl