Re: intuitionism and disjunction

[Peter Freyd <pjf@saul.cis.upenn.edu>]

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.)