How to recursively define a sum of any finite sequence I'm stuck at exercise 4.9 of chapter 3 in "Introduction to set theory" of Karel Hrbacek and Thomas Jech (Third revised edition)
The exercise is as follows:
For each finite sequence $\langle k_i: 0 \leq i < n \rangle$ of natural numbers define $\sum \langle k_i: 0 \leq i < n \rangle$ so that:

*

*$\sum\langle \rangle=0$

*$\sum\langle k_0 \rangle=k_0$

*$\sum\langle k_i: 0 \leq i <n \rangle = \sum\langle k_i: 0 \leq i <n-1 \rangle +k_n$ for $n \geq 1$
I know the idea is to recursively define a function such that for every finite sequence is image is the sum of the terms in the sequence, so I was trying to find in some way using the Recursion Theorem a unique function $\sum: Seq(\mathbb{N}) \longrightarrow \mathbb{N}$ that satisfies points 1 to 3, but I was not able to do it ($Seq(\mathbb{N})$ is the set of all finite sequences).
Any help would be apreciate, thanks.
 A: Here is one way to do it. First two lemmas:
Lemma 1. Let $\langle a_n\rangle$ be an infinite sequence of natural numbers. There exists a unique infinite sequence of natural numbers $\langle b_n\rangle$ satisfying
(1) $b_0=a_0$
(2) $b_n=b_{n-1}+a_n$ for all $n> 0$.
We call $\langle b_n \rangle$ the cumulative sum of $\langle a_n\rangle$.
Proof. Apply the the recursion theorem from chapter 3 of Hrbacek and Jech with the function $g:\mathbb N \times \mathbb N \to \mathbb N$ defined by $g(m,n)=m+a_n$.
Lemma 2.  Let $\langle a_n\rangle$,$\langle a'_n\rangle$ be two infinite sequence of natural numbers, and let $\langle b_n\rangle$,$\langle b'_n\rangle$ denote respectively their cumulative sums. Suppose $a_n=a'_n$ for all $0\leq n \leq k$ for some fixed $k\in \mathbb N$. Then  $b_n=b'_n$ for all $0\leq n \leq k$.
Proof. By induction on $n$. For $n=0$ we have $b_0=a_0=a'_0=b'_0$ by condition (1). Suppose $b_{n-1}=b'_{n-1}$ for some $0< n\leq k$. Then $$b_n=b_{n-1}+a_n=b'_{n-1}+a_n=b'_n$$ by condition (2). By induction it follows that $b_n=b'_n$ for all $0\leq n \leq k$.
We can now prove the claim. Given an $n$-tuple $\langle a_0,\dots,a_n\rangle$ of natural numbers  we define $\sum\langle a_0,\dots,a_n\rangle$ to be $b_n$, where $b_n$ denotes the $n$th term in the cumulative sum of the sequence $a_0,\dots,a_n,0,0,\dots$. By condition (1) we have that $\sum \langle a_0\rangle=a_0$ for any natural number $a_0$. By condition (2) and Lemma 2 we have that $\sum \langle a_0,\dots,a_n\rangle=\sum \langle a_0,\dots,a_{n-1}\rangle +a_n$ for all $n$-tuples of natural numbers $\langle a_0,\dots,a_n\rangle$ with $n>0$. Finally we define the sum of the empty sequence as $\sum  \langle \rangle=0$. Note that $\sum \langle a_0, a_1\rangle=a_0+a_1$, so we have effectively extended the addition operation on $\mathbb N$.
The function $\sum: Seq(\mathbb{N}) \longrightarrow \mathbb{N}$ just defined satisfies all three points in the post. It is the unique function from $Seq(\mathbb{N})$ to $\mathbb{N}$ satisfying these three points. For suppose $\sum': Seq(\mathbb{N}) \longrightarrow \mathbb{N}$ is another such function with $\sum\neq \sum'$. Let $n_0$ denote the smallest $n\in\mathbb N$ for which there exists an $n$-tuple  $\langle a_0,\dots,a_{n}\rangle$ with $\sum  \langle a_0,\dots,a_n\rangle \neq  \sum'  \langle a_0,\dots,a_{n}\rangle$, and let $\langle a_0,\dots,a_{n_0}\rangle$ be any such $n_0$-tuple.  Clearly $n_0>0$. Then we obtain
$\sum  \langle a_0,\dots,a_{n_0}\rangle =\sum  \langle a_0,\dots,a_{n_0-1}\rangle+a_{n_0}=\sum'  \langle a_0,\dots,a_{n_0-1}\rangle+a_{n_0}=\sum  \langle a_0,\dots,a_{n_0}\rangle$
a contradiction.
A: Alphie answer is very elegant and a really natural way to get the desired function, but I will post another slightly different way of solving it (it is in fact very similar to Alphie's answer).
Let's take as in Theorem 3.6 of the book (parametric version of the Recursion theorem) the sets $P=\text{Seq}(\mathbb{N})$, $A=\mathbb{N}$, $a: P \longrightarrow A$ given by $a(p)=0$ and $g: P \times A \times \mathbb{N} \longrightarrow A$ given by $g(p,m,n)=m+p(n)$ if $n < \text{len}(p)$ and $g(p,m,n)=0$ in any other case.
Then, this theorem gives us a unique function $f:P \times \mathbb{N} \longrightarrow A$ satisfying
(a) $f(p,0)=0$ for all $p \in P$
(b) $f(p,n+1) = g(p,f(p,n),n) = f(p,n) + p(n)$ if $n < \text{len}(p)$.
Now, if we define $\sum:\text{Seq}(\mathbb{N}) \longrightarrow \mathbb{N}$ as $\sum(p)= f(p,\text{len}(p))$ we can prove that it is the desired function.

*

*$\sum\langle \rangle = f(\langle \rangle,0)=0$


*$\sum\langle k_0 \rangle = f(\langle k_0 \rangle, 1) = f(\langle k_0 \rangle, 0+1) = f(\langle k_0 \rangle, 0) + k_0 = k_0$
For proving 3, we need the following lemma which can be easily proven by induction.
Lemma: Given $p, q \in \text{Seq}(\mathbb{N})$, if $n \leq \text{len}(q) < \text{len}(p)$ and $p(k)=q(k)$ for every $k<n$, then $f(p,n)=f(q,n)$.


*Using the lemma in the fourth equality we get
$$\sum\langle k_0, \cdots, k_{n+1} \rangle = f\left(\langle k_0, \cdots, k_{n+1} \rangle, n+2 \right)=f\left(\langle k_0, \cdots, k_{n+1} \rangle, (n+1)+1 \right)=f\left(\langle k_0, \cdots, k_{n+1} \rangle, n+1 \right)+k_{n+1}=f\left(\langle k_0, \cdots, k_{n} \rangle, n+1 \right)+k_{n+1}=\sum \langle k_0, \cdots, k_{n} \rangle + k_{n+1}$$
Proving that it is unique can be done in the same way as in Alphie's answer.
