*Semantics Club 07 12 2001*

# After the Interval

(joint work with Martin Escardo)### Abstract

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?