Gyula Lakos’s paper that I plan to formalize for IsarMathLib uses a natural generalization of interval arithmetic to abelian group setting. In this post I will go over section 2.A “Algebraic sums” in this paper, quoting it as needed and tell how I want to formalize the notions defined there.
The first step in every formalization is to make things more precise. This consists of guessing what the author of informal text is trying to say, filing in the gaps and working around the errors. It is also a good idea to try to generalize the material as much as possible. It is a bit more work this way, but it pays in the long term.
2.1. Definition. Let be a commutative group.
a.) Suppose that is a countable indexed family of elements of . Assume that for all except for finitely many. Only in that case we define the algebraic sum as any finite sum consisting all the nonzero elements.
Like most definitions in informal math this definition starts with an assumption. In Isabelle/ZF however definitions do not have assumptions, only theorems and locales do. This was surprising to me at the beginning, but later I realized that such assumptions are only hints on the context a definition is intended to be used. There is no reason to put such assumptions in the formal text of the definitions, they will be included in the theorems when needed. They are still useful though as (informal) comments accompanying the definition.
The “indexed family” in the quote above is just a fancy name for a function. Since the cardinality of plays no role in the definition, we will just discard that “countable” assumption. So suppose we have a function . This function is equal to zero everywhere except possibly finitely many points . The set of arguments for which a function is not zero is sometimes called the support of the function and denoted . IsarMathLib includes some theorems on functions with finite support that we can use.
Now we take “any” sum of those nonzero values. The word “any” comes from the fact that we can add the nonzero elements in different order. Since the operation is commutative clearly it does not matter in which order we add the elements. However, this is quite hard to prove.
IsarMathLib provides a setup for adding elements of a list, where lists are functions from to some (semi)group . Since in ZF set theory for we have we can say that a list of elements of is a function . IsarMathLib allows then to define the sum of elements of such list, let’s denote it .
Now we can formalize the word “any” and define the sum over some set in the following way:
Let’s see what is going on in this definition. We intend to use it for finite sets. In such case (the number of elements in ) is a natural number and there are some bijections from (remember natural numbers are sets) to . Hence is a list of the group elements and is a well defined element of the group. Moreover, because of commutativity of the group operation the value of is the same for all , where denotes the space of bijections from to . This means that is a singleton and we can use the formula to extract its only element.
b.) More generally, suppose is a countable indexed family of subsets of . Assume that for all $\lambda \in \Lambda$ except for finitely many. Only in that case
we define the algebraic sum as except for finitely many .
The meaning of this definition is obfuscated by the fact that is bound in the formula, but is referred to later outside of its scope. This a very common and annoying mistake in informal mathematics. My best guess here is that now we have a function valued in the powerset (set of subsets) of and we consider functions such that for all (choice functions) with finite support. Then we use the notion of sum defined earlier to define the set of all possible sums of such functions over their support sets.
This is when I realized that I have to start over. Unless we know that is finite we need some form of axiom of choice to assert that choice functions exist and the result of summing up the sets is not empty. We are dealing with finite sets all the time, I am sure there is a way to formulate the definitions so that we don’t need the Axiom of Choice so soon. In addition we have to rethink the role zero plays in the all this. Do we really need a monoid, or we can do this with a semigroup? We need a Pass 2.