From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/617 Path: news.gmane.org!not-for-mail From: categories Newsgroups: gmane.science.mathematics.categories Subject: Re: Challenge from Harvey Friedman Date: Mon, 26 Jan 1998 15:00:15 -0400 (AST) Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241017074 26530 80.91.229.2 (29 Apr 2009 14:57:54 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 14:57:54 +0000 (UTC) To: categories Original-X-From: cat-dist Mon Jan 26 15:00:16 1998 Original-Received: (from cat-dist@localhost) by mailserv.mta.ca (8.8.8/8.8.8) id PAA29830; Mon, 26 Jan 1998 15:00:15 -0400 (AST) Original-Lines: 48 Xref: news.gmane.org gmane.science.mathematics.categories:617 Archived-At: Date: Mon, 26 Jan 1998 12:10:01 +0000 From: Steven Vickers >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.