I am trying to get a grasp about the mechanicly difference between First order logic (FOL) and Second order logic (SOL). From my understanding objects within them can be divided into these parts
At which formula/terms are constructed recursively. My understanding is that FOL allows the quantifiers, $\exists,\forall$, can range over variables, while in SOL it can range over predicates too, is that correct? I don't want to understand it as "ranging over sets" because that is when we go for a set theoretical intepretation of it but I want to understand it mechanicly.
Onto set theory though as it baffles me.
Two simple sentences $$\forall x\forall y\exists z(x\in z\land y\in z)$$ $$\forall P\forall x(x\in P\lor x\notin P)$$
The former is a FOL statement, the latter a SOL statement. The first is axiom of pairing in ZFC and the latter is an example from wikipedia. If my previous understanding is correct, then how is the latter SOL but not the former, or vice versa? They both talk about objects being in sets that they range over and in ZFC all objects are sets.
A hypothesis I had for it is that the predicate $\in$ is usually seen as binary but you can technically have it as an unary by having it be $\in P$ instead, at which it would range over a form of predicate to be SOL, but then we get the same intepritation for the former as well.
I have tried rewriting it as
$$\forall x\forall y\exists z(P(x,z) \land P(y,z))$$ $$\forall z\forall x(P(x,z)\lor \neg P(x,z))$$
to get rid of the set theoretical view of it, and quite frankly it only makes them look even more the same.
Any clearification on this would be most appriciated!