# Minimum number of axioms for ZFC set theory

What is the minimum number of axioms needed for ZFC Set Theory?

I have found that Suppes' Axiomatic Set Theory lists 7 axioms, but I am not sure if this can be reduced or not. Any references on this subject would be much appreciated.

Suppes' list:

1. Axiom of Extensionality
2. Sum Axiom
3. Power Set Axiom
4. Axiom of Regularity
5. Axiom of Infinity
6. Axiom Schema of Replacement
7. Axiom of Choice
• Note that 6 is an axiom schema, so is really a countably infinite set of axioms. All the others can be combined into one just by putting and between them and making one axiom. Jul 1, 2017 at 19:47
• @MichaelHardy: I said item 6 was a countably infinite set. That was exactly my point. Any finite set of axioms can be combined into one, but an infinite set cannot. I know, but have not pursued the proof, that ZFC is not finitely axiomatizable Jul 1, 2017 at 20:04
• To expand Ross Millikan's comment: Not only is the standard list of axioms of ZFC infinite, but no finite list is possible. This is a consequence of the reflection theorem. Jul 1, 2017 at 20:04
• @Michael: I feel like that's sort of like saying you only need finitely many decimal digits to write $1/3$, because you can write it as $0.\bar{3}$.
– user14972
Jul 1, 2017 at 20:26
• @MichaelHardy I don't think algorithmic proof-checking is the relevant issue here. One could surely design proof-checkers for a logic that allows schematic predicate symbols and has a rule of inference that lets you substitute arbitrary formulas for atomic formulas built using such a symbol. (Morse's book A Theory of Sets develops such a logic, though in the context of MK rather than ZF.) I think the infinitude of axioms involved in replacement is simply because one wants the underlying logic to be standard first-order logic (and not such a schematic extension). Jul 2, 2017 at 0:19

The reflection principle is a theorem schema in ZFC, meaning that for each formula $\phi(\vec x)$ we can prove in ZFC a version of the principle for $\phi$. In particular, it gives us that if $\phi$ holds (in the universe of sets) then there is some ordinal $\alpha$ such that $V_\alpha\models \phi$.
It follows from this that (assuming its consistency) $\mathsf{ZFC}$ is not finitely axiomatizable. Otherwise, $\mathsf{ZFC}$ would prove its own consistency, violating the second incompleteness theorem. The (standard) list of axioms you presented is actually an infinite list, with replacement being in fact an axiom schema (one axiom for each formula).
It is perhaps worth mentioning that no appeal to the incompleteness theorem is needed: If $\mathsf{ZFC}$ is consistent, and finitely axiomatizable, then it would prove (because of reflection) that there are $\alpha$ such that $V_\alpha\models\mathsf{ZFC}$. It would then follow that there is a least such $\alpha$. But inside $V_\alpha$ there must be some $\beta$ such that $$V_\alpha\models\mbox{}V_\beta\models\mathsf{ZFC}\mbox{''}$$ (because $V_\alpha$ is a model of set theory, so it satisfies reflection), and easy absoluteess arguments give us that then $\beta<\alpha$ is indeed an ordinal, and $V_\beta$ is really a model of $\mathsf{ZFC}$, contradicting the minimality of $\alpha$.
• (Of course, if $\mathsf{ZFC}$ is inconsistent, then it is finitely axiomatizable, and one axiom suffices.) Jul 1, 2017 at 20:15
• A similar argument applies to $\mathsf{PA}$: The (first-order) induction axiom is actually an axiom schema, and $\mathsf{PA}$ is not finitely axiomatizable, because it can prove the consistency of any of its finite fragments. Jul 1, 2017 at 20:17
It seems to me the OP is asking whether any of the 7 assertions (specifically 6 axioms and a schema) listed are unnecessary, i.e. whether we can remove any one of them and still derive all of ZFC (similar to how Suppes removed pairing and comprehension because they can be proved from the other axioms). And the answer to that is no, none of these 7 assertions can be proven from the other 6. E.g., ZFC-Infinity+ $\neg$Infinity holds in the model $HF,$ and is thus relatively consistent to ZFC.