Diener, Hannes; Hendtlass, Matthew

Completeness: When Enough is Enough

Doc. Math. 24, 899-914 (2019)
DOI: 10.25537/dm.2019v24.899-914


We investigate the notion of a complete enough metric space that, while classically vacuous, in a constructive setting allows for the generalisation of many theorems to a much wider class of spaces. In doing so, this notion also brings the known body of constructive results significantly closer to that of classical mathematics. Most prominently, we generalise the Kreisel-Lacome-Shoenfield Theorem/Tseytin's Theorem on the continuity of functions in recursive mathematics.

Mathematics Subject Classification

03F60, 03D78, 03F55


constructive mathematics, computable analysis, completeness


  • 1. P. Aczel and M. Rathjen. Notes on constructive set theory. Technical Report 40, Institut Mittag-Leffler, The Royal Swedish Academy of Sciences, 2001.
  • 2. E. Bishop and D. S. Bridges. Constructive Analysis. Springer-Verlag, 1985. zbl 0656.03042; MR0804042.
  • 3. D. S. Bridges and H. Ishihara. Linear mappings are fairly well-behaved. Archiv der Mathematik, 54(6):558-562, 1990. DOI 10.1007/BF01188684; zbl 0715.46053; MR1052976.
  • 4. D. S. Bridges, P. Schuster, and F. Richman. A weak countable choice principle. Proceedings of the American Mathematical Society (128):2749-2752, 2000. DOI 10.1090/S0002-9939-00-05327-2; zbl 0949.03060; MR1664313.
  • 5. D. S. Bridges and L. S. Vî\ct\ua. Techniques of constructive analysis. Universitext. Springer, New York, 2006. DOI 10.1007/978-0-387-38147-3; zbl 1107.03065; MR2253074.
  • 6. H. Diener. Variations on a theme by Ishihara. Mathematical Structures in Computer Science, 25(7):1569-1577, 2015. DOI 10.1017/S0960129513000261; zbl 1362.03054; MR3391063.
  • 7. H. Diener and M. Hendtlass. Bishop's lemma. Mathematical Logic Quarterly, 64(1-2):49-54, 2018. MR3803066.
  • 8. D. L. G. Kreisel and J. R. Shoenfield. Fonctionnelles récursivement définissables et fonctionnelles récursives. C. R. Acad. Sci. Paris, 245:399-402, 1957. zbl 0078.00702; MR0088457.
  • 9. H. Ishihara. Continuity and nondiscontinuity in constructive mathematics. Journal of Symbolic Logic, 56(4):1349-1354, 1991. DOI 10.2307/2275479; zbl 0745.03048; MR1136461.
  • 10. H. Ishihara. Continuity properties in constructive mathematics. Journal of Symbolic Logic, 57(2):557-565, 1992. DOI 10.2307/2275292; zbl 0771.03018; MR1169194.
  • 11. H. Ishihara. Sequential continuity of linear mappings in constructive mathematics. Journal of Universal Computer Science, 3(11):1250-1254, 1997. zbl 0970.46050; MR1661782.
  • 12. U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer, Berlin Heidelberg, 2008. DOI 10.1007/978-3-540-77533-1; zbl 1158.03002; MR2445721.
  • 13. R. Lubarsky. On the failure of BD-N and BD, and an application to the anti-specker property. Journal of Symbolic Logic, 78(1):39-56, 2013. DOI 10.2178/jsl.7801030; zbl 1278.03089; MR3087060; arxiv 1510.00990.
  • 14. M. Mandelkern. Constructive Continuity. Memoirs of the American Mathematical Society. American Mathematical Society, 1983. DOI 10.1090/memo/0277; zbl 0537.26002; MR0690901.
  • 15. M. Mandelkern. Constructively complete finite sets. Mathematical Logic Quarterly, 34(2):97-103, 1988. DOI 10.1002/malq.19880340202; zbl 0627.03044; MR0930253.
  • 16. F. Richman. Intuitionistic notions of boundedness in \(\mathbb{n} \). Mathematical Logic Quarterly, 55(1):31-36, 2009. DOI 10.1002/malq.200710072; zbl 1155.03043; MR2489290.
  • 17. G. Tseĭtin. Algorithmic operators in constructive complete separable metric spaces. Doklady. Akademii Nauk SSSR, 128:49-52, 1959. zbl 0124.00402; MR0115910.


Diener, Hannes
School of Mathematics and Statistics, University of Canterbury, Christchurch, New Zealand
Hendtlass, Matthew
School of Mathematics and Statistics, University of Canterbury, Christchurch, New Zealand