 Frege’s Theorem is that the five Dedekind/Peano axioms for number theory can be derived from Hume’s Principle in second-order logic. In this section, we reconstruct the proof of this theorem; it can be extracted from Frege’s work using the definitions and theorems assembled so far. Some of the steps in this proof can be found in Gl. (See the Appendix to Boolos 1990 for a reconstruction.) Our reconstruction follows Frege’s Gg in spirit and in most details, but we have tried to simplify the presentation in several places. For a stricter description of Frege’s Gg proof, the reader is referred to Heck 1993. The following should help prepare the reader for Heck’s excellent essay.