Suppose we have *n* objects , and we want to assert
that they are all distinct. The obvious way to do it is to have
axioms . We can do it with by
writing the axioms , which
comes to *n*-1 axioms. We then write and . This ordering trick permits
proving that the s are all distinct. The transitivity of <
lets us infer the *n*(*n*-1) inequalities we want. Notice that the
ordering has no relation to any properties of of the s, and any
of the *n*! total orderings of will do.

It might be considered more elegant to write functions from the
s to the integers and use the transitivity, etc. of the integers
to infer the inequalities. Thus we would write , which comes to *n* equations.
The index functions are arbitrary, because all they have to do is
assign different indexes to different objects.

Within a computer program, we may give the objects names, e.g. write
equations *name*(*Fido*) = "*Fido*", etc. and rely on the computer to
assert that the strings "Fido", "Rover", etc. are distinct.

When we have only a few objects, it isn't too much trouble to write the inequalities directly.

Thu Jan 30 13:14:14 PDT 1997