Re: intuitionism and disjunction

[Toby Bartels <toby+categories@math.ucr.edu>]

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