ZFC: Zermelo-Fraenkel Set Theory with Choice [000I]

ZFC is a pure set theory meaning that every object is a set. It uses the same logical axiom scheme and inference scheme as PA - but the resulting axioms are different.

The Zermelo-Fraenkel axioms are (TODO: write them out).

1. Extensionality
2. Pairing
3. Union
4. Power set
5. Infinity
6. Foundation
7. Choice
8. Separation scheme
9. Replacement schme