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.
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.