intuitionism and disjunction

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

Paul Levy writes

  ...a model of intuitionistic logic is a *bi*cartesian closed category.

  I see no reason to regard disjunction as more "peripheral" to
  intuitionistic logic than implication.  (And, likewise, no reason to
  regard sum types as more peripheral to simple type theory than function
  types.)  Does anybody disagree?

The original intuitionists did, of course, see such reasons. But for
those who don't care about such issues as the nature of mathematical
existence there's this reason: if by a *bi*cartesian closed category
one were to mean a ccc category whose dual is also ccc then one would
be stuck with that fact that all *bi*cartesian closed categories are
just pre-ordered sets.

The status of disjunction and sum types in the presence of function
types is, indeed, significantly different from the status of
conjunction and products types.

Let me take the occasion to record a factoid I don't think I ever had
an excuse to record before (and don't really have one now). Define the
notion of a Heyting semi-lattice (HSL) by removing disjunction and
bottom from the definition of Heyting algebra. Define a _linear_ HSL
as one that satisfies the further equation

    ((x -> y) -> z) ^ ((y -> x) -> z)  =  z

e.g. any linearly ordered set with top (indeed, every linear HSL is
representable as a sub HSL of a product of linear ones).

In a linear HSL one may construct disjunction as

    ((x -> y) -> y) ^ ((y -> x) -> x)

The factoid of interest is this sort-of converse: the only HSL
varieties in which every member is a lattice are varieties of linear
HSLs.