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 <http://en.wikipedia.org/w/index.php? title=Disjunction_and_existence_properties&action=history>: it looks like the part before the ellipsis was written by English Wikipedia User Chalst <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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