If I define summation recursively, how do I prove formally that both of the following definitions are equivalent? First definition:
$\sum_{x=a}^{b} f(x)=f(b)+\sum_{x=a}^{b-1} f(x)$ if $a\leq b$, and equals $0$ otherwise
Second definition:
$\sum_{x=a}^{b} f(x)=f(a)+\sum_{x=a+1}^{b} f(x)$ if $a\leq b$, and equals $0$ otherwise
Intuitively, I have no doubt that both statements are always equal, but I am struggling to come up with a formal proof for it. I tried induction over $b$, but only got so far on working with the second definition:
$\sum_{x=a}^{b+1} f(x)=f(b+1)+\sum_{x=a}^{b}$
 A: Let's prove it formally, by strong induction on $b - a$. If $b - a < 0$, then both definitions produce $0$, so we consider only the case where $b - a \ge 0$, allowing us to use strong induction.
Let's be clear about the predicate we're proving. Let $R(f,a,b)$ and $L(f, a, b)$ be the result of applying the two respective definitions to $\sum_{x=a}^b f(x)$ (in case it's not entirely obvious, $R$ is for "right" and $L$ is for "left", to represent from where we're stripping off terms). We are claiming that:
$$P(n) : (\forall a)(\forall b)(\forall f)\Big(a - b = n \implies R(f, a, b) = L(f, a, b)\Big).$$
The base cases I wish to start from are $P(0)$ and $P(1)$. First, we tackle $P(0)$. Assuming $a - b = 0$,
$$R(f, a, b) = R(f, a, a) = R(f, a, a - 1) + f(a) = 0 + f(a),$$
and
$$L(f, a, a) = f(a) + L(f, a + 1, a) = f(a) + 0.$$
Next, if $a - b = 1$, then
$$R(f, a, b) = R(f, a, a + 1) = R(a, a) + f(a + 1) = f(a) + f(a + 1) + 0,$$
and similarly for $L(f, a)$.
Now, let's fix $n \ge 2$, and suppose that $P(k)$ is true for $k < n$. To prove $P(k)$, let us suppose $a$ and $b$ such that $b - a = n$, and $f$ is some function. Now,
$$L(f, a, b) = f(a) + L(a + 1, b).$$
Because $b - (a + 1) = n - 1 < n$, we therefore know that $L(a + 1, b) = R(a + 1, b)$, so
$$L(f, a, b) = f(a) + R(a + 1, b) = f(a) + R(a + 1, b - 1) + f(b).$$
A similar argument shows
$$R(f, a, b) = f(a) + L(a + 1, b - 1) + f(b),$$
which is equal to the quantity above, since $b - 1 - (a + 1) = n - 2 < n$ (note: we needed the assumption that $n \ge 2$ to ensure that two terms can be pulled out this way, hence the need for double base case). Thus, the induction step is completed, and the result is proven by strong induction.
A: We do induction by the number $a-b+1$ of summands.
We start with the definition of the sum:
$$\sum_{x=a}^{b} f(x):=\sum_{x=a}^{b-1} f(x)+f(b)$$
and we want to prove
$$\sum_{x=a}^{b} f(x)=f(a)+\sum_{x=a+1}^{b} f(x)$$
For $b-a+1=1$ and $b-a+1=2$ the statement can be easily verified, so let us assume $b-a+1\gt3$. Then we have:
$$\begin{align}
\sum_{x=a}^{b} f(x)  
\\ \text{by definition of the sum we have} &
\\=f(b)+\sum_{x=a}^{b-1} f(x)  \tag 1
\\\text{so by the induction hypothesis we have}  
\\=f(b)+\left(f(a)+\sum_{x=a+1}^{b-1} f(x)\right) \tag 2
\\=f(a)+\left(f(b)+\sum_{x=a+1}^{b-1} f(x)\right) \tag 3
\\\text{and again by definition of the sum}
\\=f(a)+\sum_{x=a+1}^{b} f(x) \tag 4
\end{align}$$
We have chosen $b-a+1\ge3$ in the proof to guarantee that $\sum_{x=a+1}^{b-1} f(x)$ has at least one summand.
A: First, we assume $a,b$ are integers (and so must be finite). If $a > b$, both sums yield $0$ (and thus agree), so assume $a \le b$.

A, intuitive direct approach is to apply the recursion. You have with the first definition:
$$
\begin{split}
\sum_{x=a}^b f(x)
 &= f(a) + \sum_{x=a+1}^b f(x) \\
 &= f(a) + f(a+1) + \sum_{x=a+2}^b f(x) \\
 &= f(a) + f(a+1) + \ldots + f(b-1) + \sum_{x=b}^b f(x) \\
 &= f(a) + f(a+1) + \ldots + f(b-1) + f(b) + \sum_{x=b+1}^b f(x) \\
 &= f(a) + f(a+1) + \ldots + f(b-1) + f(b) + 0 \\
 &= f(a) + f(a+1) + \ldots + f(b-1) + f(b)
\end{split}
$$
The second definition yields
$$
\begin{split}
\sum_{x=a}^b f(x)
 &= f(b) + \sum_{x=a}^{b-1} f(x) \\
 &= f(b-1) + f(b) + \sum_{x=a}^{b-2} f(x) \\
 &= f(a+1) + \ldots + f(b-1) + f(b) + \sum_{x=a}^a f(x) \\
 &= f(a) + f(a+1) + \ldots + f(b-1) + f(b) + \sum_{x=a-1}^a f(x) \\
 &= f(a) + f(a+1) + \ldots + f(b-1) + f(b) + 0 \\
 &= f(a) + f(a+1) + \ldots + f(b-1) + f(b)
\end{split}
$$
so the sums agree.

A more formal approach is to use induction on the number of terms.
