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

[Andrej Bauer]

I was rather hoping that the topic is closed, but the the moderator
asked me to respond, and so I shall. I will first comment on the
mathematical points that were raised by the members of the editorial
board, thereby making it easy for those who are interested in
mathematics to skip the rest.

>  >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.

The powersets have nothing to do with the construction. I reiterate
that the construction is based on exponentials, not powersets. It may
be a bit unusual to work with exponentials as a primitive notion for
those who are used to set theory, where the existence of exponentials
is typically viewed as a consequence of the existence of powersets. It
is especially confusing in _classical_ set theory, where the existence
of exponentials is equivalent to the existence of powersets (P(A) is
isomorphic to 2^A in classical set theory). You can read more about
powersets vs. exponentials in Aczel & Rathjen notes on constructive
set theory, see my post 013603 from May 10th.

>  >In he last post, I think Bauer hid the ball by just positing that
>  >there was a complete ordered field.

No, I did not. The construction of reals as a quotient of the set of
rational Cauchy sequences gives a complete ordered field. This is not
posited but proved, using countable choice. The proof of completeness
is the usual one: take a sequence of reals, use countable choice to
get a sequence of Cauchy sequences representing them, from that define
a Cauchy sequence that represents their limit.

> 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.

I would just like to point out that this is _not_ the construction I
described, but rather a similar construction in set theory. My
construction is performed in the internal language of a "Pi-pretopos
with natural numbers and countable choice" where there is no
replacement and no distinction between sets and classes. The above
thinking is most similar to how real numbers are treated in
constructive set theory, which can be read about in the first
reference in my May 10 post (Aczel & Rathjen notes on constructive set
theory, section 3.6).

> I recall Bauer saying that his R is not (or at least need not be) a set.

Indeed, in constructive set theory and formal topology, R is a class.
But the construction in the May 16th post is not of that kind.

>  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.

If you are referring to the construction from my May 16th post 013632,
then I can clarify. The construction is to be performed in the
internal language of a Pi-pretopos with natural numbers object and
countable choice. To someone who knows only set theory I would
describe this as a kind of intuitionistic bounded set theory (all
quantifiers are bounded), without powersets, without replacement, but
with exponentials, products, disjoint sums, (bounded) separation, and
quotients. But this is a bit misleading because the internal language
is really a form of type theory because there is no global membership
relation.

The nLab wiki has an overview of various kinds of pretoposes, see
http://ncatlab.org/nlab/show/pretopos

Examples of Pi-pretoposes with natural numbers are: ZFC (after you
make a category out of it), intuitionistic set theory IZF (after you
make a category out of it), any topos with natural numbers, various
realizability models, setoids over dependent type theory (subtle
issues there, need to be careful). I do not know off the top of my
head precisely which variations of constructive set theory CZF give a
pretopos (exponentials?), or whether the classes in CZF form a
pretopos. I am sure there are readers on this list who can answer this
question.

In any of these there is an object R which is a quotient of the object
of rational sequences. R is always an archimedean ordered-field. If
the pretopos satisfies number choice then it is also Cauchy complete.

>  More generally, does his assertion about constructive proofs being
> compatible with classical set theory imply that they can be carried
> out in ZFC?

Yes. ZFC is a Pi-pretopos with natural numbers and countable choice.

> 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?

No, because in ZFC without power set you cannot prove the existence of
exponentials. In particular, you cannot prove that the exponential N^N
exists. I was quite explicit in the May 16th post what is needed, see
http://www.cs.nyu.edu/pipermail/fom/2009-May/013632.html . If after
reading the post it is still unclear how the construction works,
please contact me privately.

> I think answers to questions like these would greatly help to clarify the situation.

I hope that my answers helped. This concludes the mathematical part of
my post. If you wish to discuss any further mathematical points
contact me privately. I will not reply on the FOM list about this
anymore.

I am deeply disappointed by the level of hostility that is often
displayed on FOM. Electronic communication is known to easily cause
unnecessary misunderstanding. If we talked about real numbers over a
couple of beers, we would never need moderator intervention (well
perhaps after 10 beers). Therefore, I urge everyone to be a little
kinder to fellow FOMers.

Lastly, I object to the fact that the moderator published the
following, presumably with the permission of the member of the
editorial board who wrote it:

>In the last post, I think Bauer hid the ball by just positing that
>there was a complete ordered field.

I do not even know who said this, which alone is a problem. Why are
members of the editorial board allowed to post such things
anonymously? I resent the implication that I am trying to trick people
by "hiding the ball".  If even a member of the editorial board thinks
that the members of FOM write in bad faith, then FOM is in a sad state
indeed.

With kind regards,

Andrej