Dear Vaughan,

[Executive summary: Yes.]

The banning of empty carriers is historically a part not only of
algebra, but also more generally of model theory in logic.

I haven't investigated the history, but it must surely derive from
examples such as the following.

1. (all x) P(x) |- (exists x) P(x) is provable according to the rules
of first order logic, but is unsound if empty carriers are allowed.
(Michel Hebert mentioned this in his message.)

2. Consider a many-sorted algebraic theory with two sorts S and T,
with a unary operation f: S -> T, two constants a and b of sort T,
and equational laws f(x) = a and f(x) = b. From transitivity (and
symmetry) of =, we deduce a = b, which does not necessarily hold in
an algebra with empty carrier for S.

In both examples, the syntactic proofs arise from an unrestricted
licence to introduce a free variable x. This tacitly assumes that all
the variable symbols denote, and so that all the carriers are non-empty.

Thus my understanding is that the semantics were fine-tuned (ban
empty carriers) to match a feature of the logical syntax (admit
arbitrary use of free variables).

In constructive logic, banning emptiness becomes much more
problematic and early on (Mostowski, as I understand the history)
constructive logic fine-tuned the syntax to match a semantics that
admits empty carriers. One technique is for each sequent to specify
its particular stock of free variables. Then (all x) P(x) |- (exists
x) P(x) is provable in the presence of a free variable a, and is
sound in any model in which a is given an interpretation.

Thus the practice did not particularly arise in category theory,
though both the problem and the solution are just as important in
categorical logic.

The basic problem is the mismatch between unrestricted free variables
in the syntax, and unrestricted carriers in the semantics.

The experience from constructive mathematics shows us that there
always were two solutions:

(1) modify the semantics by banning empty carriers (the traditional
approach), or
(2) modify the syntax to control use of free variables.

It seems to me that by now the evidence is overwhelming that approach
(2) gives more elegant mathematics and (1) was a blind alley.
Constructive and categorical logic are two examples of this, but the
initial algebra theorem is an excellent example in more mainstream
mathematics. In (2) it can be stated simply, while in (1) it is
overwhelmed by side conditions that exist only to avoid empty
carriers. My recent paper with Palmgren on initial algebras for
essentially algebraic theories could not have been written sensibly
in approach (1).

It would be interesting to hear of examples where (1) works more neatly.

By the way, the reference to monads in -
> In category theory the initial algebra can be found equivalently
> either
> in the Kleisli category of a monad (consisting of the free algebras of
> the variety) as the free algebra on no generators, or in the
> Eilenberg-Moore category of that monad (consisting of the whole
> variety)
> as the algebra whose underlying set consists of the constants.
>
limits the field to single-sorted algebraic theories if you expect
the monad to be on the category of sets.

All the best,

Steve.