 In what follows, we shall suppose that the second-order predicate calculus with which we began has been extended with (a) a primitive \(\#\) operator, so that we can formulate terms such as \(\#F\) to signify ‘the number of \(F\)s’, and (b) a new axiom, namely, Hume’s Principle, to govern the new terms. As previously mentioned, Frege’s Theorem is that the Dedekind/Peano axioms of number theory are derivable as theorems in a second-order predicate calculus extended in this way. In this section, we introduce the definitions required for the proof of Frege’s Theorem. In the next section, we go through the proof. In the final section, we conclude with a discussion of the philosophical questions that arise when we extend the predicate calculus in this way, and take Hume’s Principle as a replacement for Basic Law V.