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: formalized mathematics, Lesgue integral

This entry was posted on December 6, 2008 at 10:57 pm and is filed under mathematics. 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.

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

Interval arithmetic in groups - pass 2 « Formalized Mathematics Says:
March 1, 2009 at 9:49 pm | Reply
[…] arithmetic in groups – pass 2 By slawekk This is a continuation of the Interval arithmetics in groups: Pass 1 […]
IsarMathLin version 1.6.8 released « Formalized Mathematics Says:
April 26, 2009 at 12:18 am | Reply
[…] 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. […]

Formalized Mathematics

Interval arithmetic in groups: Pass 1

Share this:

Like this:

Related

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

Leave a Reply Cancel reply