You already know that first-order logic has a completeness theorem. That means that we can determine validity in first-order logic by looking at deductions - it makes proof theory possible. In second-order logic with full semantics, because there is no completeness theorem, to study things like validity we end up having to answer questions about the power set of the domain.
Here's an example. There is a sentence $\phi_1$ in the second-order language of ordered fields that characterizes the real numbers, up to isomorphism, in second-order logic with full semantics. There is another sentence $\phi_2$, in the language with just equality, which states that the domain has cardinality $\aleph_1$ (that is, any model of $\phi_2$ in second-order logic with full semantics has a domain of that cardinality). Now in order to show that $\phi_1 \to \phi_2$ in this logic, we would have to prove the continuum hypothesis, and to disprove that implication we would have to disprove the continuum hypothesis (this is because $\phi_1$ has only one model up to isomorphism).
Examples like this give us a sense that studying second-order logic with full semantics comes down, in many cases, to studying set theory. But if that's that case, many people say, why not just study set theory, as with ZFC? Studying set theory in the guise of "logic" only seems to obfuscate what's going on.
Moreover, for those who want to use the logic for foundational purposes, it is unattractive to pick a logic that seems to already have the answers to set-theoretic questions like the continuum hypothesis built into it - this goes against the idea that "logic" itself should make a minimal number of ontological assumptions.
This sort of argument was made in detail by Quine, who called second-order logic with full semantics "set theory in sheep's clothing". Not everyone agrees with this, and many people do use second-order logic with Henkin semantics as a way to keep the expressiveness without including the set theory. But the dominant opinion accepts Quine's argument.
I also recommend "The Road to Modern Logic-An Interpretation" by José Ferreirós, Bulletin of Symbolic Logic (2001), 441-484. This paper has a very nice historical study of the development of what is now called first-order logic.
There is a point of confusion in the question:
For instance, I've read that we can define addition in second-order arithmetic by writing
- $x+0 = x$
- $x+S(y) = S(x+y).$
Why does this work in second order arithmetic, but not in first-order?
That does not work in second-order arithmetic. It is an implicit characterization of the addition function, but it is not an explicit definition of the addition function in terms of the successor function.
A genuine definition is a formula $\phi(n,m,p)$ in a language without the addition symbol $+$ such that, for all natural numbers $n,m,p$, we have $n + m = p$ if and only if $\phi(n,m,p)$ holds. A "pseudo-definition" that is able to refer to the object being defined is called an implicit definition, but implicit definability is much weaker than actual definability.
One actual definition of addition of natural numbers in second-order arithmetic is:
$$
n + m = p \Leftrightarrow (\forall f)\left[ \left( f(0) = n \land (\forall k)[f(S(k)) = S(f(k)]\right ) \to f(m) = p\right].
$$
Here $n,m,p$ are natural numbers, $(\forall k)$ quantifies over the natural numbers, and $(\forall f)$ quantifies over all unary functions from the natural numbers to themselves. Notice that, crucially, the right side does not mention $+$. In the particular definition, we could also rewrite it with an existential function quantifier:
$$
n + m = p \Leftrightarrow (\exists f)\left( f(0) = n \land (\forall k)[f(S(k)) = S(f(k))] \land f(m) = p\right.)
$$
Why does this definition not work in first-order logic? Because, in a single-sorted first-order theory of arithmetic, it is not possible to quantify over functions in the way that the definition does.
Now, that does not prove that it is impossible to define addition of natural numbers in terms of successor. It only shows that the definition in second-order arithmetic does not go through unchanged.
One way to see that addition is not definable from successor is sketched in this answer by Alex Kruckman. The key point is that if we look at the first-order theory of the natural numbers with successor and a constant for 0, every formula in this language (with some free variables) is equivalent to a quantifier-free formula in the language (with the same free variables). A proof of that is given by Richard Kaye here. So if addition was definable in that structure, it would be definable by a quantifier-free formula. But by analyzing the form of such a formula we can show that it cannot define addition.
Actually, more is known. Neither addition nor multiplication is definable from successor alone; multiplication is not definable from successor and addition; and addition is not definable from successor and multiplication. The theory of the natural numbers with multiplication and addition is undecidable, but the restriction to just addition is decidable, and the restriction with just multiplication is decidable.
Best Answer
Each set of axioms has its own purposes, and neither is better than the other in all circumstances.
It is true that, when they are interpreted in set theory, the second-order Peano axioms are categorical. They are useful for characterizing the natural numbers once we have a notion of "set" to work with.
The second-order Peano axioms that most people think of are not so useful for reasoning about natural numbers. To be clear, I am referring to the following list of three axioms:
The issue in working "with" these axioms is that they don't tell you how to construct any set $X$ to apply the third axiom. So, if you want to proceed on an axiomatic basis, you have to add additional axioms to allow for the construction of sets, before you can actually use the third axiom in any nontrivial way.
For example, the categoricity proof that is mentioned in the questions is not proved "from" these axioms - it is proved "about" these axioms in the metatheory. Similarly, the definition of the addition function mentioned in the question is not proved from the three axioms, it is proved in the metatheory using set-theoretic methods.
When you add set existence axioms to the three above, in order to start writing formal proofs from the axioms, what you will be able to prove is strongly influenced by which set existence axioms you add. For example, we can make the theory known as "second order arithmetic" ($\mathsf{Z}_2$) by adding set existence axioms which quantify only over numbers and sets of numbers, or we can make a stronger theory by adding all the set existence axioms of ZFC. Each of these systems is able to prove many things that the three axioms above cannot prove in the usual deductive system for predicate logic.
On the other hand, the axioms of Peano arithmetic (which are the axioms of a discrete ordered semiring, abbreviated $\mathsf{PA}^-$, plus the axiom scheme of induction) can be used "as is" to prove many nontrivial theorems. They are particularly useful when we want to prove things about the natural numbers without getting involved in set theoretic issues and without referring to set existence axioms.