From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2318 Path: news.gmane.org!not-for-mail From: Todd Wilson Newsgroups: gmane.science.mathematics.categories Subject: Re: Topos logic arises naturally Date: Tue, 3 Jun 2003 09:04:05 -0700 Message-ID: <16092.50933.427818.743898@localhost.localdomain> References: <30CB5DA5-95A5-11D7-BEF0-00039384D4B8@cam.ac.uk> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241018570 3520 80.91.229.2 (29 Apr 2009 15:22:50 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:22:50 +0000 (UTC) To: Categories Original-X-From: rrosebru@mta.ca Tue Jun 3 16:55:07 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Jun 2003 16:55:07 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19NHqi-0004ah-00 for categories-list@mta.ca; Tue, 03 Jun 2003 16:53:36 -0300 In-Reply-To: <30CB5DA5-95A5-11D7-BEF0-00039384D4B8@cam.ac.uk> X-Mailer: VM 7.07 under 21.4 (patch 8) "Honest Recruiter" XEmacs Lucid Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 8 Original-Lines: 22 Xref: news.gmane.org gmane.science.mathematics.categories:2318 Archived-At: On Tue, 3 Jun 2003, Lawrence Paulson wrote: > Isabelle's internal logic comes from Lambek and Scott. It is an > instance of Example 1.1 on page 132, where all types are assumed to be > non-empty. But this is the heart of the matter. There is a certain precise sense in which what happens in a topos between the empty set and a singleton set governs the behavior of the rest of the topos. Instead, why not factor out the topos logic and add whatever nonemptiness assumptions that are perceived necessary from a practical standpoint as an additional theory? This factoring shouldn't affect those that rely on the non-emptiness assumptions, but it would make a big difference to those who want to work in the topos logic. -- Todd Wilson A smile is not an individual Computer Science Department product; it is a co-product. California State University, Fresno -- Thich Nhat Hanh