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