I can prove the following:
$$\exists a\forall b(b + a = b) \vdash \exists a(a + a = a)$$
as shown below:
$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$ $\fitch { 1. \qquad \exists a\forall b(b + a = b) \qquad (A) }{ \fitch { 2. \qquad \forall b(b + c = b) \qquad (A) }{ 3. \qquad c + c = c \qquad (\forall E: 2) \\ 4. \qquad \exists a(a + a = a) \qquad (\exists I: 3) } \\ 5. \qquad \exists a(a + a = a) \qquad (\exists E: 1, 2-4) }$
but I don't know how to prove $\exists a(b + a = b) \vdash \exists a(a + a = a)$. The two sequents are similar, except that I guess the second one is a bit weaker, but I would have thought it would be provable as well. The attempts I have made are as follows:
$\fitch { 1. \qquad \exists a(b + a = b) \qquad (A) }{ \fitch { 2. \qquad (b + b = b) \qquad (A) }{ 3. \qquad \exists a(a + a = a) \qquad (\exists I: 2) } \\ 4. \qquad \exists a(a + a = a) \qquad (\exists E: 1, 2-3) }$
The final line is an invalid inference, since the term used in the substitution on line 2 ($b$) is present in an undischarged assumption on line 1, violating the $\exists E$ rule. This is a consequence of using a term that already existed in the first assumption. So, I tried using a new variable as follows:
$\fitch { 1. \qquad \exists a(b + a = b) \qquad (A) }{ \fitch { 2. \qquad (b + c = b) \qquad (A) }{ 3. \qquad \exists c(c + c = c) \qquad (\exists I: 2) } \\ 4. \qquad \exists c(c + c = c) \qquad (\exists E: 1, 2-3) }$
Of course, the final line is also invalid here because $c$ is present in an undischarged assumption (line 2).
In summary, I have had no luck trying to prove this sequent. It seems like this sequent is true, since if there exists an $a$ such that $b + a = b$ (we know there is from experience: $a = 0$), then there exists an $a$ such that $a + a = a$ (which we also know from experience is true: $a = 0$). What mistake am I making?
EDIT: I think perhaps my flaw here is that I am using my intuition of what addition means in arithmetic, and placing this meaning on the function symbol +, which has no meaning in this context. If I was to remove these and replace with a notation $f(a,b)$ instead, it may not be true that $\exists a(f(b,a) = b) \vdash \exists a(f(a,a) = a)$ for all functions $f$. I'm just trying to think of a counterexample function where this does not hold for $f$.