## Overview Edit

**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 Edit

### Questions Edit

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?

- Are there theorems that
- 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 Edit

### The MIU-system Edit

(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 Edit

(This is an important concept for understanding what the Tortoise's point is, in the following Two-Part Invention.)

## Further reading Edit

(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 Edit

(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.)