×

Problems, solutions, and completions. (English) Zbl 1184.03059

Summary: If a continuous function on a complete metric space has approximate roots and in a uniform manner at most one root, then it actually has a root. We validate this heuristic principle in Bishop-style constructive mathematics without countable choice, and thus can shed some more light on the role played by the completion when it comes to solving equations.

MSC:

03F60 Constructive and recursive analysis
03E25 Axiom of choice and related propositions
54E50 Complete metric spaces
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] P. Aczel, The type theoretic interpretation of constructive set theory, in: A. Macintyre, L. Pacholski, J. Paris, (Eds.), Logic Colloquium’77, North-Holland, Amsterdam, 1978, pp. 55-66.; P. Aczel, The type theoretic interpretation of constructive set theory, in: A. Macintyre, L. Pacholski, J. Paris, (Eds.), Logic Colloquium’77, North-Holland, Amsterdam, 1978, pp. 55-66. · Zbl 0481.03035
[2] Aczel, P.; Crosilla, L.; Ishihara, H.; Palmgren, E.; Schuster, P., Binary refinement implies discrete exponentiation, Studia Logica, 84, 361-368 (2006) · Zbl 1112.03048
[3] P. Aczel, M. Rathjen, Notes on Constructive Set Theory, Institut Mittag-Leffler Preprint no. 40, 2000/2001.; P. Aczel, M. Rathjen, Notes on Constructive Set Theory, Institut Mittag-Leffler Preprint no. 40, 2000/2001.
[4] A. Bauer, Realizability as connection between constructive and computable mathematics, in: T. Grubba, P. Hertling, H. Tsuiki, K. Weihrauch (Eds.), CCA 2005, Second International Conference on Computability and Complexity in Analysis. Kyoto, Japan, August 2005, Fernuniversität Hagen, Informatik-Berichte, vols. 326-327, 2005, pp. 378-379.; A. Bauer, Realizability as connection between constructive and computable mathematics, in: T. Grubba, P. Hertling, H. Tsuiki, K. Weihrauch (Eds.), CCA 2005, Second International Conference on Computability and Complexity in Analysis. Kyoto, Japan, August 2005, Fernuniversität Hagen, Informatik-Berichte, vols. 326-327, 2005, pp. 378-379.
[5] A. Bauer, P. Taylor, The Dedekind reals in abstract Stone duality, in: T. Grubba, P. Hertling, H. Tsuiki, K. Weihrauch (Eds.), CCA 2005, Second International Conference on Computability and Complexity in Analysis. Kyoto, Japan, August 2005, Fernuniversität Hagen, Informatik-Berichte, vols. 326-327, 2005, pp. 25-64.; A. Bauer, P. Taylor, The Dedekind reals in abstract Stone duality, in: T. Grubba, P. Hertling, H. Tsuiki, K. Weihrauch (Eds.), CCA 2005, Second International Conference on Computability and Complexity in Analysis. Kyoto, Japan, August 2005, Fernuniversität Hagen, Informatik-Berichte, vols. 326-327, 2005, pp. 25-64. · Zbl 1262.03130
[6] J. Berger, The fan theorem and uniform continuity, in: S.B. Cooper, B. Löwe, L. Torenvliet, (Eds.), New Computational Paradigms, First Conference on Computability in Europe, CiE 2005, Amsterdam, The Netherlands, June 2005, Lect. Notes Comput. Sci., vol. 3526, Springer, Berlin and Heidelberg, 2005, pp. 18-22.; J. Berger, The fan theorem and uniform continuity, in: S.B. Cooper, B. Löwe, L. Torenvliet, (Eds.), New Computational Paradigms, First Conference on Computability in Europe, CiE 2005, Amsterdam, The Netherlands, June 2005, Lect. Notes Comput. Sci., vol. 3526, Springer, Berlin and Heidelberg, 2005, pp. 18-22.
[7] J. Berger, The logical strength of the uniform continuity theorem, in: A. Beckmann, U. Berger, B. Löwe, J.V. Tucker (Eds.), Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, July 2006, Lect. Notes Comput. Sci., vol. 3988, Springer, Berlin and Heidelberg, 2006, pp. 35-39.; J. Berger, The logical strength of the uniform continuity theorem, in: A. Beckmann, U. Berger, B. Löwe, J.V. Tucker (Eds.), Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, July 2006, Lect. Notes Comput. Sci., vol. 3988, Springer, Berlin and Heidelberg, 2006, pp. 35-39. · Zbl 1145.03339
[8] Berger, J.; Bridges, D.; Schuster, P., The fan theorem and unique existence of maxima, J. Symb. Logic, 71, 713-720 (2006) · Zbl 1107.03064
[9] Berger, J.; Ishihara, H., Brouwer’s fan theorem and unique existence in constructive analysis, Math. Log. Quart., 51, 369-373 (2005)
[10] Berger, J.; Schuster, P., Classifying Dini’s theorem, Notre Dame J. Formal Logic, 47, 253-262 (2006) · Zbl 1156.03055
[11] Bishop, E., Foundations of Constructive Analysis (1967), McGraw-Hill: McGraw-Hill New York · Zbl 0183.01503
[12] Bishop, E.; Bridges, D., Constructive Analysis (1985), Springer: Springer Berlin · Zbl 0656.03042
[13] Brattka, V., Borel complexity and computability of the Hahn-Banach theorem, Arch. Math. Logic, 46, 547-564 (2008) · Zbl 1140.03040
[14] Bridges, D., Recent progress in constructive approximation theory, (Troelstra, A. S.; van Dalen, D., The L.E.J. Brouwer Centenary Symposium (1982), North-Holland: North-Holland Amsterdam), 41-50
[15] Bridges, D.; Richman, F., Varieties of Constructive Mathematics (1987), Cambridge University Press · Zbl 0618.03032
[16] Bridges, D.; Vıˆţă, L., Techniques of Constructive Analysis (2006), Springer: Springer New York
[17] C.W. Burden, C.J. Mulvey, Banach spaces in categories of sheaves, in: M. Fourman, C. Mulvey, D. Scott (Eds.), Applications of Sheaves, Proceedings, Durham, 1977, Lecture Notes in Math., vol. 753, Springer, Berlin and Heidelberg, 1979, pp. 169-196.; C.W. Burden, C.J. Mulvey, Banach spaces in categories of sheaves, in: M. Fourman, C. Mulvey, D. Scott (Eds.), Applications of Sheaves, Proceedings, Durham, 1977, Lecture Notes in Math., vol. 753, Springer, Berlin and Heidelberg, 1979, pp. 169-196. · Zbl 0432.46066
[18] Crosilla, L.; Ishihara, H.; Schuster, P., On constructing completions, J. Symb. Logic, 70, 969-978 (2005) · Zbl 1099.03044
[19] C. Fox, Point-set and point-free topology in constructive set theory, Doctoral Dissertation, School of Mathematics, University of Manchester, 2005.; C. Fox, Point-set and point-free topology in constructive set theory, Doctoral Dissertation, School of Mathematics, University of Manchester, 2005.
[20] Ishihara, H., Informal constructive reverse mathematics, Sūrikaisekikenkyūsho Kōkyūroku, 1381, 108-117 (2004)
[21] Ishihara, H., Constructive reverse mathematics: compactness properties, (Crosilla, L.; Schuster, P., From Sets and Types to Topology and Analysis. From Sets and Types to Topology and Analysis, Oxford Logic Guides, vol. 48 (2005), Oxford University Press), 245-267 · Zbl 1095.03075
[22] Ishihara, H., Reverse mathematics in Bishop’s constructive mathematics, Philosophia Scientiae, cahier spécial, 6, 43-59 (2006)
[23] H. Ishihara, Unique existence and computability in constructive reverse mathematics, in: S.B. Cooper, B. Löwe, A. Sorbi (Eds.), Computation and Logic in the Real World, Third Conference on Computability in Europe, CiE 2007, Siena, Italy, June 2007, Springer, Berlin and Heidelberg, Lect. Notes Comput. Sci., vol. 4497, 2007, pp. 368-377.; H. Ishihara, Unique existence and computability in constructive reverse mathematics, in: S.B. Cooper, B. Löwe, A. Sorbi (Eds.), Computation and Logic in the Real World, Third Conference on Computability in Europe, CiE 2007, Siena, Italy, June 2007, Springer, Berlin and Heidelberg, Lect. Notes Comput. Sci., vol. 4497, 2007, pp. 368-377. · Zbl 1151.03351
[24] 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, 27-94 (1993) · Zbl 0795.03086
[25] Kohlenbach, U.; Oliva, P., Proof mining: a systematic way of analysing proofs in mathematics, Proc. Steklov Inst. Math., 3, 242, 136-164 (2003) · Zbl 1079.03045
[26] V. Ja. Kreı˘novič, Review of‘Constructive Functional Analysis’, MR0521982, 82k:03094.; V. Ja. Kreı˘novič, Review of‘Constructive Functional Analysis’, MR0521982, 82k:03094.
[27] P. Lietz, From Constructive Mathematics to Computable Analysis via the Realizability Interpretation, Doctoral Dissertation, Technische Universität Darmstadt, 2004.; P. Lietz, From Constructive Mathematics to Computable Analysis via the Realizability Interpretation, Doctoral Dissertation, Technische Universität Darmstadt, 2004. · Zbl 1131.03303
[28] Lifshits, V. A., Investigation of constructive functions by the method of fillings, J. Soviet Math., 1, 41-47 (1973) · Zbl 0252.02034
[29] Loeb, I., Equivalents of the (weak) fan theorem, Ann. Pure Appl. Logic, 132, 51-66 (2005) · Zbl 1060.03081
[30] C.J. Mulvey, Banach spaces over a compact space, in: H. Herrlich, G. Preuss (Eds.), Categorical Topology, Proceedings, Berlin, 1978, Lecture Notes in Math., vol. 719, Springer, Berlin and Heidelberg 1979, pp. 243-249.; C.J. Mulvey, Banach spaces over a compact space, in: H. Herrlich, G. Preuss (Eds.), Categorical Topology, Proceedings, Berlin, 1978, Lecture Notes in Math., vol. 719, Springer, Berlin and Heidelberg 1979, pp. 243-249.
[31] Palmgren, E., A constructive and functional embedding of locally compact metric spaces into locales, Topol. Appl., 154, 1854-1880 (2007) · Zbl 1116.03057
[32] M. Rathjen, Choice principles in constructive and classical set theories, in: Z. Chatzidakis, P. Koepke, W. Pohlers (Eds.), Logic Colloquium’02, Proceedings, Münster, 2002, Lect. Notes Logic 27, Assoc. Symbol. Logic, La Jolla, 2006, pp. 299-326.; M. Rathjen, Choice principles in constructive and classical set theories, in: Z. Chatzidakis, P. Koepke, W. Pohlers (Eds.), Logic Colloquium’02, Proceedings, Münster, 2002, Lect. Notes Logic 27, Assoc. Symbol. Logic, La Jolla, 2006, pp. 299-326. · Zbl 1121.03065
[33] Richman, F., Intuitionism as generalization, Philos. Math., 5, 3, 124-128 (1990) · Zbl 0716.03001
[34] Richman, F., The fundamental theorem of algebra: a constructive development without choice, Pacific J. Math., 196, 213-230 (2000) · Zbl 1046.03036
[35] Richman, F., Spreads and choice in constructive mathematics, Indag. Math. (NS), 13, 259-267 (2002) · Zbl 1035.03032
[36] Richman, F., Real numbers and other completions, Math. Log. Quart., 54, 98-108 (2008) · Zbl 1134.03041
[37] Schuster, P., Unique existence, approximate solutions, and countable choice, Theoret. Comput. Sci., 305, 433-455 (2003) · Zbl 1050.03042
[38] Schuster, P., Countable choice as a questionable uniformity principle, Philos. Math., 12, 3, 106-134 (2004) · Zbl 1074.03003
[39] Schuster, P., Unique solutions, Math. Log. Quart., 52, 534-539 (2006), Corrigendum: Math. Log. Quart. 53 (2007) 214 · Zbl 1110.03059
[40] P. Schuster, Problems as solutions, in: S.B. Cooper, B. Löwe, A. Sorbi (Eds.), Computation and Logic in the Real World, Third Conference on Computability in Europe, CiE 2007, Siena, Italy, June 2007, Lect. Notes Comput. Sci., vol. 4497, Springer, Berlin and Heidelberg, 2007, pp. 676-684.; P. Schuster, Problems as solutions, in: S.B. Cooper, B. Löwe, A. Sorbi (Eds.), Computation and Logic in the Real World, Third Conference on Computability in Europe, CiE 2007, Siena, Italy, June 2007, Lect. Notes Comput. Sci., vol. 4497, Springer, Berlin and Heidelberg, 2007, pp. 676-684.
[41] P. Schuster, H. Schwichtenberg, Constructive solutions of continuous equations, in: G. Link (Ed.), One Hundred Years of Russell’s Paradox, International Conference in Logic and Philosophy, München, Germany, June 2001, De Gruyter, Berlin, De Gruyter Series in Logic and Its Applications, vol. 6, 2004, pp. 227-245.; P. Schuster, H. Schwichtenberg, Constructive solutions of continuous equations, in: G. Link (Ed.), One Hundred Years of Russell’s Paradox, International Conference in Logic and Philosophy, München, Germany, June 2001, De Gruyter, Berlin, De Gruyter Series in Logic and Its Applications, vol. 6, 2004, pp. 227-245. · Zbl 1074.03030
[42] Schwichtenberg, H., A direct proof of the equivalence between Brouwer’s fan theorem and König’s lemma with a uniqueness hypothesis, J. UCS, 11, 2086-2095 (2005) · Zbl 1124.03042
[43] Stolzenberg, G., Sets as limits yellow, Typescript (1988)
[44] P. Taylor, A lambda calculus for real analysis, in: T. Grubba, P. Hertling, H. Tsuiki, K. Weihrauch (Eds.), CCA 2005, Second International Conference on Computability and Complexity in Analysis, Kyoto, Japan, August 2005, Fernuniversität Hagen, Informatik-Berichte, vol. 326-327, 2005, pp. 227-266.; P. Taylor, A lambda calculus for real analysis, in: T. Grubba, P. Hertling, H. Tsuiki, K. Weihrauch (Eds.), CCA 2005, Second International Conference on Computability and Complexity in Analysis, Kyoto, Japan, August 2005, Fernuniversität Hagen, Informatik-Berichte, vol. 326-327, 2005, pp. 227-266.
[45] W. Veldman, Brouwer’s fan theorem as an axiom and as a contrast to Kleene’s alternative, Preprint, Radboud University, Nijmegen, 2005.; W. Veldman, Brouwer’s fan theorem as an axiom and as a contrast to Kleene’s alternative, Preprint, Radboud University, Nijmegen, 2005. · Zbl 1327.03046
[46] Vickers, S., Localic completion of generalised metric spaces. I, Theor. Appl. Categ., 14, 15, 328-356 (2005), electronic · Zbl 1083.54019
[47] S. Vickers, Localic completion of generalised metric spaces. II. Power locales, Preprint, School of Computer Science, University of Birmingham, 2004.; S. Vickers, Localic completion of generalised metric spaces. II. Power locales, Preprint, School of Computer Science, University of Birmingham, 2004.
[48] Weihrauch, K., Computable Analysis. An Introduction (2000), Springer: Springer Berlin · Zbl 0956.68056
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.