From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3046 Path: news.gmane.org!not-for-mail From: Peter Freyd Newsgroups: gmane.science.mathematics.categories Subject: Re: intuitionism and disjunction Date: Mon, 27 Feb 2006 08:26:37 -0500 (EST) Message-ID: <200602271326.k1RDQb3K008051@saul.cis.upenn.edu> NNTP-Posting-Host: main.gmane.org X-Trace: ger.gmane.org 1241019063 7024 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:34:00 2006 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 27 Feb 2006 09:34:00 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.52) id 1FDiV8-0005uK-4c for categories-list@mta.ca; Mon, 27 Feb 2006 09:33:22 -0400 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 29 Original-Lines: 23 Xref: news.gmane.org gmane.science.mathematics.categories:3046 Archived-At: 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.)