From mboxrd@z Thu Jan 1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3049
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 14:09:44 +0000 (GMT)
Message-ID:
References: <200602271326.k1RDQb3K008051@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 1241019065 7038 80.91.229.2 (29 Apr 2009 15:31:05 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 29 Apr 2009 15:31:05 +0000 (UTC)
To: categories@mta.ca
Original-X-From: rrosebru@mta.ca Mon Feb 27 19:30:38 2006 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 27 Feb 2006 19:30:38 -0400
Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.52)
id 1FDrgf-0000FA-Pv
for categories-list@mta.ca; Mon, 27 Feb 2006 19:21:53 -0400
In-Reply-To: <200602271326.k1RDQb3K008051@saul.cis.upenn.edu>
Original-Sender: cat-dist@mta.ca
Precedence: bulk
X-Keywords:
X-UID: 32
Original-Lines: 41
Xref: news.gmane.org gmane.science.mathematics.categories:3049
Archived-At:
I agree that intuitionistic logic satisfies the disjunction property.
But I don't see why this should make disjunction a more peripheral part of
intuitionistic logic than implication.
Paul
> Paul Levy asks how the original intuitionists viewed disjunction. I
> don't know how to say it better than this paragraph from Wikipedia
> (anyone know who wrote it?).
>
> The disjunction and existence properties are validated by
> intuitionistic logic and invalid for classical logic; they are key
> criteria used in assessing whether a logic is constructive.... The
> disjunction property is a finitary analogue, in an evident sense.
> Namely given two or finitely many propositions P_i, whose
> disjunction is true, we want to have an explicit value of the index
> i such that we have a proof of that particular P_i. There are quite
> concrete examples in number theory where this has a major effect.
>
> It is a (meta)theorem that in free Heyting algebras and free topoi
> (and all sorts of variations thereon) that the disjunction property
> holds. In the free topos that translates to the statement that the
> terminator, 1, is not the join of two proper subobjects. Together with
> the existence property it translates to the assertion that 1 is an
> indecomposable projective object -- the functor it represents (i.e.
> the global-section functor) preserves epis and coproducts. (And with
> a little more work one can show it also preserves co-equalizers.)
>
>
>
--
Paul Blain Levy email: pbl@cs.bham.ac.uk
School of Computer Science, University of Birmingham
Birmingham B15 2TT, U.K. tel: +44 121-414-4792
http://www.cs.bham.ac.uk/~pbl