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.

In IsarMathLib we are able to define a product of a list of elements of a semigroup using the the notion of Fold. So, if we know what is . How can we generalize it for any finite set of indices?

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.

### Like this:

Like Loading...

*Related*

Tags: formalized mathematics

This entry was posted on August 24, 2008 at 5:04 pm and is filed under news, Proofs. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

September 27, 2008 at 12:54 am |

[…] with the same number of elements are order-isomorphic and the isomorphism is unique. I have written previously on the motivation for this. The theorem was surprisingly tedious to prove and required about 50 […]

March 20, 2009 at 2:47 am |

It looks like you still have more work to do to formalize something like

(lambda x1 … xn. f(x1, …, xn)) == (lambda x1. (lambda x2. (… (lambda xn. f(x1, …, x2)) …)).

(Seen here.)

BTW, I responded to your comment at my site.

March 20, 2009 at 9:14 pm |

Note that IsarMathLib is is based on ZF set theory, not lambda calculus. I don’t know lambda calculus, so I can’t even think about some sort of analogous statement in set theory. But I always wanted to learn something about l. c., so thanks for the link.

March 20, 2009 at 10:41 pm |

I think the idiom is general to all nested structures, of which there are plenty in ZF. For instance, if I wanted to talk about the representation of the natural n, I could write the set (using underscore as subscript, 0 as empty set)

{_1 {_2 … {_n 0 } … } }

March 20, 2009 at 11:24 pm |

But the expression (in the first comment) you wrote is an identity between two forms of such nested structure. Could you write what would be such identity for the natural numbers? Perhaps one more example (with functions?) so that I can have a better feel for the analogy?

March 21, 2009 at 12:28 am |

Hmm. I’m not sure if this is what you’re looking for, but I suppose one could define a function to convert a natural number to a pair of natural numbers, like so:

f(n) ==

f({_1 {_2 … {_n 0 } … } }) ==

Where a pair is defined appropriately.

March 21, 2009 at 1:40 am |

Oh my, it looks like my angle brakets were all eaten and such.

March 21, 2009 at 12:45 pm |

It is best to use LaTeX markup like this: (dollar sign)latex some formula (dollar sign).

The dollar sign should be without parentheses of course and there should be no space between the opening dollar sign and the “latex” word.

March 21, 2009 at 3:09 pm |

Hmm, I’m not so familiar with latex, but I’ll give it a shot.

You can delete the superfluous comments. (No preview!)

March 21, 2009 at 6:45 pm |

I see what you mean. But what would it mean to formalize this? Normally it would mean “invent a notation for this that doesn’t use three dots and prove some properties that informally would be written with three dots”. For example instead of (informal)

we could have formal notation that would replace and prove something like .

In case of natural numbers such thing is already done in Isabelle/ZF. Natural numbers are defined in the way standard for ZF set theory as sets built from the empty set with the nested structure like you write in your comment. There are lots of theorems proven about those sets (natural numbers).