[FOM] impredicative definitions/paper announcement

[Andrej Bauer]

>  Now the main difficulty of the predicativists is that the "real"
> numbers, so central to modern mathematics and science, are not
> objects of the crystal clear type described above.

One way to work with the real numbers is to use locale theory, in
particular countably presented locales. The reals are then described
in terms of the countable basis of open intervals with rational
endpoints. The locale itself is uncountable, but one can work with the
basis all the time. This is one way in which real numbers can be
implemented (computers are predicativists, even constructive
predicativists), and is also how they are viewed in formal topology.

Would the locale of reals (expressed in terms of a countable basis
with a countable presentation) be an acceptable definition of reals
for a predicativist? Which theorems of analysis can we use as the
Litmus test to see whether the definition is good enough?

With kind regards,

Andrej