Completeness: When Enough is Enough
Hannes DienerSchool of Mathematics and Statistics, University of Canterbury, Christchurch, New Zealand
Matthew HendtlassSchool of Mathematics and Statistics, University of Canterbury, Christchurch, New Zealand
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.
Cite this article
Hannes Diener, Matthew Hendtlass, Completeness: When Enough is Enough. Doc. Math. 24 (2019), pp. 899–914DOI 10.4171/DM/696