Showing permutation does not change output of commutative operation (recursion theorem)

Question

(In what follows, NB that $\mathbb{N}^\times$ is the positive natural numbers, and $\mathbb{N}$ includes 0.)

I am working on Exercise 1 of Amann and Escher Analysis I, and the problem is essentially asking:

Show that if $X$ is a set with a commutative and associative (addition) operation defined thereon, then $\sum_{j=0}^n x_j = \sum_{j=0}^n x_{\sigma(j)}$ where $\sigma$ is any permutation (bijection) of $\{0,1,...,n\}$.

I am really baffled as to how to even start. It's obviously true, but I need to prove it using the recursion theorem of set theory (Amann and Escher's Proposition 5.11). I understand how the standard sum notation ought to interpreted. I've written:

We must first interpret the notation $\sum_{j=0}^n x_{\sigma(j)}$. Given the definition for general associative operations in Example 5.12, one is led to presume that this notation refers to a recursive definition which is induced by the original. The original $\sum_{j=0}^n x_j$ is technically defined by Prop 5.11 in terms of some sequence $x_0,x_1,x_2,...$ in $X$ and some sequence of functions $V_n: X^n \to X, (y_0,...,y_{n-1}) \mapsto y_{n-1} + x_n$ for $n \in \mathbb{N}^\times$. Now take the unique function $f: \mathbb{N} \to X$ (by Prop 5.11) for which $f(0) = x_0$ and for all $n \in \mathbb{N}$, $f(n+1) = V_{n+1}(f(0),...,f(n)) = f(n) + x_{n+1}$. Then define $\sum_{j=0}^n x_j := f(n)$.

I am guessing that I need to interpret the notation $\sum_{j=0}^n x_{\sigma(j)}$ somehow in terms of a recursive definition related to the sequence $V_n$ which defined $\sum_{j=0}^n x_j$ (and then perhaps I need to use induction somehow?), but I can't see how given that $\sigma$ is defined for fixed $n$, among other things. Can anyone provide a hint or even a sketch of a proof, with careful attention paid to what $\sum_{j=0}^n x_{\sigma(j)}$ really means?

For those interested in all the gory details of what I have, I have attached a couple pictures of relevance, but hopefully my question is valid as it stands.

Answer 1

First of all, I don't believe you have sufficient foundation in basic logic to tackle such problems. This is not your fault, naturally, because it is hard to find good teachers. For you to truly grasp how everything in mathematics is built, you would need to learn basic FOL (first-order logic) including an actually usable deductive system such as this one.

As part of that, you need to understand precisely the logical underpinnings of definitions, which are captured by definitorial expansion. An important example is the pair-projection function-symbols first and second where first(p) and second(p) are the first and second items in p for any ordered pair p. (These can be defined rigorously in this way.) We can then use the notation ( S x , T y ↦ E(x,y) ) as short for ( (S×T) i ↦ E(first(i),second(i)) ) and similarly use the notation ( S x , T y , U z ↦ E(x,y,z) ) as short for ( (S×(T×U)) i ↦ E(first(i),first(second(i)),second(second(i))) ).

The proposition 5.11 that you cited from your book is actually a very shoddy one from a logical viewpoint. It has the nebulous ellipsis ("..."), which in general is imprecise and results in shoddy conceptual understanding. The real general recursion theorem is:

  ∀A,S∈set ∀c∈A→S ∀f∈A×(ℕ×S)→S ∃g∈A×ℕ→S ∀x∈A
  ( g(x,0) = c(x) ∧ ∀k∈ℕ ( g(x,k+1) = f(x,(k,g(x,k))) ) ).

This allows you to construct the summation fully rigorously like this (skipping minor steps):

