# About the definition of summation

Let $\odot:A\times A\to A,\ (a,b)\mapsto a\odot b$ be a binary operation on nonempty set $A,$ and denote $\left\{1,2,\cdots,k\right\}$ as $S_k,$ here $k\in \mathbb N,$ and the set of all mappings $f:S_k\to A$ is denoted as $T_k,$ the it seems that we can define a series of functions (recursively) $${\Sigma}_{k+1}:T_{k+1}\to A,\ f\mapsto \big[{\Sigma}_k(f|_{S_k})\odot f(k+1)\big];$$ $${\Sigma}_1:T_1\to A,\ f\mapsto f(1).$$ I call these functions ${\Sigma}_k(k\in \mathbb N)$ as summation functions.

So the only thing left is to prove our recursive definition of ${\Sigma}_k$ is reasonable and well-defined. But unluckily I'm not familiar with mathematical logic...

Question: Prove that the definition of ${\Sigma}_k$ is well-defined. Any hint would be appreciated.

• $\displaystyle \sum_{i=1}^k a_i$ can be recursively and rigorously defined. – Kenny Lau Jan 7 '18 at 5:51
• What is lax about the usual definition $$\sum_{k=1}^0a_k=0,\ \sum_{k=1}^{n+1}a_k=\left(\sum_{k=1}^na_k\right)+a_{n+1}\ ?$$ What more is required for a strict definition? – bof Jan 7 '18 at 6:00
• Well, this is a recursive definition, and I believe we have to prove this recursive definition is well-defined... – painday Jan 7 '18 at 6:04
• Maybe now the symbol would be better... – painday Jan 7 '18 at 6:08
• The cleanest way to deal with this, in my opinion, is to view (finite) summation as a function from lists of numbers to numbers (or generally, given a monoid). The key phrase here is "structural induction" which can be reduced to (structural) induction over the naturals in set theory if you want, or can be understood categorically via initial algebras. $\sum\langle\rangle = 0$, $\sum(a\bar a)=a+\sum\bar a$ is then well-defined via structural induction (specifically it can be defined as a fold: $\mathsf{fold}(0,(x,y)\mapsto x+y,\bar a)$). – Derek Elkins left SE Jan 7 '18 at 6:38

Yes, recursive definitions can be reduced to explicit definition. Fix $a_i$ for $i=1,2,3,\ldots$. Let $M$ be a non negative integer. Show by induction on $M$ that for any $M$, and any ? there exists a unique sequence $S_M(1,k)$ (sum from 1 to $k$ of the $a_i$) $k=1,2,3,\ldots,M$) satisfying your recursive conditions for all $k=1,\ldots,M$. These finite sequences fit together to form one infinite sequence $S(1,k)$, $k=1,2,3,4,\ldots$ (sum from 1 to k of the $a_i$s). This reduction avoids having to add an infinite number of axioms, or rules of inference to set theory . It also means you can in practice use recursive definitions freely.

• Woah, you aren't able to use arbitrary recursive definitions freely. You need some argument that the recursive definition gives a unique and total function. That's built-in to structural recursion and fixed point recursion, but those only allow stylized patterns of recursion (with additional constraints in the latter case). – Derek Elkins left SE Jan 7 '18 at 8:12
• To use the general recursion theorem I know ,you may need the Axiom of choice as one of the axioms of set theory . Other than that ,I would like to see and example of a recursive defined sequence that which doesn't define a unique sequence . – StuartMN Jan 7 '18 at 21:45