Overview[]
The MU-puzzle
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[]
Questions[]
Many of these questions were adapted from Curry and Kelleher's lecture notes for this chapter.
- 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?
Topics[]
The MIU-system[]
(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.)
Further reading[]
(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.)
Commentary[]
(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.)
Links[]
- "The MU-puzzle" 2012 Read Through Discussion Thread on Reddit
- Web interactive MIU game developed by Gihan Marasingha using the Lean Game Maker