 Frege’s system is an axiomatization of what has come to be known as second-order logic, which is an important extension of classical quantificational logic. Hilbert &amp; Ackermann (1928) contains the first axiomatic treatment of quantificational logic as a subject of its own, which they called “the narrower functional calculus”. In what follows, we look at what is now a common axiomatization of pure quantificational logic. This axiom system adopts all tautologies of propositional logic as axioms and modus ponens as a rule of inference, and it supplements them with two more axiom schemata and a rule of universal generalization. The first two axiom schemata are: