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.
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:
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.