This chapter 2 of GEB introduces the pq-system as a simple formal system with axioms and a rule of production to illustrate the power of such systems. It discusses decision procedures for determining theorems within a formal system, contrasting top-down and bottom-up approaches. The text then explores the concept of isomorphism as a basis for meaning by showing how pq-theorems can correspond to arithmetic addition, and introduces the distinction between meaningful and meaningless interpretations. Finally, the chapter touches upon the relationship between formal systems and reality, using mathematics and number theory as examples, and concludes with a playful dialogue, "Sonata for Unaccompanied Achilles," seemingly unrelated but potentially foreshadowing later themes