From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2324 Path: news.gmane.org!not-for-mail From: Paul B Levy Newsgroups: gmane.science.mathematics.categories Subject: Re: topos logic arising nicely Date: Wed, 4 Jun 2003 16:42:32 +0100 (BST) Message-ID: References: <200306032014.WAA05082@fb04305.mathematik.tu-darmstadt.de> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241018573 3548 80.91.229.2 (29 Apr 2009 15:22:53 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:22:53 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Thu Jun 5 16:09:32 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:09:32 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O00W-0006vR-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:02:40 -0300 In-Reply-To: <200306032014.WAA05082@fb04305.mathematik.tu-darmstadt.de> Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 15 Original-Lines: 16 Xref: news.gmane.org gmane.science.mathematics.categories:2324 Archived-At: On Tue, 3 Jun 2003, Thomas Streicher wrote: > I don't know Isabelle too well BUT in Higher Order Logic one may > well assume inhabitedness of all types when these are built up from > N (and 1) via x,-> and P(-). In higher order logic one cannot form > subtypes in the logical sense and that's the only way how one can > build types that aren't inhabited. "The neglect of sum types is the root of all evil." Paul