From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2316 Path: news.gmane.org!not-for-mail From: Lawrence Paulson Newsgroups: gmane.science.mathematics.categories Subject: Re: Topos logic arises naturally Date: Tue, 3 Jun 2003 10:24:35 +0100 Message-ID: <30CB5DA5-95A5-11D7-BEF0-00039384D4B8@cam.ac.uk> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 (Apple Message framework v552) Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241018569 3511 80.91.229.2 (29 Apr 2009 15:22:49 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:22:49 +0000 (UTC) To: Categories Original-X-From: rrosebru@mta.ca Tue Jun 3 12:03:03 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Jun 2003 12:03:03 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19NDEl-0001wJ-00 for categories-list@mta.ca; Tue, 03 Jun 2003 11:58:07 -0300 X-Mailer: Apple Mail (2.552) Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 6 Original-Lines: 25 Xref: news.gmane.org gmane.science.mathematics.categories:2316 Archived-At: > -----Original Message----- > From: Elwood Wilkins [mailto:elwood@essex.ac.uk] > Sent: Friday, May 30, 2003 4:35 AM > To: Categories > Subject: categories: Re: Topos logic arises naturally > > 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. 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. However, even their full system is unacceptable to many constructivists because it is impredicative. Constructive theories, like a certain commuting diagrams package, have a surprising tendency to "time out". Larry Paulson