Subject: categories: intuitionism and disjunction

From: Peter Freyd <[email-masked]>
Date: Sun, 26 Feb 2006 11:18:45 -0500 (EST)

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.

---

From: Paul B Levy <[email-masked]>
Date: Mon, 27 Feb 2006 03:00:04 +0000 (GMT)

Dear Peter.

> existence

Can you explain the "of course" here, please?  What were these reasons,
and do they still hold water? I would have thought that tuples pose
less of an ontological difficulty than functions.

> there's this reason: if by a *bi*cartesian closed category one were to
> mean a ccc category whose dual is also ccc

What I meant was cartesian closed category with finite coproducts.

> then one would be stuck with that fact that all *bi*cartesian closed
> categories are just pre-ordered sets.
>

I don't know what you mean - maybe that product types are more similar to
function types than sum types are?  If so, I agree, but I was comparing
function types with sum types, not (function and sum) with (function and
product).

Paul