 Let us briefly take stock of the situation as it existed in 1915. Peirce had differentiated between first-order and second-order logic, but had put the distinction to no mathematical use, and it dropped from sight. Both Frege and Russell had formulated versions of multi-level type theory, but neither had singled out the first-order fragment as an object worthy of study. The American postulate theorists, Edward Huntington and Oswald Veblen, had formulated various notions of completeness and categoricity, and Veblen had remarked that axiomatic deducibility might diverge from semantic implication (Awodey &amp; Reck 2002: 15–19). But Veblen did not possess a precise characterization of formal deduction, and his observation remained inert. Löwenheim had proved a deep theorem about what in retrospect could be characterized as first-order formulas, but had not isolated a system of first order logic. A similar point holds for Hermann Weyl, who in 1910 proposed (in effect) to use first-order logic to make precise the concept of “definite property” in Zermelo’s axiom of separation. But this, too, is a retrospective characterization, and Weyl’s interest was in set theory, not in the study of a system of first-order logic.