 Quine (1969), chapters XI and XII, is a masterly tracing of a route consisting of incremental theoretical adjustments that one could in principle make, beginning with the type theory of Principia Mathematica (PM), and ending with Zermelo-Fraenkel set theory. The purpose behind postulating the Axiom of Reducibility in type theory, as already observed, was to ensure that every propositional function is coextensive with a predicative one. As Quine points out, however (and as Ramsey had pointed out before him), the Axiom of Reducibility really defeats the purpose behind its own postulation, thereby motivating the adoption of a simple type theory in place of PM’s ramified one. If one then reformulates simple type theory with ‘general’, or untyped, variables, and lets the types be cumulative (rather than remain stratified one from another without overlap), one effects the segue to Zermelo set theory. Fraenkel’s Axiom Scheme of Replacement finally allows one to “[pierce] all type ceilings” (Quine 1969: 282), and reach Zermelo-Fraenkel set theory. Replacement says that any function that is defined on a set as its domain has a set as its range. This allows one to form, for example, for any transfinite ordinal number κ, the set 