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?
In a first order theory of "widgets", all objects the theory makes statements about, are widgets. In a second order theory of widgets, we additionally have statements about sets of widgets or possibly relations of higher arity and can quantify over such.
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).
The language of set theory is powerful enough to "emulate" sets/relation/functions of sets as in higher-order theories. But an important point is that it is the axioms themselves that describe what counts as set. For example, if we replace the Axiom of Infinity with its negation, then there are no infinite sets in ZFC, hence also all sets of sets/relations between sets/functions of sets that we can express in ZFC as just sets are also finite, whereas a second order theory would still allow us to quantify over all sets of sets (including infinite sets of -necessarily finite - sets).
You asked specifically for a formulation of the axiom of choice:
$$ \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}$$