How to justify the definition of summation $s_n=\sum_{i=1}^n a_i=a_1+\cdots+a_n$?

Question

I read https://www.wikiwand.com/en/Summation#/Formal_definition and found that they define summation via recursion, so I decided to formalize the proof that that this definition is actually valid. I've two questions:

1. Does my proof contain any error?

2. Are there other simple ways to define summation?

Thank you so much!

Suppose that $(a_1,\cdots,a_n)$ is a finite sequence in $\mathbb N$. Show that there is a sequence $(s_1,\cdots,s_n)$ such that $s_1=a_1$ and $s_{i+1}=s_i+a_{i+1}$ for all $1\leq i<n$.

My attempt:

We define mapping $f$ as follows: $f: \mathbb N\times\mathbb N\to\mathbb N\times\mathbb N: (i,a)\mapsto\begin{cases} (i+1,a+a_{i+1})&\text{if }i<n\\ (i+1,a)&\text{if }i\geq n \end{cases}$

By recursion theorem, there is a unique sequence $(p_i\mid i\in\mathbb N)$ such that $p_0=(1,a_1)$ and $p_{i+1}=f(p_i)$. Let $\pi:\mathbb N\times\mathbb N\to\mathbb N$ be the projection to the second co-ordinate i.e. $\pi(i,a)=a$. Let $s_i=\pi(p_i)$ for all $1\leq i\leq n$, then $(s_i\mid 1\leq i\leq n)$ is the required sequence. It's clear from the definition of $s_i$ that $s_{i+1}=s_i+a_{i+1}$ for all $1\leq i<n$.

Answer 1

There are still a few issues with this proof. Most notably, you're being a bit sloppy with the definitions of all of your 'entities' around the proof; for instance, you say that "$s_{i+1}=f(s_i)$," but $f$ is defined on $\mathbb{N}\times\mathbb{N}$, and it's unclear whether individual elements $s_i$ are members of $\mathbb{N}$ or $\mathbb{N\times N}$; at one point you say $s_0=\langle 1,a_1\rangle$ which suggests that each $s_i$ is a member of $\mathbb{N}\times\mathbb{N}$, but then later you say $s_{i+1}=s_i+a_{i+1}$, which suggests that the $s_i$ are members of $\mathbb{N}$.

Instead, I suggest writing it in this form:

For each function $a():\mathbb{N}\mapsto\mathbb{N}$, there is a function $s():\mathbb{N}\mapsto\mathbb{N}$ such that for all $n\in\mathbb{N}$, $s(n)=\sum_{i=1}^na(i)$.

Now it's clear exactly what the domain of the quantities being worked with is, and you can be more precise in your usage of the recursion theorem: in particular, we can rewrite the statement above as follows:

For each function $a():\mathbb{N}\mapsto\mathbb{N}$, there is a function $s():\mathbb{N}\mapsto\mathbb{N}$ such that $s(1)=a(1)$ and such that for all $n\in\mathbb{N}$, $s(n+1)=s(n)+a(n+1)$.

And now it should be clear that we can take the function $f(i,m): \mathbb{N}\times\mathbb{N}\mapsto\mathbb{N}$ given by $f(i,m)=m+a(i)$ and apply the recursion theorem to $f()$. (Note that there's no need for cases in the definition of $f()$; the 'base case' is essentially passed directly into the recursion theorem.)