A simple formal system (the MIU-system) is presented, and the reader is urged to work out a puzzle to gain familiarity with formal systems in general. A number of fundamental notions are introduced: string, theorem, axiom, rule of inference, derivation, formal system, decision procedure, working inside/outside the system. (p. viii)
While you read
- In principle, any three letters could have been chosen for the puzzle. Why were “M”, “I”, and “U” employed?
- What does it mean to be “in possession of a string”?
- The text states that from MU you can get MUU. It's a true statement. Does that imply that you can get MU? If so, then the puzzle is solved!
- How does a theorem differ from an axiom (both in mathematics and the sense used in GEB)?
- You've probably become convinced that, when MI is the only axiom, all theorems will begin with M. How did you become convinced of that? Which mode of reasoning are you using -- M-mode, I-mode, or U-mode? Or if you're not convinced, why not?
- Hofstadter suggests that the numbers 3 and 2 play important roles in the MIU-system. What roles?
- Will the decision tree shown in Figure 11 (p. 46) produce every theorem of the MIU-system from the axiom MI?
- Be sure to try the puzzle as stated! Is MU a theorem? Why or why not?
- You've found a number of MIU-theorems that can be derived from MI. You can do the reverse with at least some of them: you can start from one of those theorems and derive MI. (Example: MIUU.) If a theorem x can be derived from MI and MI can be derived from x, let's call them "equivalent".
- Are there theorems that aren't equivalent to MI?
- Can you make rules that generate only theorems that are equivalent to MI?
- Can you make a decision procedure for the MIU system, which takes in any string of M, I, and U and tells you definitively that it's a theorem or not a theorem? To do this, you have to do things besides just applying the rules, because the rules don't tell you about non-theorems.
- Can you make another decision procedure that decides whether a string is equivalent to MI?
(For example, here we might work through some examples of MIU-system derivations, and link to scripts in some programming languages that implement the system.)
Working inside and outside of the system
(This is an important concept for understanding what the Tortoise's point is, in the following Two-Part Invention.)
(For example, here we might refer to other sets of axioms, such as Euclid's. We can also try to put Post production systems in context.)
(This section is for adding your thoughts about the chapter. Sign what you write with your user name. Others may edit this section for length later. More free-form, unedited discussion can take place in the comment section below.)