[FOM] From the moderator (was "Constructivism, Geometry, and Powerset")

[Martin Davis]

Dear subscribers,

The thread on "Constructivism, Geometry, and Powerset" seems to have 
become a matter of disputants reiterating their same claims and 
largely talking past one another. Nevertheless  the editors believe 
that a number of interesting issues are being raised. In the interest 
of reaching some kind of clarity I am posting some comments by 
editors. I hope that Avron and Bauer  will post replies that are 
clear and very succinct that can appropriately terminate this thread..

A DIALOG BETWEEN TWO EDITORS:
 >Arnon points out that it is consistent with ZFC-P that all sets are
 >countable.

 >He argues that this invalidates the claim that Bauer proof is not
 >using power in some sense.  And I certainly wonder where the limits
 >of the Cauchy sequences are coming from if not from power set.  In
 >the last post, I think Bauer hid the ball by just positing that
 >there was a complete ordered field.

The limit of  Cauchy sequence is just the Cauchy sequence, whose
existence (in ZFC-P) follows by replacement.

One can prove constructively that, if F is a function on N whose
values are real numbers, then there is a real number not in its range
of values without assuming powerset.

For example, in ZFC-P one can define R, the _class_ of Cauchy
sequences, and prove that it is uncountable in the above sense.


 >On the other hand I have no notion what Avron means when he says `R
 >(the reals in some intuitive sense) can clearly be proved
 >uncountable' -- what are the axioms?

FROM ANOTHER EDITOR:
  It seems to be quite generally agreed that the discussion between
Avron and Bauer (+ Taylor) is not progressing toward understanding.
As far as I can tell, both sides have reasonable ideas (which I'd
like to understand), but the ideas are getting lost in terminological
confusions, and the reasonableness is getting lost in polemics.
         I recall Bauer saying that his R is not (or at least need not be) a
set.  At the time, I thought he wanted it to be a type (or something
like that) instead, but he certainly could have meant for it to be a
proper class.  I'd certainly like to see this point clarified.  More
generally, does his assertion about constructive proofs being
compatible with classical set theory imply that they can be carried
out in ZFC?  And does his claim that he doesn't use the power set
axiom mean that the arguments can be carried out in ZFC minus power set?
         Similarly, I'd like to see a clarification from Avron about his view
(which he claims all humans share) of the Euclidean plane.  For
example, if I choose two points (so as to fix both a particular line
and a unit of distance) and then carry out the traditional
construction of addition and multiplication operations on the points
of that line, will the result be an ordered field?  A complete
ordered field?  If so, should I think of that field as R?  Can I use
it to coordinatize the plane, i.e., to set up the traditional
bijection between the points of the plane and R^2?  If so, do R^2 and
the plane differ only in that some arbitrary choices are needed for
the coordinatization, or is there a more fundamental difference (such
as the plane being something other than a structured collection of
points)?  If the coordinatization fails, what goes wrong?  Do we get
an incomplete field (perhaps just an ordered field with square roots
of all positive elements, perhaps even less)?
         I think answers to questions like these would greatly help to
clarify the situation.

Martin


                           Martin Davis
                    Visiting Scholar UC Berkeley
                      Professor Emeritus, NYU
                          martin at eipye.com
                          (Add 1 and get 0)
                        http://www.eipye.com