From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2337 Path: news.gmane.org!not-for-mail From: Hendrik Tews Newsgroups: gmane.science.mathematics.categories Subject: Re: topos logic arising nicely Date: Fri, 6 Jun 2003 11:29:15 +0200 Message-ID: <16096.24299.686053.329698@ithif51.inf.tu-dresden.de> References: <200306051108.NAA00738@fb04209.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 1241018589 3659 80.91.229.2 (29 Apr 2009 15:23:09 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:23:09 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Fri Jun 6 17:21:04 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Jun 2003 17:21:04 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19ONcO-0004L7-00 for categories-list@mta.ca; Fri, 06 Jun 2003 17:15:20 -0300 In-Reply-To: <200306051108.NAA00738@fb04209.mathematik.tu-darmstadt.de> X-Mailer: VM 7.14 under Emacs 21.2.1 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 28 Original-Lines: 30 Xref: news.gmane.org gmane.science.mathematics.categories:2337 Archived-At: Hi, Thomas Streicher writes: Date: Thu, 5 Jun 2003 13:08:14 +0200 (CEST) Subject: categories: Re: topos logic arising nicely But I would be surprised if HOL has subtype formation as from a logical point of view subtypes are neither necessary nor convenient. Adding subtypes is only necessary for getting a topos out of a model of HOL. I don't know, if I miss the point here. However, PVS has a HOL system with predicate subtypes. And it is _very very_ convenient (because of the predicate subtypes). I don't know if it is a necessity, but the absence of subtypes in Isabelle/HOL leads to a representation of partial functions, that allows you to prove unexpected results. Despite what the Isabelle tutorial says at page 187, you _can_ prove hd [] = last [] (saying that the head of the empy list equals its last element) Bye, Hendrik