[FOM] When is it appropriate to treat isomorphism as identity?

Andrej Bauer andrej.bauer at andrej.com
Sun May 10 03:13:46 EDT 2009

Dear Arnon,

> The concept of a "real number" was historically
> problematic, and in my opinion it still is, since it
> depends on the very questionable powerset axiom.

But aren't there constructions of real numbers that do not require the
powerset axiom? For example:
- reals in constructive set theory, see section 3.6 of
- reals in type theory with inductive definitions,
- reals in Abstract Stone Duality, http://www.paultaylor.eu/ASD/dedras/
- reals by a universal property,
- reals may be constructed in any "Pi-pretopos with natural numbers",
http://ncatlab.org/nlab/show/pretopos , as completion of rationals by
Cauchy sequences

In a particular setting such as ZF it might be the case that one needs
the powerset axiom to show that the reals exist, but this may a
deficiency of the particular setting, not the real numbers. Do you
feel that the reals themselves (not necessarily within ZF) are

With kind regards,


More information about the FOM mailing list