First-Order Logic vs. Second-Order Logic

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

The statement is indeed a first order statement in standard Set Theory. But it is no wonder you are a bit confused.

Most people think of sets and elements as different things. However, in standard set theory this is not the case.

In standard set theory, everything is a set (there are no "ur-elements", elements that are not sets). The objects of set theory are sets themselves. The primitive relation $\in$ is a relation between sets, not between ur-elements and sets. So, for example, the Axiom of the Power Set in ZFC states that $$\forall x\exists y(\forall z(z\in y \leftrightarrow z\subseteq x))$$ which is a first order statement, because all the things being quantified over are objects in the theory (namely, "sets").

So you need to forget the notion that "elements" are things in sets and sets are things that contain elements. In ZF, everything is a set.

It's a little hard to see the distinction between first and second order statements in ZF precisely because "sets" are the objects, and moreover, given any set, there is a set that contains all the subsets (the power set). In a way, the Axioms are set up precisely to allow you to talk about collections of sets without having to go to second order logic.

In ZF, to get to second order you need to start talking about "proper classes" or "properties". For instance, that's why Comprehension is not a single axiom, but an entire infinite family of axioms. Comprehension essentially says that for every property $P$ and every object $x$ of the theory (i.e., every set $x$), $\{y\mid y\in x\wedge P(y)\}$ is a set. But trying to quantify over all propositions would be a second order statement. Instead, you have an "Axiom Schema" which says that for each property $P$, you have an axiom that says $$\forall x\exists y\Bigl(z\in y\leftrightarrow\bigl(z\in x\wedge P(z)\bigr)\Bigr).$$ If you try quantifying over "all $P$", then you get a second order statement in ZF.

Replace the non-logical relational symbol ∈ with R and the confusion goes away. Your problem arises from the fact that the symbol ∈ makes you confuse the neutral symbol of the language of set theory (which has no properties other than those expressed by axioms of the theory) with the intended interpretation of the symbol about real sets. The set theories like ZF have very strange models which has nothing to do with the intended model and interpretation of the relation $R$ has nothing to do with the real membership relation between sets.

A first-order theory can have many sorts and the intended meaning of some of those sorts can be higher type objects, e.g. we can have a two sorted theory where the intended meaning of the objects of the first sort are natural numbers and the intended meaning of the objects of the second sort are sets of natural numbers. We can quantify over them and the theory is still first order, though it has two sorts. The models of this theory needs to have two sets, one for interpreting the objects of the first sort and the other for interpreting the objects of the second sort, but there does not need to be any relation between these two sets that are used for interpreting objects even if the intended interpretation for the second sort of sets of objects from the first sort. The only properties of that these two sets need to satisfy are those expressed by axioms of the theory. You can add axioms of a set theory like ZFC for the second sort and consider objects of the first sort as urelements of the set theory that satisfying some other axioms e.g. first order Peano Arithmetic. This is still a first order theory. And the theory will have models where the interpretations of the two sort are not related in the intended way, i.e. the objects of the second sort will not be the sets of objects of the first sort, and there are no way to enforce this syntactically, i.e. using axioms.

A second- or higher-order theory enforces some restriction on possible interpretations of some sort which are called the higher sort. These restrictions are not syntactical, i.e. they are not axioms of theory, but semantical, i.e. we restrict the models of the theory to those that satisfy some certain conditions, e.g. the members of the set interpreting the second sort in the two sorted number theory I mentioned above are really the sets of objects of the first sort. This is like assuming some amount of set theory semantically. Without these semantical restrictions about interpretation the theory is still first order.

The higher-order theories are interesting for studying things like natural numbers. The (complete/full) second-order Peano arithmetic will force the set interpreting the second sort to be exactly the powerset of the first sort. Note that this theory is not axiomatizable, i.e. there are no set of first order axioms that will capture exactly these models. (In fact even weaker version of this second-order set theory which do not require the existence of all subsets of the first sort are not axiomatizable.)

On the other hand, I don't know any higher order set theory, and in fact the concept itself seems a little bit unnatural (of course it can be due to my lack of knowledge).