Let SumZ = ( (ℕ⁺→ℂ) f ↦ ( ℕ k ↦ 0 ) ).
Let SumA = ( (ℕ⁺→ℂ) f , ℕ k , (ℕ→ℂ) g ↦ ( ℕ i ↦ i ≤ k ? g(i) : g(k)+f(k+1) ) ).
[Now we apply the general recursion theorem on SumZ and SumA.]
Let SumP∈(ℕ⁺→ℂ)×ℕ→(ℕ→ℂ) such that
  ∀f∈ℕ⁺→ℂ ( SumP(f,0) = SumZ(f) ∧ ∀k∈ℕ ( SumP(f,k+1) = SumA(f,(k,SumP(f,k)) ) ).
Let Sum = ( (ℕ⁺→ℂ) f , ℕ k ↦ SumP(f,k)(k) ).
Given f∈ℕ⁺→ℂ:
  Sum(f,0) = SumP(f,0)(0) = SumZ(f)(0) = ( ℕ k ↦ 0 )(0) = 0.
  Given k∈ℕ:
    Sum(f,k+1) = SumP(f,k+1)(k+1) = SumA(f,(k,SumP(f,k)))(k+1)
     = SumP(f,k)(k)+f(k+1) = Sum(f,k)+f(k+1).
  ∀k∈ℕ ( Sum(f,k+1) = Sum(f,k)+f(k+1) ).
∀f∈ℕ⁺→ℂ ( Sum(f,0) = 0 ∧ ∀k∈ℕ ( Sum(f,k+1) = Sum(f,k)+f(k+1) ) ).
[We have now obtained the Sum operator with its desired properties.]

I want to emphasize that nowhere in this 100% rigorous construction do we rely on assuming associativity or commutativity of + on ℂ! Only when we want to prove some further properties of Sum would we need those.

~ ~ ~

Now on to your question. As a beginner you should probably not use subscripts if you are dealing with a genuine function. You can see already that the Sum operator as defined above requires two inputs, one being a function from ℕ⁺→ℂ and the other being a natural number that represents the index to sum to. Don't think of it as $\sum_{i=1}^k f_i$. Think of it as $\sum_{i=1}^k f(i)$, which is what it truly is.

Then everything regarding permutations would become crystal-clear too. You want to prove that $\sum_{i=1}^k f(i) = \sum_{i=1}^k f(σ(i))$ for every $f{∈}ℕ⁺{→}ℂ$ and permutation σ on $[1..k]$. Of course, $\sum_{i=1}^k f(σ(i)) = \sum_{i=1}^k (f∘σ)(i)$, and so you ought to know precisely what that means. If conventional notation is confusing, simply use the precise formal notation and it is clear.

In particular, you must supply Sum with a function from ℕ⁺→ℂ and the index to sum to. Given f∈ℕ⁺→ℂ, remember that f(i) is not a function, but f is, and so is f∘σ. For convenience, let's not ask for the summation operator to be able to handle functions whose domain is not ℕ⁺, otherwise the above definition of Sum is insufficient. (Your cited text makes this mistake as well.) So eliminate this problem, we can define a permutation of $[1..k]$ as a function $f{∈}ℕ⁺{→}ℕ⁺$ such that $Im(f{↾}[1..k]) = [1..k]$.

Rigorously:

Let Perm = ( ℕ k ↦ { f : f∈ℕ⁺→ℕ⁺ ∧ ∀x∈[1..k] ∃i∈[1..k] ( f(i) = x ) } ).
Given f∈ℕ⁺→ℂ and k∈ℕ and σ∈Perm(k):
  σ∈ℕ⁺→ℕ⁺.
  f∘σ∈ℕ⁺→ℂ.
  If k = 0:
    Sum(f∘σ,k) = 0.
  If k > 0:
    k−1∈ℕ.
    Sum(f∘σ,k) = Sum(f∘σ,k−1)+(f∘σ)(k).

Now the desired theorem is:

  ∀f∈ℕ⁺→ℂ ∀k∈ℕ ∀σ∈Perm(k) ( Sum(f,k) = Sum(f∘σ,k) ).

How do we prove it? Ignoring all the other technical problems with the cited text, scleaver gives an intuitive method, but there is still a big problem: It is actually not at all easy to prove the theorem for a single arbitrary transposition. I will hence demonstrate an alternative approach:

For any permutation $σ$ on $[1..k]$ define $c(σ)$ to be the number of pairs $⟨i,j⟩$ from $[1..k]^2$ such that $i < j$ and $σ(i) > σ(j)$. It is easy to prove that:

1. If $c(σ) = 0$ then $σ(i) = i$ for every $i∈[1..k]$.
2. If $c(σ) > 0$ then there is some $d∈[1..k{−}1]$ such that $σ(d) > σ(d+1)$.

By strong induction along $ℕ$ we can assume that the theorem holds for any permutation $φ$ with $c(φ) < c(σ)$. If $c(σ) = 0$ then we are done. Otherwise by the above let $d∈[1..k{−}1]$ such that $σ(d) > σ(d+1)$. Let $σ'$ be the same as $σ$ except that $σ'(d) = σ(d+1)$ and $σ'(d+1) = σ(d)$. Then we can show that $c(σ') < c(σ)$, and so $\sum_{i=1}^k f(i) = \sum_{i=1}^k (f∘σ')(i)$. We also have:
  $\sum_{i=1}^k (f∘σ)(i)$
  $ = \Big( \big( \sum_{i=1}^{d-1} (f∘σ)(i) + (f∘σ)(d) \big) + (f∘σ)(d+1) \Big) + \sum_{i=d+2}^{k} (f∘σ)(i)$ [by (✻)]
  $ = \Big( \big( \sum_{i=1}^{d-1} (f∘σ')(i) + (f∘σ')(d+1) \big) + (f∘σ')(d) \Big) + \sum_{i=d+2}^{k} (f∘σ')(i)$
  $ = \Big( \big( \sum_{i=1}^{d-1} (f∘σ')(i) + (f∘σ')(d) \big) + (f∘σ')(d+1) \Big) + \sum_{i=d+2}^{k} (f∘σ')(i)$
    [by associativity and commutativity of + on ℂ]
  $ = \sum_{i=1}^k (f∘σ')(i)$ [by (✻)]
  $ = \sum_{i=1}^k f(i)$.

(✻) is one key property of summation that must be proven before you can do this kind of manipulation. It relies on associativity, but not commutativity, of + on ℂ. Also note that the "$\sum_{i=d+2}^{k}$" summation notation with a variable lower index can be defined in terms of the more basic summation notation with a fixed lower index of $1$. If you want to make it fully rigorous, you can either define it in terms of Sum, or in the first place define Sum to take an extra input for the lower index. Both are viable choices.

I have chosen not to formalize the entire theorem in full so that you can see enough to convince yourself of how it can be done, and if you are keen enough to try it you can ask me if you get stuck.

Answer 2

Here's a sketch of what I had in mind in my comment, or something like it. I may be overcomplicating this but I'm trying to be explicit to avoid confusion over notation.

Let $x: \Bbb N \to X$ be a sequence and for all $n \in \Bbb N$ and all permutations $\sigma$ of length $n + 1$ define $$\sum_{j=0}^nx_j := f(n)$$ $$\sum_{j=0}^nx_{\sigma(j)} := f_\sigma(n)$$ where $f$ is the sequences of partial sums defined as in the book which satisfy $$f(0) = x_0$$ $$f(n) = f(n - 1) + x_n$$ and $f_\sigma$ is defined analogously so that it satisfies $$f_\sigma(0) = x_{\sigma(0)}$$ $$f_\sigma(n) = f_\sigma(n - 1) + x_{\sigma(n)}$$ The claim is$$\forall n \in \Bbb N : \forall \sigma: \{0, 1, ...n \} \leftrightarrow \{0, 1, ...n \}:f(n) = f_\sigma(n)$$

The base case is trivial since if $n = 0$ then $\sigma: \{0\} \leftrightarrow \{0\}$ is the identity so $f(0) = f_\sigma(0) = x_0$. Now assume $n > 0$ and $$\forall k < n: \forall \sigma: \{1, 2, ...k\} \leftrightarrow \{1, 2, ...k\}:f(k) = f_\sigma(k)$$

If $\sigma(n) = n$ then $f_\sigma(n - 1)$ corresponds to a permuted sum of length $n - 1$ so we can use the induction hypothesis to show $$f_\sigma(n) = f_\sigma(n - 1) + x_n = f(n - 1) + x_n = f(n)$$

If $\sigma(n) \ne n$, the idea is to swap the position of the $x_n$ term that's somewhere in the partial sum $f_\sigma(n - 1)$ with $x_{\sigma(n)}$, resulting in $f_\sigma(n) = f_{\sigma'}(n) = f(n)$ for some $\sigma'$ such that $\sigma'(n) = n$. So it suffices to show that the result is true for transpositions, ie, permutations that just swap two elements, because $\sigma' = \tau \circ \sigma$ for some transposition $\tau$, so we can let the initial sequence be $x_{\sigma(n)}$ and get $f_\sigma(n) = f_{\tau\sigma}(n) = f_{\sigma'}(n)$.

I'll leave the rest out for now, including the actual use of commutativity, but that's the idea. If you can prove that permuted sums are equal when the permutation is a transposition then the rest should follow.