Saunders MacLane wrote that -

The "empty algebra" has been proscribed in UA. Since there is now occasion to consider models of algebras not just in sets (possibly in topoi or in regular categories) this early proscription seems too narrow.

Hear, hear! Even in classical sets, the exclusion of empty carriers gets remarkably messy when you deal with many-sorted algebras. There are well-known paradoxes in the logic (e.g. apparent failures of the transitive law) when empty carriers are allowed, but the constructivists have shown us how to reason cleanly by labelling each sequent or equation with a list of the free variables that are being used (if there are any, then the algebra must be inhabited by the interpretations of those free variables). In our first year logic course we teach natural deduction in a form in which for forall-elimination and exists-introduction, the terms used cannot contain freely invented variables - they must be made up from those posed in the problem or introduced for forall-intro or exists-elim. (We use nested boxes to mark the scopes of these introduced variables.) This is sound even for empty carriers, and it's my belief that the restricted rules are easier to understand than the unrestricted ones. Steve Vickers --------------------------------------------------------------------------- President, Imperial Society for the Prevention of Cruelty to Empty Sets. ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++