From mboxrd@z Thu Jan  1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2320
Path: news.gmane.org!not-for-mail
From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
Newsgroups: gmane.science.mathematics.categories
Subject: Re: topos logic arising nicely
Date: Tue, 3 Jun 2003 22:14:04 +0200 (CEST)
Message-ID: <200306032014.WAA05082@fb04305.mathematik.tu-darmstadt.de>
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 1241018571 3527 80.91.229.2 (29 Apr 2009 15:22:51 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 29 Apr 2009 15:22:51 +0000 (UTC)
To: categories@mta.ca
Original-X-From: rrosebru@mta.ca Wed Jun  4 12:14:48 2003 -0300
Return-path: <cat-dist@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 04 Jun 2003 12:14:48 -0300
Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10)
	id 19NZpw-0003IR-00
	for categories-list@mta.ca; Wed, 04 Jun 2003 12:06:00 -0300
X-Mailer: ELM [version 2.4ME+ PL66 (25)]
X-MailScanner: Found to be clean
Original-Sender: cat-dist@mta.ca
Precedence: bulk
X-Keywords: 
X-UID: 10
Original-Lines: 23
Xref: news.gmane.org gmane.science.mathematics.categories:2320
Archived-At: <http://permalink.gmane.org/gmane.science.mathematics.categories/2320>

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.
Of course, even if type sigma is inhabited from

    (1)   \forall x:\sigma. A(x)->B

one must not conclude

    (2)   \exists x:\sigma. A(x) /\ B

BUT only

    (3)  \exists x:\sigma. A(x) -> B

BTW concluding (2) from (1) is false also classically.

Thomas