In this section, we'll talk about the various formal systems that get used in the book.  I'll try to describe them informally for non-technical readers, and then offer successively deeper versions for those who want them.