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?