How many axioms are in ZFC, and is ZFC a decidable language? I am reading Jech's book Set Theory and he lists 9 "axioms":

*

*Extensionality

*Pairing

*Schema of Separation

*Union

*Power Set

*Infinity

*Schema of Replacement

*Regularity

*Choice

Two of these are schema, which I take to be not really axioms, but instead something more like an indexed bundle of axioms.  Separation is indexed by any "property" which I take to be something written in the first-order language using the symbols = and $\in$.
Replacement is also a schema, this time indexed by all functions.  This is the part that kind of concerns me.  As I understand it, ZFC is a first-order language and is decidable.  I could well be wrong about that, but I thought the argument went something like this: As a first-order language with a decidable set of axioms, it is decidable.  But if we have an axiom for every function, that sounds like ... a whole lotta axioms.  And it doesn't sound decidable, since you would need a decision procedure for whether a given class is a function.
Probably I'm way off about a bunch of things.  Can anyone set me straight about (1) how many axioms are there? Uncountably many, if you say that for every function there is an axiom, right?  (2) Is ZFC decidable?
 A: I haven’t read this work of Jech, but it seems you are under a few misconceptions.
Replacement is not indexed by “all functions”. A function is an object discussed in ZFC, so it does not make sense to say there is one axiom per function. Instead, replacement is indexed over “properties” in the same way separation is.
Formally, consider any formula $P(x, y, w_1, \ldots, w_n)$ - that is, a formula $P$ in the language of set theory such that every variable which occurs free in $P$ is one of $x, y, w_1, \ldots$, or $w_n$. The instance axiom of replacement for $P$ states
$$\forall w_1 \cdots \forall w_n \forall a (\forall x \in a \exists! y P(x, y, w_1, \ldots, w_n) \implies \exists b \forall y (y \in b \iff \exists x \in a P(x, y, w_1, \ldots, w_n)))$$
It is clear that because there are only countably many such $P$, there are only countably many instances of replacement. It is also clear that deciding whether a particular sentence is an instance of the axiom scheme of replacement is decidable. The same is true for deciding whether a sentence is an instance of the axiom scheme of separation. Therefore, whether a sentence is an axiom of ZFC is decidable.
For the rest of the discussion, we assume ZFC is consistent.
We can encode sentences in the language of arithmetic into the language of set theory in such a way that makes ZFC an extension of Peano Arithmetic. Because ZFC is a recursively axiomatisable consistent extension of Peano Arithmetic, there is no algorithm which can decide whether a particular sentence can be proved in ZFC.
Finally, ZFC cannot be finitely axiomatised. There is a powerful principle called the “reflection principle”, which states that for all sentences $\phi$, ZFC proves that there is some transitive set $S$ such that $(S \models \phi) \iff \phi$. So for any list $A_1, \ldots, A_n$ of axioms of ZFC, we can prove in ZFC that there is some model of $\phi := A_1 \land A_2 \land \cdots \land A_n$, and thus the combination of axioms $A_1, \ldots A_n$ is consistent. If ZFC were finitely axiomatisable, then it would prove itself consistent, which is impossible by Gödel’s second incompleteness theorem.
So the set of axioms of ZFC is countably infinite and decidable, and we can’t cut the axioms down to a nice finite list while still having all the theorems of ZFC.
