[FOM] R and the powerset axiom

[Andrej Bauer]

On Thu, May 14, 2009 at 9:50 AM, Arnon Avron <aa at tau.ac.il> wrote:
> I admit that I am not acquainted with the constructions you have cited
> (I thought they are all in the context of constructive mathematics).

Constructive mathematics (of Bishop's, but not intuitionism of
Brouwer's) is consistent with classical mathematics.

> However, I do not understand how a construction of the real "reals"
> (*those that are supposed to correspond in exact way to the points
> on an Euclidean straight line*) can be done without the powerset axiom
> or something equivalent.

Well, that's what those constructions do and so I cited them for your benefit.

Briefly, one way to get at the reals wihtout powersets is as follows.
Assume we can form the following sets: natural numbers, finite
cartesian products, subsets defined by bounded formulas, quotients by
equivalence relations, and exponentials.

The exponential of sets A and B is a set B^A with a function e : (B^A)
x A -> B such that, for every function f : C x A -> B there exists a
unique function g : C -> (B^A), such that e(g(z),x) = f(z,x) for all z
in C and x in A. (In classical mathematics the existence of
exponentials implies the existence of powersets because the powerset
of A is the exponential {0,1}^A, but please bare with me for a
moment.)

With these constructions we can form the reals as follows. First we
form the integers and the rationals Q in the usual way. Then we form
the set C of Cauchy sequences in Q as a subset of Q^N. The set R is
defined a quotient of C by a suitable equivalence relation. With
countable choice we can prove that R is a Cauchy-complete archimedean
ordered field, i.e., what many people call "reals".

If you also happen to believe in classical logic, then you will be
able to construct powersets from exponentials, an issue that is
unrelated to the fact that we constructed R and proved it to have the
desired properties without ever using powersets (and without classical
logic). So our construction works in many models. For example, there
is a topological model in which the construction gives "all" reals
(the ones you want, without holes), automagically equipped with the
Euclidean topology, and there are no powersets in the model.

The relationship between exponentials and powersets, and much more, is
explained in the notes on constructive set theory by Aczel and Rathjen
that I cited.

One could ask the following question: is there a formulation of set
theory with classical logic in which the reals can be constructed but
the powerset of the natural numbers cannot? For the question to make
sense we would first have to find a way of expressing the statement
"reals are complete" that does not  involve talking about arbitrary
bounded subsets of R, or about arbitrary infinite sequences of numbers
(because either of those easily gives the powerset of the naturals
when combined with classical logic).

> As far as I know, without the powerset axiom one cannot prove in ZFC the existence of any
> uncountable set (including the real R).

Well then don't use ZFC if you're unhappy with the powersets :-) There
are many other options out there.

Best regards,

Andrej