From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1489 Path: news.gmane.org!not-for-mail From: Wilkins E B Newsgroups: gmane.science.mathematics.categories Subject: Re: Osius' set theory Date: Wed, 19 Apr 2000 16:52:05 +0100 Organization: University of Essex Message-ID: <38FDD625.A3AD2CB4@essex.ac.uk> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 X-Trace: ger.gmane.org 1241017872 31492 80.91.229.2 (29 Apr 2009 15:11:12 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:11:12 +0000 (UTC) To: Category mailing list Original-X-From: rrosebru@mta.ca Thu Apr 20 14:57:23 2000 -0300 Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA04844 for categories-list; Thu, 20 Apr 2000 14:52:52 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: Mozilla 4.6 [en] (X11; I; Linux 2.2.14 i686) X-Accept-Language: en Original-Sender: cat-dist@mta.ca Precedence: bulk Original-Lines: 49 Xref: news.gmane.org gmane.science.mathematics.categories:1489 Archived-At: Paul Taylor wrote: > > Gerhard Osius's work was significant in 1974 as one of the ways in which > it was shown that toposes do the same thing as set theory. Osius showed that well-pointed topoi do essentially the same thing as set theory. I have yet to find any adequate analogy between what elementary topoi in general do and set theory. The problem being, as far as I can see, that classical set theory finds it very difficult to describe the rather more subtle behaviour occurring in the initial topos. Whence the standard set theoretic account of topos logic includes the assumption that bound variables denote, which make the semantics of elementary topoi almost identical to those of well-pointed ones (for instance every proper subtype of 1 is treated as though it is empty!). > In fact Osius's > is, so far as I am aware, the only work that discusses *set* theory - > Benabou, Joyal, Mitchell, Lawvere etc showed that toposes do the same thing > as some form of *type* theory. Of course, it is the latter that > mathematicians actually use when they claim to be using set theory > as foundations ... In practice this is true, but not if they're interested in actually studying the foundations of maths. My (set minded) colleagues point out (quite forcibly) that unless something is expressible in ZF (say) then they find it hard to accept, a view that appears to be widespread in the theoretical end of computer science. Now I have the practical problem of convincing people that what I do constructively is better than what they do with their "bound variables denote" assumptions, and an axiomatic set theory equivalent to the initial topos would make this much easier: they could go away contentedly believing that I'm really doing set theory (while I can be happy with the knowledge that they're doing typed theory). There are potential applications to category theory from producing a set theory. For instance one might speculate that this set theory could replace the rather cumbersome Freyd cover in the proof of the constructive properties of the initial topos. A host of other speculations can be formulated ... Elwood -- Dr Elwood Wilkins e-mail: elwood@essex.ac.uk Senior Research Officer tel: (+44) (0)1206 872336 Department of Computer Science fax: (+44) (0)1206 872788 University of Essex, Colchester, Essex, UK