The Well-known MU Puzzle

Logic Level 3

In Douglas Hofstadter's book, Godel, Escher, Bach, he proposes the following puzzle about formal systems.

Axiom: MI is an axiom.

Theorem: The axiom is a theorem by default. All the (and only all the) strings that can be derived using the following transformations on a theorem is also a theorem.

Formal Rule	Informal Description	Example
x`I` → x`IU`	Changing any terminal `I` to `IU`	`MII` → `MIIU`
`M`x → `M`xx	Double the string after `M`	`MIU` → `MIUIU`
x`III`y → x`U`y	Replace three `I`s with an `U`	`MIIIU` → `MUU`
x`UU`y → xy	Remove an occurence of double `U`s	`MUUI` → `MI`

Problem: Is MU a theorem?

Guessing the answer to this problem is not very difficult. However, an interested problem solver could explore this questions:

If your answer was yes, what is the proof of the MU theorem, i.e, what is the sequence of transformation rules that will take you from MI to MU?
Is the MIU system decidable, i.e, is there a computer program to decide if a given string is a theorem?
If not, is the system semidecidable, i.e, is there a computer program that will eventually tell if a string is a theorem, but never tell if it isn't?

Excel in math and science

Master concepts by solving fun, challenging problems.

It's hard to learn from lectures and videos

Learn more effectively through short, interactive explorations.

Used and loved by over 7 million people

Learn from a vibrant community of students and enthusiasts, including olympiad champions, researchers, and professionals.