KnowledgeBase » 
PUBLICATION
» ID = 779
The Continuum
by Robert L. Constable
2020
Abstract
The key feature of Brouwer’s intuitionistic mathematics is its treatment of the continuum of real numbers. That type includes real numbers given by computable sequences of rationals in the style of the 1985 book by Bridges and Bishop, Constructive Analysis. It also includes real numbers given by free choice sequences of point cores. It is natural to assign a com- putational complexity cost in the style of Hartmanis and Stearns to real numbers given by algorithms. However, free choice sequences are not given by algorithms. On the other hand, in order for a choice sequence to define a real number, the elements of the sequence must be increasingly better rational approximations to the number. There is a cost parameterized by the natural numbers to computing these rational approximations. That is one measure for the computational complexity of the real numbers given by free choice.
This short article establishes a framework for formalizing and investigating this notion of complexity for computing with Brouwer’s continuum. The fundamental principle about the intuitionistic continuum is the Continuity Principle. This is perhaps the central principle of Brouwer’s mathematics, showing that his real numbers are not enumerable, i.e. count- able, and it contradicts classical real analysis. It allows us to compute with Brouwer’s real numbers.