Suppose is a semigroup with an operation (written multiplicatively as ““), is a sequence of elements of and is a finite set of natural numbers. We want to define the product of elements given by the indices coming from , i.e. the element expressed by the formula .
It is easy to explain to a human what we want by using the “three dots” notation. Namely, if , then by we mean . However, this will not work with a machine. When doing machine verifiable mathematics we actually have to define what we mean.
Let’s look at the three dots in the expression . This is a list of natural numbers, which can be understood as a function . In ZF set theory for a natural number we have so we can write . We want to list the numbers from in the increasing order, so really is an order isomorphism from to . The key fact that we can rely on is that for linear order relations each two finite sets that have the same number of elements are order isomorphic and the isomorphism is unique. This allows to define the enumeration of a finite set of natural numbers as the unique order isomorphism between the number of elements of and , i.e. . Here is the set of order isomorphisms between a set ordered by relation and set ordered by relation , is the number of elements in (which is a natural number for finite sets) and is the (natural linear) order relation on natural numbers. We are using the formula to extract the only element from a singleton.
This way we can reduce a product over a finite set of indices to the product over a list by defining , where is the unique enumeration of the set .
And to do that we need to prove that any two finite linearly ordered sets admit a unique order isomorphism. That was quite unexpected.
Tags: formalized mathematics