# Is ZFC a first- or third-order theory?

I keep finding everywhere that ZFC is a first-order theory, but something sounds wrong about the axiom of choice.

It reads for every family of sets you can select elements so that you have a set. Isn't that a third-order quantifier?

What I understand:

• "for every element in a set" - first-order quantifier
• "for every set in a family" - second-order quantifier
• "for every family (of all families of sets)" - third-order quantifier.

How can we write the axiom of choice as a first-order statement, without quantifying over families of sets?

• A family in this context is also just a set, which is the single type of object of ZFC Commented Jun 11, 2018 at 19:14

For example, $$\tag1 \forall a\forall b\colon a>b\to a\ge b+1$$ is a first order statement that happens to be true if the domain of dicourse is the natural numbers. While specific relations ($<$, $\le$) and operations ($+$) occur here, we do not quantify over them. Rather, these specific relations are part of the language (originally or by extension). On the other hand, $$\tag2\forall S(\exists a\colon a\in S)\to (\exists a\forall b\colon a\in S\land (b\in S\to b\ge a))$$ is a second statement in which we quantify not only over natural numbers ($a$, $b$), but also over sets of natural numbers ($S$). And in $$\tag3\exists f\forall a\forall b\colon(f(a)\ne 1\land (f(a)=f((b)\to a=b))$$ we quantify over functions. To this end, we use different sorts of variables (in the above, indicated by suggestive variable names).
In ZFC, there is only one sort of variable: variables for sets. And there is only one specific relation (apart from equality) that is part of the language and denoted by the same symbol $\in$ that we use in a higher order theory to denote the element-of relation between "widgets" and sets of "widgets". So in $(2)$, $a\in S$ means that the number $a$ is an element of the set of numbers $S$. Whereas $C\in A$ in $$\tag4 \forall A\forall B\exists C\colon ((C\in A\leftrightarrow C\in B)\leftrightarrow A=B)$$ can be viewed as simply expressing that $C$ and $A$ are in this specific part of the language relation, the special properties (or even meaning) of which are further specified by $(4)$ (and other axioms).
\begin{align}\forall A\colon&( \forall B\exists C\colon (B\in A\to C\in B)\\&\land \forall B\forall C\forall D\colon(B\in A\land C\in A\land D\in B\land D\in C\to B=C) )\\&\quad\to \exists F \forall B\exists C\forall D\colon (B\in A\to C\in B\land C\in F\land(D\in B\land D\in F\to D=C))\end{align}