Terry Tao's 2007 post on nonfirstorderizability and branching quantifiers gives an interesting view of the boundary between first- and second-order logic. Key quote:

Moving on to a more complicated example, if Q(x,x’,y,y’) is a quaternary relation on four objects x,x’,y,y’, then we can express the statement

For every x and x’, there exists a y depending only on x and a y’ depending on x and x’ such that Q(x,x’,y,y’) is true

...but it seems that one cannot express

For every x and x’, there exists a y depending only on x and a y’ depending only on x’ such that Q(x,x’,y,y’) is true

in first order logic!

The post and comments give some well-known theorems that turn out to rely on such "branching quantifiers", and an encoding of the predicate "there are infinitely many X" which cannot be done in first-order logic.