Hostname: page-component-7b7567c8c-jswmv Total loading time: 0 Render date: 2026-11-15T10:57:38.130Z Has data issue: false hasContentIssue false
  • English
  • Français

Uniqueness, continuity and the existence of implicit functions in constructive analysis

Part of:Real functions: Miscellaneous topicsProof theory and constructive mathematics

Published online by Cambridge University Press:  01 June 2011

H. Diener and
P. Schuster
H. Diener
Affiliation:
Universitat Siegen, Fachbereich 6: Mathematik Walter-Flex-Str. 3 57072 Siegen, Germany (email: diener@math.uni-siegen.de)
P. Schuster
Affiliation:
Pure Mathematics, University of Leeds, LS2 9JT, U.K. (email: pschust@maths.leeds.ac.uk)

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We extract a quantitative variant of uniqueness from the usual hypotheses of the implicit function theorem. Not only does this lead to an a priori proof of continuity, but also to an alternative, full proof of the implicit function theorem. Additionally, we investigate implicit functions as a case of the unique existence paradigm with parameters.

MSC classification

Secondary:03F60: Constructive and recursive analysis26E40: Constructive real analysis03F55: Intuitionistic mathematics

Information

Type
Research Article
Information
LMS Journal of Computation and Mathematics , Volume 14 , 2011, pp. 127 - 136
Copyright
Copyright © London Mathematical Society 2011

References

[1]Aczel, P., ‘The type theoretic interpretation of constructive set theory’, Logic colloquium ’77 (eds Macintyre, A., Pacholski, L. and Paris, J.; North-Holland, Amsterdam, 1978) 55–66.CrossRefGoogle Scholar
[2]Aczel, P. and Rathjen, M., ‘Notes on constructive set theory’, Institut Mittag–Leffler Preprint No. 40, 2000/01.Google Scholar
[3]Berger, J., Bridges, D. and Schuster, P., ‘The fan theorem and unique existence of maxima’, J. Symbolic Logic 71 (2006) 713–720.CrossRefGoogle Scholar
[4]Bishop, E., Foundations of constructive analysis (McGraw-Hill, New York, 1967).Google Scholar
[5]Bishop, E. and Bridges, D., Constructive analysis (Springer, Berlin, 1985).CrossRefGoogle Scholar
[6]Bridges, D., Calude, C., Pavlov, B. and Ştefănescu, D., ‘The constructive implicit function theorem and applications in mechanics’, Chaos Solitons Fractals 10 (1999) 927–934.Google Scholar
[7]Bridges, D. and Richman, F., Varieties of constructive mathematics (Cambridge University Press, Cambridge, 1987).CrossRefGoogle Scholar
[8]Bridges, D. and Vǐţă, L., Techniques of constructive analysis (Springer, New York, 2006).Google Scholar
[9]Diener, H. and Schuster, P., ‘Uniqueness, continuity, and existence of implicit functions in constructive analysis’, Sixth Internat. Conf. on Computability and Complexity in Analysis 2009 (eds Bauer, A., Hertling, P. and Ko, Ker-I; Schloß Dagstuhl Leibniz–Zentrum für Informatik, Dagstuhl, 2009), http://drops.dagstuhl.de/opus/volltexte/2009/2265.Google Scholar
[10]Forster, O., Analysis 2: differentialrechnung im ℝn, gewöhnliche differentialgleichungen, 6th edn (Vieweg, Wiesbaden, 2005).CrossRefGoogle Scholar
[11]Krantz, S. G. and Parks, H. R., The implicit function theorem. History, theory, and applications (Birkhäuser, Boston, 2002).Google Scholar
[12]McNicholl, T. H., ‘A uniformly computable implicit function theorem’, MLQ Math. Log. Q. 54 (2008) 272–279.CrossRefGoogle Scholar
[13]Rathjen, M., ‘Choice principles in constructive and classical set theories’, Logic colloquium ’02. Proceedings, Münster, 2002, Lecture Notes in Logic 27 (eds Chatzidakis, Z., Koepke, P. and Pohlers, W.; Assoc. Symbol. Logic, La Jolla, 2006) 299–326.Google Scholar
[14]Richman, F., ‘Intuitionism as generalization’, Philos. Math. (3) 5 (1990) 124–128.CrossRefGoogle Scholar
[15]Richman, F., ‘The fundamental theorem of algebra: a constructive development without choice’, Pacific J. Math. 196 (2000) 213–230.CrossRefGoogle Scholar
[16]Schuster, P., ‘What is continuity, constructively?’, J. UCS 11 (2005) 2076–2085.Google Scholar
[17]Schuster, P., ‘Unique solutions’, Math. Log. Q. 52  (2006) 534–539; Corrigendum: Math. Log. Q. 53 (2007) 214.CrossRefGoogle Scholar
[18]Schuster, P., ‘Zur Eindeutigkeit impliziter Funktionen’, Preprint, Universitá di Firenze, 2009.Google Scholar
[19]Schuster, P., ‘Problems, solutions, and completions’, J. Log. Algebr. Program. 79 (2010) 84–91.CrossRefGoogle Scholar
[20]Weihrauch, K., Computable analysis. An introduction (Springer, Berlin, 2000).CrossRefGoogle Scholar
[21]Ziegler, M., ‘Effectively open real functions’, J. Complexity 22 (2006) 827–849.CrossRefGoogle Scholar