How many axioms does ZFC have?

Question

ZFC doesn't have finitely many axioms because it has some axiom schemas. Let's look at Axiom Schema of Specification:

$$ \forall X \exists Y \forall a \quad (a \in Y \iff a \in X \land P(a)) $$

This specifies a different axiom for each predicate $P$. Since $P$ is essentially a function from $X$ to boolean values, taken literally as $X$ is an arbitrary set, this axiom schema specifies uncontainably many axioms. That is, the class of axioms this axiom schema specifies is not a set.

Still, I think this axiom schema actually specifies countably infinite axioms, because we can construct an $X$ and a $P$ only in finitely long "text" with finitely many "characters". Is this the case?

Answer 1

In the schema that you've written $P$ needs to be a formula of the language of set theory. The language of set theory is finite, and formulas are finitely long, so there are only countably many $P$ available to consider.

In other words, not every function from $X$ to $\{T, F\}$ is eligible to be $P$ in the schema.

Answer 2

A "predicate" in this context is not an arbitrary Boolean-valued function on $X$. Instead, $P$ is restricted to predicates that can be written down as formulas in the language of set theory. Such a formula is a finite string of characters from a finite alphabet, so there are only countably many of them.

(Technical point: the predicates used in the axiom schemas are allowed to have parameters; i.e., they are allowed to refer to arbitrary individual sets. However, this doesn't change the fact that there are only countably many relevant predicates, because you handle the parameters by representing them as a variable with an extra quantifier. For instance, Separation for a formula $P(x,y)$ with two free variables says that $$\forall b\forall X \exists Y \forall a \quad (a \in Y \iff (a \in X \land P(a,b)))$$ where the variable $b$ is serving as a parameter (and the outer $\forall b$ means you can substitute any set for it.))

Answer 3

You already have two answers correctly explaining that the specification schema of ZFC uses only those $P$ that can be expressed by first-order formulas in the language of set theory. But it might be of historical interest to mention that Zermelo's original axiom system (of 1908) did not have this restriction on $P$. He required only that $P$ must express a "definite property", and he gave no mathematically precise definition of what that means. The suggestion that "definite" should mean "first-order expressible" was made by Skolem about a decade later. Zermelo didn't like it at all; if I remember correctly, he denounced it in paper of 1930. Nevertheless, Skolem's suggestion was incorporated when setting up the theory ZFC in first-order logic.