The separation axiom of ZFC states
Suppose some set $x$ exists, and let $C$ be any condition. Then there exists a set $y$ consisting of all and only the members of $x$ that satisfy $C$.
To translate this into FOL, and since they can't quantify over $C$s, people employ an axiom schema, an infinite set (?!) of axioms.
This seems circular to me (using sets to define sets?), but perhaps I'm misunderstanding something here.
Is it fair to say that ZFC axioms can not even be stated in FOL?
Best Answer
No, that's not true at all.
Let's start with the most basic of meta-theories: $\sf PRA$, the theory of Primitive Recursive Arithmetic. Here we have the natural numbers, and the primitive recursive functions.
This theory is strong enough to internalise FOL, so we can just assume that we're manipulating strings. The point of an axiom schema is that it is a predicate that lets us recognise all the axioms which have a certain form. And any reasonable schema, including those of $\sf ZFC$, are in fact primitive recursive. In other words, there is a primitive recursive function $f_{\rm Sep}(n)$ which takes in $n$, and if $n$ is the Gödel number of a formula with some basic properties $\varphi$, then $f_{\rm Sep}(n)$ is the Gödel number of the axiom obtained from the schema by putting $\varphi$ into it. If $n$ is not the Gödel number of a suitable formula, just return the axiom for the formula $\varphi$ given by $x=x$ or something like that.
Since $\sf ZFC$ is presented as finitely many axioms and one or two schemata (Separation and Replacement, but Replacement is generally enough to prove Separation, making it redundant), then the collection of Gödel numbers of axioms of $\sf ZFC$ is in fact primitive recursive. So we can really talk about the first-order theory that is $\sf ZFC$.
To recap, the point of the schemata is to allow us to have infinitely many axioms with the same structure—that we can recognise mechanically—so that when we need to use any such axiom in a proof, we can always be sure that it is part of this or not.
Another way to approach this is by saying that our foundation is in fact $\sf ZFC$. We use set theory to discuss set theory. This sounds circular, but how is this any different than using $\sf PRA$ to study the logical consequences of $\sf PRA$? It's not. Mathematics is not something that we do in vacuum, some assumptions are needed. And it is perfectly fine to study $\sf ZFC$ inside $\sf ZFC$.
There, we have the notions of sets already existing, so we can talk about a set of axioms. Of course, we need to argue why a certain set exists, which is to say that we need to be able to prove that the set of these axioms actually exists. And again we use the fact that a schema is a function which takes formulas and returns axioms, so we may replace the schema with the axioms, as it is the range of this function.
So again, we have that $\sf ZFC$ is a set of first-order axioms in the language of set theory.