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