Semantics Club 07 12 2001
In this talk I will address the question: "what is the correct constructive notion of real number?" Standard accounts are based on arithmetisation - one starts off with the natural numbers and constructs the real numbers from them. I shall discuss an alternative approach, which is joint work with Martin Escardo. Rather than constructing the real numbers, we assume instead the existence of an interval of real numbers as an independent object that is to be identified via its characterising geometric properties. Interestingly, this approach gives rise to a new constructive notion of real number - at least it appears to. I shall discuss how this new notion of real number compares with the familiar notions of Cauchy and Dedekind real. Several open questions remain, not least: is the new notion of real number genuinely different from the Cauchy reals?