Subject: categories: Re: intuitionism and disjunction

From: Peter Freyd <[email-masked]>
Date: Mon, 27 Feb 2006 08:26:37 -0500 (EST)

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

---

From: Toby Bartels <[email-masked]>
Date: Mon, 27 Feb 2006 11:07:28 -0800

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

>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

---

From: Paul B Levy <[email-masked]>
Date: Mon, 27 Feb 2006 14:09:44 +0000 (GMT)

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 Blain Levy              email: [email-masked]
School of Computer Science, University of Birmingham
Birmingham B15 2TT, U.K.      tel: +44 121-414-4792
http://www.cs.bham.ac.uk/~pbl