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