From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3045 Path: news.gmane.org!not-for-mail From: Paul B Levy Newsgroups: gmane.science.mathematics.categories Subject: Re: intuitionism and disjunction Date: Mon, 27 Feb 2006 03:00:04 +0000 (GMT) Message-ID: References: <200602261618.k1QGIjNW003204@saul.cis.upenn.edu> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241019063 7020 80.91.229.2 (29 Apr 2009 15:31:03 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:31:03 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Mon Feb 27 09:33:16 2006 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 27 Feb 2006 09:33:16 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.52) id 1FDiRU-0005b7-0X for categories-list@mta.ca; Mon, 27 Feb 2006 09:29:36 -0400 In-Reply-To: <200602261618.k1QGIjNW003204@saul.cis.upenn.edu> Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 28 Original-Lines: 37 Xref: news.gmane.org gmane.science.mathematics.categories:3045 Archived-At: Dear Peter. > I see no reason to regard disjunction as more "peripheral" to > intuitionistic logic than implication. (And, likewise, no reason to > regard sum types as more peripheral to simple type theory than function > types.) Does anybody disagree? > > The original intuitionists did, of course, see such reasons. But for > those who don't care about such issues as the nature of mathematical > existence Can you explain the "of course" here, please? What were these reasons, and do they still hold water? I would have thought that tuples pose less of an ontological difficulty than functions. > there's this reason: if by a *bi*cartesian closed category one were to > mean a ccc category whose dual is also ccc What I meant was cartesian closed category with finite coproducts. > then one would be stuck with that fact that all *bi*cartesian closed > categories are just pre-ordered sets. > > The status of disjunction and sum types in the presence of function > types is, indeed, significantly different from the status of > conjunction and products types. I don't know what you mean - maybe that product types are more similar to function types than sum types are? If so, I agree, but I was comparing function types with sum types, not (function and sum) with (function and product). Paul