In order to avoid the paradoxes and put it on a firm footing, set theory had to be axiomatized. The first axiomatization was due to Zermelo (1908) and it came as a result of the need to spell out the basic set-theoretic principles underlying his proof of Cantor’s Well-Ordering Principle. Zermelo’s axiomatization avoids Russell’s Paradox by means of the Separation axiom, which is formulated as quantifying over properties of sets, and thus it is a second-order statement. Further work by Skolem and Fraenkel led to the formalization of the Separation axiom in terms of formulas of first-order, instead of the informal notion of property, as well as to the introduction of the axiom of Replacement, which is also formulated as an axiom schema for first-order formulas (see next section). The axiom of Replacement is needed for a proper development of the theory of transfinite ordinals and cardinals, using transfinite recursion (see Section 3). It is also needed to prove the existence of such simple sets as the set of hereditarily finite sets, i.e., those finite sets whose elements are finite, the elements of which are also finite, and so on; or to prove basic set-theoretic facts such as that every set is contained in a transitive set, i.e., a set that contains all elements of its elements (see Mathias 2001 for the weaknesses of Zermelo set theory). A further addition, by von Neumann, of the axiom of Foundation, led to the standard axiom system of set theory, known as the Zermelo-Fraenkel axioms plus the Axiom of Choice, or ZFC.