Steve Vickers wrote
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).
I fully subscribe. UAs are just sloppy about language. Writing a term means to introduce a name. An "entity" may have several names, and a name may fail to denote an "entity". A theory of identity cares for the first phenemenon, a theory of existence for the second. (A look at : D.S.Scott, Identity and Existence in Intutionistic Logic, In: Applications of Sheaves, Proc. Durham, LNiMath 753, 1979, is recommended) Now UA (if not concerned with partial algebra) usually relate introduction of names to an existence statement; whenever they write 'a' there is something which is denoted by 'a', in case of emergency "a" itself (meaning free generation). They stick to this firm belief when considering variables. This is why proofs of the kind b = f(x) = b' (where f : A -> B) go wrong if the interpretation of A does not provide denotations for x.. (Due to the peculiarities of universal quantification not even b = b' is sound). Of course, we may abandon the idea that names denote. Then, please, use a different logic (see Scott). Otherwise, keep a record of the variables, you want to use as suggested by Steve and many other people. Axel Poigne
Imperial Society for the Prevention of Cruelty to Empty Sets.
I subscribe to the society. ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++