From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3048 Path: news.gmane.org!not-for-mail From: Toby Bartels Newsgroups: gmane.science.mathematics.categories Subject: Re: intuitionism and disjunction Date: Mon, 27 Feb 2006 11:07:28 -0800 Message-ID: <20060227190727.GA23248@math-rs-n03.ucr.edu> 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 1241019064 7035 80.91.229.2 (29 Apr 2009 15:31:04 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:31:04 +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 1FDrj5-0000PE-C8 for categories-list@mta.ca; Mon, 27 Feb 2006 19:24:23 -0400 Content-Disposition: inline Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 31 Original-Lines: 48 Xref: news.gmane.org gmane.science.mathematics.categories:3048 Archived-At: Peter Freyd wrote: >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?). >>From the editing history : it looks like the part before the ellipsis was written by English Wikipedia User Chalst , who is apparently Charles Stewart, a postdoc at the International Centre for Computational Logic; and the rest was written by English Wikipedia User Charles Matthews , who is now a hobbyist but was once an academic mathematician. (I'm familiar with Charles Matthews and trust him, if my opinion matters to anybody; I don't know Chalst.) Of course, either may have copied from somewhere else without proper attribution (that's been common ~within~ Wikipedia --that is copying or moving from one WP article to another-- but it's pretty rare ~into~ Wikipedia, in my experience.) > 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.) I'm not sure how this affects Paul Levy's point, but I guess that I'll let Paul speak on that. -- Toby