Interval arithmetic in groups: Pass 1

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 \mathcal{V} be a commutative group.
a.) Suppose that \{a_\lambda \}_{\lambda \in \Lambda} is a countable indexed family of elements of \mathcal{V}. Assume that a_\lambda = 0 for all \lambda \in \Lambda except for finitely many. Only in that case we define the algebraic sum \sum_{\lambda} a_\lambda 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 \Lambda plays no role in the definition, we will just discard that “countable” assumption. So suppose we have a function a: \Lambda \rightarrow \mathcal{V}. This function is equal to zero everywhere except possibly finitely many points \lambda \in \Lambda. The set of arguments for which a function f is not zero is sometimes called the support of the function and denoted \text{supp}(f). 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 \{ 0,1,..., n-1\}, n \in \mathbb{N} to some (semi)group G. Since in ZF set theory for n \in \mathbb{N} we have n = \{ 0,1,..., n-1\} we can say that a list b of n elements of G is a function b: n \rightarrow G. IsarMathLib allows then to define the sum of elements of such list, let’s denote it \sum b.

Now we can formalize the word “any” and define the sum \sum_A a over some set A\subseteq \Gamma in the following way:

\sum_A a = \bigcup \{\sum a\circ b: b \in \text{bij}(|A|,A)\}

Let’s see what is going on in this definition. We intend to use it for finite sets. In such case |A| (the number of elements in A) is a natural number and there are some bijections b from |A| (remember natural numbers are sets) to A. Hence a \circ b is a list of the group elements and \sum a\circ b is a well defined element of the group. Moreover, because of commutativity of the group operation the value of \sum a\circ b is the same for all b \in \text{bij}(|A|,A), where \text{bij}(X,Y) denotes the space of bijections from X to Y. This means that \{\sum a\circ b: b \in \text{bij}(|A|,A)\} is a singleton and we can use the formula \bigcup \{ x\} = x to extract its only element.

b.) More generally, suppose \{ A_\lambda \}_{\lambda \in \Lambda} is a countable indexed family of subsets of \mathcal{V}. Assume that 0 \in A_\lambda for all $\lambda \in \Lambda$ except for finitely many. Only in that case
we define the algebraic sum \sum_{\lambda \in \Lambda } A_\lambda as \{ \sum_{\lambda \in \Lambda } a_\lambda : a_\lambda \in A_\lambda , a_\lambda = 0 \text{ for all } \lambda  \in \Lambda except for finitely many \}.

The meaning of this definition is obfuscated by the fact that \lambda is bound in the \sum_{\lambda \in \Lambda } a_\lambda 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 A:  \Lambda \rightarrow \text{Pow} (\mathcal{V}) valued in the powerset (set of subsets) of \mathcal{V} and we consider functions a : \Lambda \rightarrow \mathcal{V} such that a_{\lambda}  \in  A_{\lambda} for all \lambda   \in \Lambda (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 \Lambda 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.


Tags: ,

2 Responses to “Interval arithmetic in groups: Pass 1”

  1. Interval arithmetic in groups - pass 2 « Formalized Mathematics Says:

    […] arithmetic in groups – pass 2 By slawekk This is a continuation of the Interval arithmetics in groups: Pass 1 […]

  2. IsarMathLin version 1.6.8 released « Formalized Mathematics Says:

    […] The new CommutativeSemigroup_ZF theory is another take on the subject of summing up elements of some finite subset of a semigroup. This is similar to what was done in the Semigroup theory, but this time the approach is more specific to the case when the semigroup operation is commutative and does not require a linear order on the elements that we are summing up. This formalizes the definition of where is an indexed  family of elements of the semigroup and  is some finite subset of the index set. I have  written a bit about it that previously. […]

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: