Any commutative associative operation can be extended to a function on nonempty finite sets This is a fact we use very frequently in general mathematics when we write such notations as $1+2+3+4$: since we know that $+$ is commutative and associative, we can just "drop the parentheses" and not worry about order of operations. Of course I believe this, but how does one prove this in full generality? Even stating it is giving me trouble. Here's my attempt:

Assume an operation $\oplus:S\times S\to S$ is provided satisfying $x\oplus y=y\oplus x$ and $x\oplus(y\oplus z)=(x\oplus y)\oplus z$ for all $x,y,z\in S$.
Claim: Given any finite set $\emptyset\subset A\subseteq S$, there exists a unique $z\in S$ such that for any function $f:{\cal P}(A)\to{\cal P}(A)$ which satisfies $\emptyset \subset f(B)\subset B$ for all $B\subseteq A$ with $|B|\ge 2$ and any function $g:{\cal P}(A)\to S$ which satisfies $g(\{x\})=x$ for all $x\in S$ and $g(B)=g(f(B))\oplus g(B-f(B))$ for all $|B|\ge 2$, $g(A)=z$.

The operation $\oplus$ does not necessarily have an identity element, so we do not attempt to define an empty sum. Intuitively, this element $z$ represents the finite sum of the elements in $A$, so if $A=\{1,2,3\}$ and $f(\{1,2,3\})=\{1\}$ and $f(\{2,3\})=\{3\}$, then
$$z=g(\{1,2,3\})=g(\{1\})\oplus g(\{2,3\})=g(\{1\})\oplus (g(\{3\})\oplus g(\{2\}))=1\oplus(3\oplus 2).$$
There has got to be a better way to say that, but this is the only way I can think of to capture all the possibilities of parenthesization, and still be amenable to a formal proof. And now that I've stated it, how should I prove it? I suppose I should induct on something, but I've no idea what.
Edit: The goal here is to be able to define an operation $F$ such that $F(\{x_1,\dots,x_n\})=x_1\oplus\cdots\oplus x_n$ and be assured that the operation is well defined and satisfies $F(A\cup B)=F(A)\oplus F(B)$, when $A$ and $B$ are disjoint finite nonempty subsets of $S$.
 A: You can state it as follows: Given is a set $S$ with a binary $\oplus$ operation on it which is associative and commutative. 
For every finite nonempty set $A\subseteq S$, there exists an element $S_A\in S$ such that: 1) If $A=\{a\}$, then $S_A=a$. 2) If $|A|=n$ then for any bijective function $f:\{1,2,3,4,\cdots ,n\}\to A$, it holds that $S_A = f(1)\otimes S_{\{f(2),f(3),\cdots, f(n)\}}$. 
Moreover, this assignment $A\mapsto S_A$ is the only one with these properties. 
The proof of both existence and uniqueness is done by a standrad proof by induction. 
A: This is the equivalence between commutative semigroups in the usual sense and their monadic description. It follows, for example, from Beck's monadicity theorem. Here is a down-to-earth formulation: If $S$ is a commutative semigroup, then we have a map which associates to every function $\lambda : S \to \mathbb{N}$ with the property that $\lambda(s)>0$ for at least one $s$, an element $\sum_{x \in S} \lambda(x) \cdot x$ of $S$ (abbreviated by $\sum \lambda$), with the following properties: 


*

*If $E=\{s\}$ for some $s \in S$ and $\lambda(s)=1$, then $$\sum_{x \in E} \lambda(x) \cdot x = s.$$

*If $\mu$ is a function which associated to every $\lambda$ as above a natural number (with the property that there is some $\lambda$ with $\mu(\lambda)>0$), then
$$\sum_{x \in S} \left(\sum_{\lambda} \mu(\lambda) \cdot \lambda(x)\right) \cdot x = \sum_{x \in S} \left(\sum_{\sum \lambda = s} \mu(\lambda) \right) \cdot x$$


The converse is also true. Whenever $S$ is a set equipped with a sum operation as above, then this endows $S$ with the structure of a commutative semigroup. The point is that the set of functions $\lambda$ equipped with the pointwise addition is the free commutative semigroup on the set $S$. See here for the corresponding monadic description of abelian groups.
A: So you want to prove that if $S$ is a set and $+$ is a binary commutative associative law : $S \times S \to S$, then there is a unique function $\sum$ from non empty finite subsets of $S$ to $S$ satisfying :
- if $x \in S, \sum \{x\} = x$
- if $A \cap B = \emptyset, \sum A \cup B = \sum A + \sum B$.
Prove this by induction of the size of the subset : if $|A| = 1$ then we have no choice.
If $|A| \ge 2$, suppose we can define $\sum A$ in several ways : $A = B_1 \cup B_2 = C_1 \cup C_2$, where the pairs are disjoint. Using the induction hypothesis, the sums of the subsets $B_i$ and $C_j$ are well-defined and we need to show that $\sum B_1 + \sum B_2 = \sum C_1 + \sum C_2$.
Let $D_{ij} = B_i \cap C_j$. Suppose for now that none of them is empty. Then $\sum B_1 = \sum D_{11} + \sum D_{12}$ and so on, and the claim boils down to proving $\forall a,b,c,d \in S, (a+b)+(c+d) = (a+c)+(b+d)$.
And this is easy : $(a+b)+(c+d) = a+(b+(c+d)) = a+((c+d)+b) = a+(c+(d+b)) = (a+c)+(d+b) = (a+c)+(b+d)$.
The cases where one or more of the $D_{ij}$ is empty are done in a similar way (and are even easier). Or you could add an element $\star$ to $S$ and extend $+$ by defining $\star + x = x + \star = x$, prove that $+$ still is commutative and associative, and finally define $\sum \emptyset = \star$
A: It turns out that the claim as originally stated cannot be proven by induction directly, since later steps may introduce repeated elements, which are not accounted for in the claim. Instead, we shall prove it for sequences and weaken it at the end.
Claim: Let $[n]=\{0,1,\dots,n-1\}$. Given any finite sequence $A=\langle x_0,x_2,\dots,x_{n-1}\rangle$ with $n\ge1$ and each $x_i\in S$, there exists a unique $z\in S$ (denoted $F(A)$) such that for any function $f:{\cal P}[n]\to{\cal P}[n]$ which satisfies $\emptyset \subset f(B)\subset B$ for all $B\subseteq [n]$ with $|B|\ge 2$ and any function $g:{\cal P}[n]\to S$ which satisfies $g(\{i\})=x_i$ for all $i\in [n]$ and $g(B)=g(f(B))\oplus g(B-f(B))$ for all $|B|\ge 2$, $g[n]=z=F(A)$.
Let's try to prove this by induction on $n$. In the base case, $A=\langle x_0\rangle$ for some $x_0\in S$. Then $g(\{0\})=g(\{x\})=x_0$ is unique, so we are done.
In the induction step, we assume that for all $|B|\le n$, there is a unique $F(B)$ as stated in the claim and we consider $|A|=n+1$. Then we claim that there exists some two-element set that is evaluated by $g$. (This step takes some justification; we were not precise about the "relevant" part of the domain of $g$, so this should say: $\exists k\in{\Bbb N}\ \exists h:[k]\to {\cal P}(n)$ such that $h(0)=[n+1]$ and $|h(k-1)|=2$ and $\forall m<k-1\,\big[h(m+1)=f(h(m))\vee h(m+1)=h(m)-f(h(m))\big]$. This is our way of specifying a "path" through the "binary tree" prescribed by $f$.) Suppose $h(k-1)=\{i,j\}$ is this two-element set. Then $g(\{i,j\})=x_i\oplus x_j$ or $g(\{i,j\})=x_j\oplus x_i$, and we know these are equal.
Now consider $B=\langle y_0,\dots,y_{n-1}\rangle=A-\langle x_i,x_j\rangle+\langle x_i\oplus x_j\rangle$, where we remove $x_i$ and $x_j$ from the sequence and append $x_i\oplus x_j$ to the end. There is an index mapping $\varphi$ which takes each element of $A$ to the corresponding element of $B$, that is, $y_{\varphi(m)}=x_m$, except that $y_{\varphi(i)}=y_{\varphi(j)}=x_i\oplus x_j$. If we define a function $f':{\cal P}[n]\to{\cal P}[n]$ by $f'(\varphi(X))=\varphi(f(X))$, it will satisfy the induction requirements (and a $g$ satisfying the requirements given $B$ and $f'$ always exists), so we can apply the induction hypothesis to $B$, to find that we can rearrange the sequence to
$$(\,((y_0\oplus y_1)\oplus y_2)\cdots\oplus y_{n-2})\oplus(x_i\oplus x_j)=((\,((y_0\oplus y_1)\oplus y_2)\cdots\oplus y_{n-2})\oplus x_i)\oplus x_j$$
by associativity. We're nearly done; we just need to put $x_{n+1}$ at the end instead of $x_j$. If $j=n+1$, great, otherwise, swap $x_{n+1}$ with $x_i$ in the left argument (which is of length $n$ and thus can be rearranged by hypothesis) and then swap $x_{n+1}$ with $x_j$ by regular associativity and commutativity. The left argument is now $\langle x_0,x_1,\dots,x_n\rangle$ in some order, so it adds to something unique by hypothesis; thus $F(A)=F(A-\langle x_{n+1}\rangle)\oplus x_{n+1}$ is independent of $f$ and $g$ and thus is unique.
There's my proof; as you can see I got tired of the $f$ and $g$ interpretation halfway through, but hopefully the attentive reader can fill in the details. Unfortunately, that's supposed to be me, so we'll see how the real proof goes.
