next up previous
Next: Assignment and Contents Functions Up: Frame axioms using frames Previous: Frame axioms using frames

How to assert n objects distinct with n+1 axioms


Suppose we have n objects tex2html_wrap_inline410 , and we want to assert that they are all distinct. The obvious way to do it is to have tex2html_wrap_inline412 axioms tex2html_wrap_inline414 . We can do it with by writing the axioms tex2html_wrap_inline416 , which comes to n-1 axioms. We then write tex2html_wrap_inline420 and tex2html_wrap_inline422 . This ordering trick permits proving that the tex2html_wrap_inline424 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 tex2html_wrap_inline424 s, and any of the n! total orderings of tex2html_wrap_inline434 will do.

It might be considered more elegant to write functions from the tex2html_wrap_inline437 s to the integers and use the transitivity, etc. of the integers to infer the inequalities. Thus we would write tex2html_wrap_inline438 , 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.

John McCarthy
Thu Jan 30 13:14:14 PDT 1997