Re: Challenge from Harvey Friedman

[categories <cat-dist@mta.ca>]

Date: Mon, 26 Jan 1998 12:10:01 +0000
From: Steven Vickers <s.vickers@doc.ic.ac.uk>

>Topos theory with natural number object is insufficient to develop
>undergraduate real analysis - although many fom postings conceal this fact.
>One has to add to topoi: natural number object, well pointedness, and
>choice. The latter two are nothing more than slavish translations of set
>theory into the topos framework. The "idea" is to take a fatally flawed
>foundational idea and force it to "work" by transporting important ideas
>from set theoretic foundations.

The slavish translation of well pointedness and choice actually arises from
a more subtle slavish translation of point-set topology.

Point-set topology postulates that the points of a topological space can be
comprehended as a set, but this apparently innocuous idea is questionable
(perhaps we should be more sceptical about what sets can comprehend
following our experience with proper classes).

When we formulate our foundations based on the ideas of topos theory, and
interpret "set" as object in an elementary topos, then - given a natural
numbers object - we can ideed construct "sets of reals" but we find that
they misbehave. Normal theorems of analysis, such as Heine-Borel, fail
unless we also impose the additional ideas from set-theoretic foundations.

However, there is a different way of formulating topology, using locales or
"formal spaces", that works in any elementary topos (still need an NNO to
get the reals, of course) and preserves the validity of theorems such as
Heine-Borel. It works by addressing the topology directly, without regard
to what the opens in it might be sets of. It still has a concept of point,
but generalized point with respect to a varying set-theory (stage of
definition) instead in a fixed one. We can't take a single comprehension in
our favourite set-theory as encompassing all the points.

The moral is that a topological space is more than just a set of points
together with a topology of open subsets. If, for any reasons at all, we
are interested in doing mathematics constructively, then we should discard
point-set topology and use locales.

My picture of what is going on is this: when we try to make a set out of a
space by stripping off the topology, we damage the points, and we put the
well-pointedness and choice in as crutches and plasters to try to rectify
the damage we should never have done in the first place.

Steve Vickers.