Wikipedia describes the first-order vs. second-order logic as follows:
First-order logic uses only variables that range over individuals (elements of the domain of discourse); second-order logic has these variables as well as additional variables that range over sets of individuals.
It gives \forall P\,\forall x (x \in P \lor x \notin P) as an SO-logic formula, which makes perfect sense to me.
However, in a post at CSTheory, the poster claimed that \forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y)) is an FO formula. I think this must not be the case, since in the above formula, x and y are sets of individuals, while z is an individual (and therefore this must be an SO formula).
I mentioned this as a comment, but two users commented that ZF can be entirely described by FO logic, and therefore \forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y)) is an FO formula.
I’m confused. Could someone explain this please?
It seems to me that you’re confusing the first order formulas with their intended interpretations.
The language of set theory consists of just a single 2 place predicate symbol, usually denoted \in. The statement you quote is a first order statement – it means just what is says: “for all x and for all y, (x = y iff for all z, (z \in x iff z \in y))”, but it does not tell you what x is. When you say “but x is a set and z is an individual, so this statement looks second order!”, you’re adding an interpretation to the picture which is not specified by the first order formula alone – namely that “for all x” means “for all sets x” and “\in” means “the usual \in in set theory”.
In first order logic, this “adding of interpretation” is usually called “exhibiting a model”.
Here’s another way of looking at this same first order statement. Suppose I reinterpret things – I say “for all x” means “for all real numbers x” and \in means <. Then, \forall x \forall y (x=y iff \forall z, (z \in x iff z \in y)) is a true statement: it says two real numbers are equal iff they have the same collection of smaller things. Notice that in this model, nothing looks second order.
By contrast, in second order logic, you are directly referring to subsets, so that in any model (that is, interpretation), \forall S means "for all subsets of whatever set the variable x ranges over".