A version of set theory which is a formal system expressed in first-order predicate logic. Zermelo-Fraenkel set theory is based on the Zermelo-Fraenkel axioms.
Zermelo-Fraenkel set theory is not finitely axiomatized. For example, the axiom of replacement is not really a single axiom, but an infinite family of axioms,
since it is preceded by the stipulation that it is true "For any set-theoretic
formula 
."
Montague (1961) proved that Zermelo-Fraenkel set theory is not finitely axiomatizable,
i.e., there is no finite set of axioms which is logically equivalent to the infinite
set of Zermelo-Fraenkel axioms. von
Neumann-Bernays-Gödel set theory provides an equivalent finitely axiomized
system.
