I already know how to prove this statement in "English," but I would to see a proof of it entirely in first-order logic. Here is the English proof:
(1) Let $\{a_n\}$ and $\{b_n\}$ be arbitrary sequences.
(2) Assume $\lim_{n\to\infty} a_n = a$ and $\lim_{n\to\infty} b_n = b$.
(3) This means for every $\epsilon_a >0$ there exists $N_a$ such that for every $n \in N$, if $n\geq N_a$, then $\left|a_n-a\right|< \epsilon_a$ and for every $\epsilon_b >0$ there exists $N_b$ such that for every $n \in N$, if $n\geq N_b$, then $\left|b_n-b\right|< \epsilon_b$.
(4) Now, let $\epsilon>0$.
(5) Since $\lim a_n = a$ and $\lim b_n = b$, there exists $N_a$ such that for every $n \in N$, if $n\geq N_a$, then $\left|a_n-a\right|< \epsilon_a= \epsilon/2$ and there exists $N_b$ such that for every $n \in N$, if $n\geq N_b$, then $\left|b_n-b\right|< \epsilon_b = \epsilon/2$.
(6) Choose $N=\max\{N_a, N_b\}$.
(7) Let $n$ be a natural number.
(8) Assume $n\geq N$.
(9) Notice that $\left|(a_n + b_n) - (a+b)\right| = \left|a_n + b_n - a - b\right| = \left|(a_n-a) + (b_n-b)\right|$.
(10) By the triangle inequality we have $\left|(a_n-a) + (b_n-b)\right|\leq \left|a_n-a\right| + \left|b_n-b\right|$.
(11) Since $N=\max\{N_a, N_b\}$, if $N=N_a$, then $N=N_a\geq N_b$. Also, since $n\geq N$, we have $n\geq N_a\geq N_b$. So, $\left|a_n-a\right|< \epsilon/2$ and $\left|b_n-b\right|< \epsilon/2$. The same result holds if $N=N_b$.
(12) So, we have $\left|(a_n + b_n) - (a+b)\right|=\left|(a_n-a) + (b_n-b)\right|\leq \left|a_n-a\right| + \left|b_n-b\right|<\epsilon/2 + \epsilon/2=\epsilon$.
(13) Finally, we can conclude that $\lim a_n + b_n = a + b$. Q.E.D.
The first thing I would like to see is a formal line by line first-order logic proof of the above with each step justified. I'm not sure how to translate the above with quantifiers and I'm not sure what order to present each step of the proof.
Also, recall step (5) where we have "for every $\epsilon_a >0$ there exists $N_a$..." and "for every $\epsilon_b >0$ there exists $N_b$..." This step translates $\lim a_n = a$ and $\lim b_n = b$ using the definition of the limit. Is it wrong to put subscripts on each $\epsilon$ and $N$ for $\lim a_n =a$ and $\lim b_n=b$? I guess I don't understand why we need the subscripts.
Why on Earth do you want this? Even just the triangle inequality will become the silliest most tedious exercise possibly in history.
– crf Mar 06 '13 at 04:33