The MU-puzzle

The most important thing to understand about the MU-puzzle is that following rules and reasoning about those rules produce different kinds of evidence. A legal derivation proves that its final string is reachable; a long unsuccessful search proves only that one particular search did not reach its target. Today you will build a precise rulebook, derive one theorem from start to finish, and leave with a search receipt that says exactly what has and has not been established.

The puzzle asks whether the string MU can be produced from MI. Its world is deliberately small: three symbols, one starting string, and four one-way rules. That smallness removes every excuse for an illicit move. If MU is reached, every line must name the previous line and the rule used. If it is not reached within a chosen budget, the honest result is still “not seen yet,” not “impossible.”

Boundary. This lesson studies formal systems, derivations, and bounded search. It intentionally does not give the later number-theoretic argument that settles the MU question; importing that result would erase the distinction this chapter is designed to teach.

Without a fixed rulebook, a clever-looking change has no evidential value, so the first job is to say what moves exist and what objects they act on. A formal system is an alphabet of symbols, one or more starting strings called axioms, and mechanically checkable transformation rules; a string is an ordered sequence of symbols, not a bag whose letters may be rearranged.

The MIU-system has alphabet {M, I, U} and the sole axiom MI. In the rules below, x is a metavariable: it belongs to our description of the system and stands for any possibly empty suffix. It never appears in a legal MIU string.

A legal rule in isolation is not enough, because the conclusion depends on the entire chain; one bad link destroys the claimed result. A derivation is a finite, line-by-line record that begins with an axiom and produces each later string by one named legal rule.

Here is one bounded journey from MI to MUIU:

A derivation proves membership when it succeeds, but a search that has not succeeded may still have unexplored branches, so stopping creates an epistemic boundary. A search frontier is the set of generated states whose legal successors have not yet been explored; an exhaustive search is one that eventually expands every finite derivation, not one that finishes the infinite tree.

Breadth-first search expands all derivations of length zero, then one, then two, and so on. This ordering guarantees that if a target has some finite derivation, the search will eventually find a shortest one. It does not guarantee a stopping time when the target has no derivation.

Source trace. Chapter I’s systematic genie and Figure 11, printed pages 39–40, motivate level-by-level generation and the difference between eventual discovery and a finite decision. This is a conceptual reconstruction: the budget, ordering selector, frontier metric, and target readout make the search boundary explicit but do not occur as an interface in the source.

Protocol. Set Target to a string with a short visible derivation, raise Search budget, and compare Search order settings until the target appears; record its expansion number and the visible frontier count. Then choose MU, repeat with both Search order settings, and raise Search budget several times. Watch the nodes-expanded and strings-discovered metrics change while the verdict remains “not found within budget,” and state why that readout is weaker than “not a theorem.”

Limits. No finite budget settles an unsuccessful infinite search. Search order can change time-to-witness dramatically without changing the original theorem set, and de-duplication can hide how many distinct derivations reach one string. The lab demonstrates finite prefixes only; it neither proves that MU is impossible nor supplies the later invariant that can decide the puzzle.

This distinction is operationally expensive when ignored. A software test runner that finds no failing input within one million cases has measured a search budget, not proved correctness. An agent that fails to retrieve a document may have exhausted its context window or search plan, not shown that the fact is absent. A startup with no conversions after fifty visits has a bounded observation, not proof of no demand; a daily search for lost keys that skipped one room has the same open frontier.

The search can feel conclusive merely because it is tiring, and that confusion turns effort into a false proof. Working inside the system means applying its four rules to strings; working outside means making a claim about every legal derivation, the shape of the theorem tree, or the behavior of a search procedure.

Inside evidence has the form “here is the derivation.” Outside evidence needs an argument that covers cases not individually visited. The claim that every theorem begins with M is an outside claim, but it has a short proof: the axiom begins with M, and every rule preserves the first symbol. By contrast, “MU did not appear in my first 10,000 expansions” reports an experiment. It gives no property preserved by every rule and therefore cannot cross from a finite trace to a universal conclusion.

Use this decision rule: if a positive answer can be witnessed by one finite path, search may certify yes; certify no only with a terminating decision procedure or a proved invariant that excludes the target. An invariant is a property that holds initially and is preserved by every legal move.

The puzzle invites shortcuts that look productive but change the question, so recognizing them prevents false certainty later in the course. Each mistake confuses a different boundary.

Tomorrow needs a clean artifact rather than a remembered feeling, so finish by recording a formal-search receipt: the axiom and four directional rules; one audited derivation of MUIU; the target MU; the search order and budget tried; the number of visited states; the remaining frontier; and the verdict “not found within budget.” This receipt records bounded evidence that its author kept a rule, a derivation, a theorem, a search, and a decision distinct in this worked case; it does not establish general mastery.

Checklist:

• [ ] Can you define string, axiom, rule, theorem, derivation, frontier, decision procedure, and invariant at first use?
• [ ] Can you audit every line of the MUIU derivation without using meaning?
• [ ] Can you explain why breadth-first search eventually finds any finite derivation that exists?
• [ ] Can you say why a larger unsuccessful budget is stronger evidence but still not a proof of impossibility?
• [ ] Did your receipt keep the later solution to the MU-puzzle outside today’s boundary?

Day 02 consumes this receipt. It keeps the same discipline of formal moves, replaces the MIU rulebook with the simpler pq-system, and asks when a pattern of meaningless marks earns an interpretation.

A source adaptation can quietly blur transcription with invention, and that would make the labs look more authoritative than their evidence warrants. The primary source for this reconstruction is Douglas R. Hofstadter, Gödel, Escher, Bach: An Eternal Golden Braid, Vintage Books edition, Chapter I, “The MU-puzzle,” printed pages 33–42, read from the supplied local EPUB. The rulebook and core terminology are transcribed in normalized notation; all interactive controls, diagrams, application examples, protocols, and receipts are original conceptual reconstructions. The chapter deliberately stops before the later book section that resolves the puzzle.