 Early twentieth-century formalizations of logic used what were called “substitution rules” with finite set of axioms instead of schemata that specified infinitely many axioms. These “substitution rules” were not the familiar rules for “substituting equals for equals”; rather they were closer to what are called instantiation rules today. The intuitive motivation for “substitution rules” was very simple but the syntactic details for implementing them were “intolerably complex”—to use the words of Paul Rosenbloom (1950: 109). In fact several first-rate logicians were led to make embarrassing errors, as Rosenbloom documents in the place just cited. Church (1956: 158) credits von Neumann with “the device of using axiom schemata”, which rendered the (notoriously difficult to state) substitution rule unnecessary.