Hostname: page-component-cd9895bd7-jn8rn Total loading time: 0 Render date: 2024-12-22T06:25:28.490Z Has data issue: false hasContentIssue false
  • English
  • Français

Effective Choice and Boundedness Principles in Computable Analysis

Published online by Cambridge University Press:  15 January 2014

Vasco Brattka  and
Guido Gherardi
Vasco Brattka
Affiliation:
Laboratory of Foundational Aspects of Computer Science, Department of Mathematics & Applied Mathematics, University of Cape Town, Rondebosch 7701, South AfricaE-mail: [email protected]
Guido Gherardi
Affiliation:
Dipartimento Di Filosofia, Università Di Bologna, ItalyE-mail: [email protected], URL: http://cca-net.de/
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper we study a new approach to classify mathematical theorems according to their computational content. Basically, we are asking the question which theorems can be continuously or computably transferred into each other? For this purpose theorems are considered via their realizers which are operations with certain input and output data. The technical tool to express continuous or computable relations between such operations is Weihrauch reducibility and the partially ordered degree structure induced by it. We have identified certain choice principles such as co-finite choice, discrete choice, interval choice, compact choice and closed choice, which are cornerstones among Weihrauch degrees and it turns out that certain core theorems in analysis can be classified naturally in this structure. In particular, we study theorems such as the Intermediate Value Theorem, the Baire Category Theorem, the Banach Inverse Mapping Theorem, the Closed Graph Theorem and the Uniform Boundedness Theorem. We also explore how existing classifications of the Hahn–Banach Theorem and Weak Kőnig's Lemma fit into this picture. Well-known omniscience principles from constructive mathematics such as LPO and LLPO can also naturally be considered as Weihrauch degrees and they play an important role in our classification. Based on this we compare the results of our classification with existing classifications in constructive and reverse mathematics and we claim that in a certain sense our classification is finer and sheds some new light on the computational content of the respective theorems. Our classification scheme does not require any particular logical framework or axiomatic setting, but it can be carried out in the framework of classical mathematics using tools of topology, computability theory and computable analysis. We develop a number of separation techniques based on a new parallelization principle, on certain invariance properties of Weihrauch reducibility, on the Low Basis Theorem of Jockusch and Soare and based on the Baire Category Theorem. Finally, we present a number of metatheorems that allow to derive upper bounds for the classification of the Weihrauch degree of many theorems and we discuss the Brouwer Fixed Point Theorem as an example.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 17 , Issue 1 , March 2011 , pp. 73 - 117
Copyright
Copyright © Association for Symbolic Logic 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Bishop, Errett and Bridges, Douglas S., Constructive analysis, Grundlehren der Mathematischen Wissenschaften, vol. 279, Springer, Berlin, 1985.CrossRefGoogle Scholar
[2] Brattka, Vasco, Computable invariance, Theoretical Computer Science, vol. 210 (1999), pp. 3–20.CrossRefGoogle Scholar
[3] Brattka, Vasco, Computable versions of Baire's category theorem, 26th International symposium, Mathematical Foundations of Computer Science, MFCS 2001 (Sgall, Jičí, Pultr, Aleš, and Kolman, Petr, editors), Lecture Notes in Computer Science, vol. 2136, Springer, Berlin, 2001, pp. 224–235.CrossRefGoogle Scholar
[4] Brattka, Vasco, Effective representations of the space of linear bounded operators, Applied General Topology, vol. 4 (2003), no. 1, pp. 115–131.CrossRefGoogle Scholar
[5] Brattka, Vasco, Effective Borel measurability and reducibility of functions, Mathematical Logic Quarterly, vol. 51 (2005), no. 1, pp. 19–44.CrossRefGoogle Scholar
[6] Brattka, Vasco, Computable versions of the uniform boundedness theorem, Logic colloquium 2002 (Chatzidakis, Z., Koepke, P., and Pohlers, W., editors), Lecture Notes in Logic, vol. 27, Association for Symbolic Logic, 2006, pp. 130–151.Google Scholar
[7] Brattka, Vasco, Borel complexity and computability of the Hahn–Banach Theorem, Archive for Mathematical Logic, vol. 46 (2008), no. 7–8, pp. 547–564.CrossRefGoogle Scholar
[8] Brattka, Vasco, Plottable real number functions and the computable graph theorem, SIAM Journal on Computing, vol. 38 (2008), no. 1, pp. 303–328.CrossRefGoogle Scholar
[9] Brattka, Vasco, A computable version of Banach's inverse mapping theorem, Annals of Pure and Applied Logic, vol. 157 (2009), pp. 85–96.CrossRefGoogle Scholar
[10] Brattka, Vasco and Gherardi, Guido, Borel complexity of topological operations on computable metric spaces, Journal of Logic and Computation, vol. 19 (2009), no. 1, pp. 45–76.CrossRefGoogle Scholar
[11] Brattka, Vasco and Gherardi, Guido, Effective choice and boundedness principles in computable analysis, Proceedings of the sixth international conference on Computability and Complexity in Analysis, CCA 2009 (Bauer, Andrej, Hertling, Peter, and Ko, Ker-I, editors), Leibniz–Zentrum für Informatik, Schloss Dagstuhl, Germany, 2009, pp. 95–106.Google Scholar
[12] Brattka, Vasco and Gherardi, Guido, Weihrauch degrees, omniscience principles and weak computability, The Journal of Symbolic Logic, vol. 76 (2011), no. 1, pp. 143–176.CrossRefGoogle Scholar
[13] Brattka, Vasco and Presser, Gero, Computability on subsets of metric spaces, Theoretical Computer Science, vol. 305 (2003), pp. 43–76.CrossRefGoogle Scholar
[14] Brattka, Vasco and Weihrauch, Klaus, Computability on subsets of Euclidean space I: Closed and compact subsets, Theoretical Computer Science, vol. 219 (1999), pp. 65–93.CrossRefGoogle Scholar
[15] Bridges, Douglas and Richman, Fred, Varieties of constructive mathematics, London Mathematical Society Lecture Note Series, vol. 97, Cambridge University Press, Cambridge, 1987.CrossRefGoogle Scholar
[16] Caldwell, J. and Pour-El, Marian Boykan, On a simple definition of computable functions of a real variable—with applications to functions of a complex variable, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 21 (1975), pp. 1–19.Google Scholar
[17] Cenzer, Douglas and Jockusch, Carl G. Jr., classes—structure and applications, Computability theory and its applications, Contemporary Mathematics, vol. 257, American Mathematical Society, Providence, RI, 2000, pp. 39–59.CrossRefGoogle Scholar
[18] Gelfond, Michael G., A class of theorems with valid constructive counterparts, Constructive mathematics (Richman, Fred, editor), Lecture Notes in Mathematics, vol. 873, Springer, Berlin, 1981, pp. 314–320.CrossRefGoogle Scholar
[19] Gherardi, Guido, Effective Borel degrees of some topological functions, Mathematical Logic Quarterly, vol. 52 (2006), no. 6, pp. 625–642.CrossRefGoogle Scholar
[20] Gherardi, Guido and Marcone, Alberto, How incomputable is the separable Hahn–Banach theorem?, Notre Dame Journal of Formal Logic, vol. 50 (2009), pp. 393–425.CrossRefGoogle Scholar
[21] Hauck, Jürgen, Berechenbare reelle Funktionenfolgen, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 22 (1976), pp. 265–282.CrossRefGoogle Scholar
[22] Hayashi, Susumu, Mathematics based on incremental learning–excluded middle and inductive inference, Theoretical Computer Science, vol. 350 (2006), pp. 125–139.CrossRefGoogle Scholar
[23] Hertling, Peter, Unstetigkeitsgrade von Funktionen in der effektiven Analysis, Dissertation, Fern Universität Hagen, Hagen, November 1996.Google Scholar
[24] Ishihara, Hajime, An omniscience principle, the König lemma and the Hahn–Banach theorem, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 36 (1990), pp. 237–240.CrossRefGoogle Scholar
[25] Ishihara, Hajime, Informal constructive reverse mathematics, CDMTCS research report, Centre for Discrete Mathematics and Theoretical Computer Science, 2004.Google Scholar
[26] Ishihara, Hajime, Constructive reverse mathematics: compactness properties, From sets and types to topology and analysis: Towards practicable foundations for constructive mathematics (Crosilla, Laura and Schuster, Peter, editors), Oxford University Press, 2005, pp. 245–267.CrossRefGoogle Scholar
[27] Ishihara, Hajime, Unique existence and computability in constructive reverse mathematics, Computation and logic in the real world, third conference on Computability in Europe, CiE 2007 (Cooper, S. Barry, Löwe, Benedikt, and Sorbi, Andrea, editors), Lecture Notes in Computer Science, vol. 4497, Springer, Berlin, 2007, pp. 368–377.Google Scholar
[28] Jockusch, Carl G. Jr. and Soare, Robert I., Degrees of members of classes, Pacific Journal of Mathematics, vol. 40 (1972), pp. 605–616.CrossRefGoogle Scholar
[29] Kleene, S. C., Recursive predicates and quantifiers, Transactions of the American Mathematical Society, vol. 53 (1943), pp. 41–73.CrossRefGoogle Scholar
[30] Kohlenbach, Ulrich, The use of a logical principle of uniform boundedness in analysis, Logic and foundations of mathematics (Cantini, A., Casari, E., and Minari, P., editors), Synthese Library, vol. 280, Kluwer Academic Publishers, 1999, pp. 93–106.CrossRefGoogle Scholar
[31] Kohlenbach, Ulrich, On uniform weak König's lemma, Annals of Pure and Applied Logic, vol. 114 (2002), pp. 103–116.CrossRefGoogle Scholar
[32] Kohlenbach, Ulrich, Higher order reverse mathematics, Reverse mathematics 2001 (Simpson, Stephen G., editor), Lecture Notes in Logic, vol. 21, A K Peters, 2005, pp. 281–295.Google Scholar
[33] Kreisel, Georg and Lacombe, Daniel, Ensembles récursivement mesurables et ensembles récursivement ouverts et fermés, Comptes Rendus Mathématique. Académie des Sciences. Paris, vol. 245 (1957), pp. 1106–1109.Google Scholar
[34] Mandelkern, Mark, Constructively complete finite sets, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 34 (1988), no. 2, pp. 97–103.CrossRefGoogle Scholar
[35] Mylatz, Uwe, Vergleich unstetiger Funktionen: “Principle of Omniscience” und Vollständigkeit in der C–hierarchie, Ph.D. thesis, Faculty for Mathematics and Computer Science, University Hagen, Germany, 2006.Google Scholar
[36] Nakata, Masahiro and Hayashi, Susumu, A limiting first order realizability interpretation, Scientiae Mathematicae Japonicae, vol. 55 (2002), no. 3, pp. 567–580.Google Scholar
[37] Odifreddi, Piergiorgio, Classical recursion theory, Studies in Logic and the Foundations of Mathematics, vol. 125, North-Holland, Amsterdam, 1989.Google Scholar
[38] Pauly, Arno, On the (semi)lattices induced by continuous reducibilities, Mathematical Logic Quarterly, vol. 56 (2010), no. 5, pp. 488–502.CrossRefGoogle Scholar
[39] Pour-El, Marian B. and Richards, J. Ian, Computability in analysis and physics, Perspectives in Mathematical Logic, Springer, Berlin, 1989.CrossRefGoogle Scholar
[40] Richman, Fred, Polynomials and linear transformations, Linear Algebra and its Applications, vol. 131 (1990), no. 1, pp. 131–137.CrossRefGoogle Scholar
[41] Richman, Fred, Omniscience principles and functions of bounded variation, Mathematical Logic Quarterly, vol. 48 (2002), no. 1, pp. 111–116.3.0.CO;2-6>CrossRefGoogle Scholar
[42] Rogers, Hartley, Theory of recursive functions and effective computability, McGraw-Hill, New York, 1967.Google Scholar
[43] Sakamoto, Nobuyuki and Yamazaki, Takeshi, Uniform versions of some axioms of second order arithmetic, Mathematical Logic Quarterly, vol. 50 (2004), no. 6, pp. 587–593.CrossRefGoogle Scholar
[44] Schuster, Peter, Unique solutions, Mathematical Logic Quarterly, vol. 52 (2006), no. 6, pp. 534–539.CrossRefGoogle Scholar
[45] Schuster, Peter, Corrigendum to “unique solutions”, Mathematical Logic Quarterly, vol. 53 (2007), no. 2, p. 214.CrossRefGoogle Scholar
[46] Simpson, Stephen, Tanaka, Kazuyuki, and Yamazaki, Takeshi, Some conservation results on weak König's lemma, Annals of Pure and Applied Logic, vol. 118 (2002), no. 1–2, pp. 87–114.CrossRefGoogle Scholar
[47] Simpson, Stephen G., Subsystems of second order arithmetic, Perspectives in Mathematical Logic, Springer, Berlin, 1999.CrossRefGoogle Scholar
[48] Weidmann, Joachim, Linear operators in Hilbert spaces, Graduate Texts in Mathematics, vol. 68, Springer, Berlin, 1980.CrossRefGoogle Scholar
[49] Weihrauch, Klaus, The degrees of discontinuity of some translators between representations of the real numbers, Technical report TR-92-050, International Computer Science Institute, Berkeley, July 1992.Google Scholar
[50] Weihrauch, Klaus, The TTE-interpretation of three hierarchies of omniscience principles, Informatik Berichte 130, FernUniversität Hagen, Hagen, September 1992.Google Scholar
[51] Weihrauch, Klaus, Computable analysis, Springer, Berlin, 2000.CrossRefGoogle Scholar
[52] Weihrauch, Klaus, On computable metric spaces Tietze–Urysohn extension is computable, 4th International workshop on Computability and Complexity in Analysis, CCA 2000 (Blanck, Jens, Brattka, Vasco, and Hertling, Peter, editors), Lecture Notes in Computer Science, vol. 2064, Springer, Berlin, 2001, pp. 357–368.Google Scholar