Requires a Wolfram Notebook System
Interact on desktop, mobile and cloud with the free Wolfram Player or other Wolfram Language products.
Explore the MIU-system  by clicking the red buttons, each of which represents the creation of a new theorem of the system by applying a rule of inference to a previously found theorem. The main features of the display are (a) the list of rules for your reference; (b) the current theorem (framed in blue); and (c) the options possible by applying all rules in all possible ways, given as a list of four lists of red buttons.[more]
For example, starting with , the options are , meaning that the result is if you apply rule 1, if rule 2, and no results from rules 3 and 4.
You choose a path through the system, starting with the axiom and deriving a sequence of theorems. Below the current options (the possible branches to follow) is displayed the path that led to this point, including the theorems generated and the rules applied. Buttons to back up one step and to restart from the beginning and a slider to choose a different starting axiom are provided. This Demonstration is a power tool for considering the MU-puzzle : is it possible to generate the theorem from the axiom ?[less]
Contributed by: Ken Caviness (March 2011)
Open content licensed under CC BY-NC-SA
This Demonstration lets you explore the MIU-system and the MU-puzzle , an example formal system and accompanying challenge introduced by Douglas Hofstadter in Chapter 1 of Gödel, Escher, Bach as a means of illustrating the important elements of formal systems (axioms, theorems, rules of inference), the mechanical and intelligent modes of treating a formal system, and the concept of a decision procedure. The four rules of inference of the system are shown. The MU-puzzle is to start with the axiom and derive (or generate, or prove) . Rather than simply generating all possible theorems , at each step all choices are displayed and you are invited to pick a path to follow by clicking one of the buttons shown in the main window. The growing path (the current theorem's proof) is also displayed. This removes much of the drudgery of the -mode for solving the puzzle, and frees the human researcher to more easily make the jump to -mode (i.e., to jump outside the system and think about it).
Possible theorems of the system consist of strings of the letters , , . Only one theorem is given at the start: the axiom. Other theorems must be generated by applying the rules to the axiom (or any other already-generated theorem). The and in the rules can stand for any valid substrings (including the length 0 string).
Snapshot 1: starting point for the MU-puzzle. Only the axiom "MI" is given, but either rule 1 or rule 2 can be applied at this point. If rule 1 () is applied with the standing for , we have . The application of rule 2 () with representing gives . The empty lists for rules 3 and 4 indicate that they cannot be applied at this point: the patterns do not match.
Snapshot 2: a situation in which any of the rules could be applied. In the case of rule 3 (), depending on the choice of , the match can occur in three ways: , , or , resulting in , , or , respectively. The match for rule 4 () can also occur in multiple ways with : or , but since the result will be in either case, the duplicate case is not shown.
If the path becomes too long or its continuation is obvious, the "back up" button can be used to return to a more interesting branch. (But note that the MIU-system does not allow reversing the direction of theorem generation, so in backtracking we are reverting to an earlier position on the path, not "moving backwards".) The restart button can be used to simply start over from the axiom.
Snapshot 3: the same situation shown in compact display mode, using exponents to shorten the strings shown. For example, and .
Snapshot 4: going beyond the MU-puzzle. Adjusting the slider and then clicking the restart button lets you explore other regions of the MIU-system, starting with alternative axioms, but for many axioms (such as the one shown here, ) none of the rules can be applied and no additional theorems can be generated.
 Douglas R. Hofstadter, Gödel, Escher, Bach: An Eternal Golden Braid, New York: Basic Books, 1979.
 For an example of this, see "Hofstadter's MU Riddle" in the Related Links section below.