How to formally prove that index renaming doesn’t change sum

Question

How do we formally prove (e.g. in type theory) that $$\sum _ix_i=\sum_ix_{f(i)}$$ For any bijection $f:I\to I$ for any finite set $I$?

I might be overcomplicating things, but I’m having trouble seeing how to best define $\sum$ formally, and do the proof. My initial thought was to apply mathematical induction, given that we can define $\sum_i^nx_i=\sum_i^{n-1}x_i+x_n$, but I can’t see how it works for arbitrary bijections.

Answer 1

For an automated proof checker (or similar very formal system) you would probably prove a theorem/lemma that the sum of the elements in a finite set was well defined, by induction on the cardinality, invoking associative and commutative laws (which might be axioms or themselves theorems).

Related: Would it be possible / necessary to prove that a math law can be applied to a given formula. Is intuitive recognition of structure similarity enough?

Answer 2

To make it formally, you can use induction as you wanted, but first let's properly define $\sum$ for any set $I$.

Let $I$ be a well-ordered finite set, $(G, +)$ be an abelian group (for example $(\mathbb R, +)$), and let $x: I \rightarrow G$. If $I$ is non-empty, then it has a minimal element, and let $m\in I$ be this minimal element. We define $\sum_{i\in I}x(i)\in G$ inductively as $$ \sum_{i\in I}x(i) := \left\{\begin{array}{ll} 0& \text{for } I=\varnothing \\ x(m) + \sum_{i\in I\setminus\{m\}}x(i) & \text{for } I \neq\varnothing\end{array} \right.$$ where we use the fact that after removing the minimal element from a well-ordered set, the remaining set is still well-ordered.

We want to prove that

The value of $\sum_{i\in I}x(i)$ does not depend on the chosen ordering of the set $I$.

We'll prove it by Induction over $|I|$.

For $|I|=0$ and $|I|=1$ it's trivial, as such sets have only one ordering.

For $|I|\ge 2$, let's assume that we have two order structures on $I$. I'll denote them as $I$ and $I'$; they are equal as sets, but they have different ordering. Let $m$ be the minimal element in $I$ and $m'$ be the minimal element in $I'$. We have $$ \sum_{i\in I} x(i) = x(m) + \sum_{i\in I\setminus\{m\}}x(i)$$ $$ \sum_{i\in I'} x(i) = x(m') + \sum_{i\in I'\setminus\{m'\}}x(i)$$

1. If $m=m'$ then we have $x(m) =x(m')$ and $I\setminus\{m\}=I'\setminus\{m'\}$ (as sets), so from the inductive assumption we have $\sum_{i\in I\setminus\{m\}}x(i) = \sum_{i\in I'\setminus\{m'\}}x(i)$. That means that $\sum_{i\in I} x(i)=\sum_{i\in I'} x(i)$.
2. If $m\neq m'$, then $m\in I'\setminus\{m'\}$. By the inductive assumption, the ordering of $I'\setminus\{m'\}$ doesn't change the value of the sum, so we can choose such ordering that $m$ is the minimal element of $I'\setminus\{m'\}$. We have then (using associativity and commutativity of addition in $G$): $$ \sum_{i\in I'\setminus\{m'\}}x(i) = x(m) + \sum_{i\in I'\setminus\{m,m'\}}x(i)$$ \begin{align} \sum_{i\in I'} x(i) &= x(m') + \Big(x(m) + \sum_{i\in I'\setminus\{m,m'\}}x(i)\Big) = \\ &= \Big(x(m') + x(m)\Big) + \sum_{i\in I'\setminus\{m,m'\}}x(i) = \\ &= \Big(x(m) + x(m')\Big) + \sum_{i\in I'\setminus\{m,m'\}}x(i) = \\ &= x(m) + \Big(x(m') + \sum_{i\in I'\setminus\{m,m'\}}x(i)\Big) = \\ &= x(m) + \sum_{i\in I'\setminus\{m\}}x(i) = \\ &= x(m) + \sum_{i\in I\setminus\{m\}}x(i) = \sum_{i\in I}x(i)\end{align} $\Box$

Answer 3

I will present a formalization using homotopy type theory and a paper I found that constructs finite sets. This approach constructs finite sets as the free join semi-lattice of a type $A$; this construction is referred to as "Kuratowski Finite Sets." Let $\mathcal{K}(A)$ represent this type of finite sets on $A$, we will define it formally as the (higher) inductive type given by $$\begin{aligned}\mathcal{K}(A) : \mathcal{U} &:= \\ &|\;\emptyset : \mathcal{L}(A) \\ &|\; \{\cdot\} \,: A\to\mathcal{K}(A) \\ &|\; \cdot\cup\,\cdot : \mathcal{K}(A)\to \mathcal{K}(A)\to \mathcal{K}(A) \\ &|\; \textbf{nl} : \Pi(x : \mathcal{K}(A)), \emptyset\cup x=x \\ &|\; \textbf{nr} : \Pi(x : \mathcal{K}(A)), x\cup \emptyset = x \\ &|\; \textbf{idem} : \Pi(x:A), \{x\}\cup\{x\}=\{x\} \\ &|\; \textbf{assoc} : \Pi(x,y,z : \mathcal{K}(A)), x\cup(y\cup z)=(x\cup y)\cup z \\ &|\; \textbf{com} : \Pi(x,y: \mathcal{K}(A)), x\cup y = y\cup x \\ &|\; \textbf{trunc} : \text{isSet}(\mathcal{K}(A)) \end{aligned}$$ where the $\text{isSet}$ is given by $$\text{isSet}(\mathcal{K}(A)):\equiv \Pi(x,y: \mathcal{K}(A)),\Pi(p,q:x=y), p=q$$ (you can see more about $\text{isSet}$ in the HoTT book). We can then also form a membership function recursively and inductively as $$\begin{gather} \cdot \in\cdot : A\to \mathcal{K}(A)\to \text{Prop} \\ a\in\emptyset :\equiv \,\perp \\ a\in \{b\} :\equiv \| a=b\| \\ a\in (x_1\cup x_2) :\equiv \|(a\in x_1) + (a\in x_2)\| \end{gather}$$ Note that $g\in x_1$ implies $g \in x_1\cup x_2$ so we have a natural inclusion map $$\text{incl}_{x_1,x_2} : \{g : G \, |\, g\in x_1\}\to \{g : G \, |\, g\in x_1\cup x_2\}$$ and similarly $$\text{incl}'_{x_1,x_2} : \{g : G \, |\, g\in x_2\}\to \{g : G \, |\, g\in x_1\cup x_2\}.$$ Now we can formalize a repeated summation using an recursive definition that matches on the constructors.

You don't say what the $x_i$ are, but first notice that the indexed $x_i$ is the same as a function $x:I\to G$ (where $G$ is the type of whatever the $x_i$'s are). So lets suppose that $G$ is a type which has a commutative operation on it, called $+$, with an identity element $0_G$, i.e. $$\begin{gather} G : \mathcal{U} \\ \text{g_is_a_set} : \text{isSet}(G) \\ \cdot +\cdot \,: G\to G\to G \\ \text{plus_comm}\, :\, \large\Pi(x,y : G), x+y=y+x \\ 0_G : G \\ \text{add_identity} : \large\Pi(x : G), x+0_G=x \end{gather}$$ (note we want to assume that $G$ is a set so that the proposition-as-types representations of community and an additive inverse are mere propositions). Now we will define the summation over $I$ the image of a function $x : \{g : G\, |\, g\in I\}\to G$ for $I : \mathcal{K}(G)$. Let $$\text{sigma} : \Pi(I : \mathcal{K}(A)), (\{g : G\, |\, g\in I\} \to G)\to G$$ and define $\text{sigma}$ recursively by matching on the constructors of $I$. That is $$\begin{gather} \text{sigma}(\emptyset, x) :\equiv 0_G \\ \text{sigma}(\{g\}, x) :\equiv x(g) \\ \text{sigma}(x_1\cup x_2, x) :\equiv \text{sigma}(x_1, x\circ \text{incl}_{x_1,x_2}) + \text{sigma}(x_2, x\circ \text{incl}'_{x_1,x_2}) \end{gather}$$ Now we want to prove that if $f:\{g : G \, |\, g\in I\}\to \{g : G \, |\, g\in I\}$ is a bijection, then $$\Pi(x : \{g : G \, |\, g\in I\}\to G), \text{sigma}(I, x\circ f)=\text{sigma}(I, x)$$ This gives the entire set-up to attack the actual proof. As far as the actual proof, I'll leave that up to you. However, I would refer back to the paper I linked, and make use of the equivalence $$\mathcal{K}(G)\cong \mathcal{L}(G)$$ where $\mathcal{L}(G)$ constructs finite sets via lists of elements with a concatenation function. Then I would write a bijection on $f : (a::\ell)\to (a::\ell)$ as a bijection $g:\ell\to \ell'$ (with $\ell'\subset a::\ell$) composed with where $f$ sends $a$ after this bijection. Then, using the size function $\# : \mathcal{L}(A)\to\mathbb{N}$ defined in the paper induct on size, use the induction hypothesis on $g$, and then finish the inductive step by applying the commutivity of the addition to the composition with where $f$ sends $a$ which is just one swap of two elements.

Long story short, starting from scratch to prove a simple theorem like this is very annoying and difficult, as half the problem is defining the objects in the problem statement. Ideally all these definitional issues would be addressed first and form some sort of standard library. I feel comfortable stopping here, seeing as with a strong encoding of basic set theory and math into your type theory, this theorem is just as easy to prove as it is in informal mathematics. So rather than attempt the feat of defining as few things as possible to prove your specific theorem, this post shows you how you could start encoding the basic entities that would enable a more natural proof of such a theorem.