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