Let Numbers be the signature whose sort is with operations which we will call , defined over these sets. At this point we must remind ourselves that a signature is a syntactic structure; as yet we have assigned no meaning to it. Our intuition is already several steps ahead; we know what we mean by , and so on, and it is, of course, this intuition which motivates the whole subject. Nevertheless, whilst this helps us in our understanding of what we are doing and why, we must keep a tight rein on it; we must, for the time being, pretend we do not yet have a notion of meaning. We could just as easily have named the sorts in S, X and Y and the operations in etc. This would retain the strictly `meaningless' quality of the syntax until we were ready to talk about semantics; it might also make it easier to accept the somewhat less obvious semantic possibilities which we shall see later on.
We can think of the operations in our signature as a family of sets indexed by arity, w, and sort, s. Informally, the arity of an operation refers to the number and sorts of the operands and the sort refers to the result. So, for instance, we may define the operation add to be of arity and sort Nat; in OBJ-style notation,
The pair w,s is called the rank of the operation. There may well be other operations in of the same rank as add: mult, for example. So then add and mult will belong to the same member of the family, namely . We can write
Similarly, we may have
This covers all the operations named above. However, it is usual to regard the constants of each sort as operations; they are, in a sense, results without operands, so their arity is denoted by ` ' or ` ' to indicate this. So, for instance, should we decide to name the constants of Bool T and F, and the constant in Nat zero, we have
At this point we might be tempted to think we had finished, since we seem to have covered everything, but in fact the family is an infinite set of sets . Some more examples are , and so on. We have not named any operations of these ranks, however, so these sets are empty. We can now put the whole signature together as follows:
A friendlier version of the same signature is:
The constant zero together with the operation succ are called the constructors of the sort Nat; similarly, T and F are constructors of Bool.