The title of this book is not at all a pun, as it might seem at first glance. Metamathematics is a theory that studies formalized mathematical theories. A formalized theory is, roughly speaking, the set of some finite sequences of symbols called formulas and terms, and the set of some simple operations performed on these sequences. Formulas and terms produced by a few simple rules serve as substitutions for the proposition and functions of intuitive mathematical theory.