What are some benefits of a second order logic?

I have read that a second-order logic can help one define equality by quantifying over all predicates such as what is done in the following definition:

(x=y):⟺[∀P:P(x)⟺P(y)]

By contrast a first-order logic with identity would define "=" as a primitive logical symbol.

Besides this benefit, but using it as an example of a benefit, what are other uses or benefits of a second-order logic over a first-order logic?

Han de Bruijn (https://math.stackexchange.com/users/96057/han-de-bruijn), Leibniz' Law and that good old riddle, URL (version: 2013-12-18): https://math.stackexchange.com/q/608947

• It depends on what counts as a benefit. Second order logic is believed to be closer to our natural reasoning. In particular, one can formulate induction in a natural way for all predicates instead of postulating it for each predicate one at a time as in the first order induction schema. One can also exclude the non-standard models of arithmetic by using it. Boolos argued that natural language constructions with plural quantification are modeled by the second order logic. On the other hand, it is technically unwieldy, there is no good proof theory for it. Commented Sep 1, 2019 at 22:57
• Commented Sep 2, 2019 at 7:15
• Commented Sep 2, 2019 at 7:18
• As for natural language constructions which Conifold brought up, not only plural NPs, but also many other perfectly common natural language expressions can only straightforwardly be translated in the language of second order logic: for instance, quantifiers like more than or most can be proven not to be first-order definable; and adverbs (e.g. slowly(walk)) as well many ordinary adjectives/nouns/verbs (e.g. color(red) or is-a-property(color)) are properties of properties (of properties) and thus higher-order concepts. Commented Sep 2, 2019 at 9:25