From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2307 Path: news.gmane.org!not-for-mail From: Till Mossakowski Newsgroups: gmane.science.mathematics.categories Subject: Re: Topos logic arises naturally Date: Fri, 30 May 2003 16:37:13 +0200 Message-ID: <3ED76C99.1020801@informatik.uni-bremen.de> References: <3ED34194.9050005@informatik.uni-bremen.de> <002801c326a1$05dc0000$f112fea9@essex.ac.uk> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241018563 3470 80.91.229.2 (29 Apr 2009 15:22:43 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:22:43 +0000 (UTC) To: Categories Original-X-From: rrosebru@mta.ca Fri May 30 23:18:07 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 30 May 2003 23:18:07 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19Lvsv-0002Kc-00 for categories-list@mta.ca; Fri, 30 May 2003 23:14:17 -0300 User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.3) Gecko/20030313 X-Accept-Language: en-us, en In-Reply-To: <002801c326a1$05dc0000$f112fea9@essex.ac.uk> Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 57 Original-Lines: 85 Xref: news.gmane.org gmane.science.mathematics.categories:2307 Archived-At: I did not want to deny the need of mathematical thought, but I found this example of topos theory emerging unexpectedly quite pleasing. Note that the mail is *not* about Isabelle. Admittedly, I do not know anything about the quoted system HOL light, so I have not verified Slind's claim. Till Elwood Wilkins wrote: > Isabelle's internal logic is not constructive. The existential clause of the > BHK-interpretation is violated so that a consquence of "all unicorns have > horns" is that "some unicorn has a horn". The moral (biased towards > theorists): software engineering considerations are not enough, a coherant > philosophy of mathematics is also needed. > > Elwood > > ----- Original Message ----- > From: Till Mossakowski > To: Categories > Sent: Tuesday, May 27, 2003 11:44 AM > Subject: categories: Topos logic arises naturally > > > >>You see: even with just aesthetic and software engineering >>considerations you are eventually lead to topos logic... >> >>-- >>Till Mossakowski Phone +49-421-218-4683 >>Dept. of Computer Science Fax +49-421-218-3054 >>University of Bremen till@tzi.de >>P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till >> >>Message-Id: <200305270616.h4R6G3w8008134@plxc2089.pdx.intel.com> >>To: Randy Pollack >>cc: John Harrison , isabelle-users@cl.cam.ac.uk >>Subject: Re: HOL without description operators >>Date: Mon, 26 May 2003 23:16:03 -0700 >>From: John R Harrison >>Sender: Larry Paulson >> >>Hi Randy, >> >>| Perhaps more usefully, how do you suggest I do this task of developing > > HOL > >>| without description operators. >> >>You might find it interesting to look at HOL Light. This gives a >>different axiomatization of the HOL logic, developed precisely because I >>was dissatisfied with the one in the original HOL system, on which I >>believe the Isabelle/HOL logic is based. >> >>Although I do eventually introduce the description operator, quite a lot >>of the basic logic --- including the automation of inductive definitions >>--- is developed without it (and indeed without excluded middle or >>extensionality). You may find it a more congenial starting-point. >> >>As Konrad Slind later pointed out, what I settled on is remarkably close >>to the internal logic of a topos, as presented for example in Lambek and >>Scott's book. This was a surprise to me since at that time I knew next to >>nothing about toposes and was motivated by a mixture of aesthetic and >>software engineering considerations. >> >>Cheers, >> >>John. >> >> >> >> -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till