This is a sub-puzzle of the MIU-system, as described by Douglas Hofstadter in his book Gödel, Escher, Bach. (One can also find a description of this system here.)
My question is: is
MUUI a MIU-string (assuming, as usual, that the sole axiom is the string
If yes, I'd like to see a derivation, starting from
MI. If no, I'd like to see a proof.
NB: As a reminder, the MIU-system rules may not be "run backwards". In particular, even though rule IV allows one to drop
UU from any MIU-string, it does not allow one to add
UU to any MIU string. In other words, rule IV may not be invoked to obtain
MUUI from the axiom string
The following is excerpted from p. 260 of the latest American edition of GEB:
I. If x
Iis a theorem, so is x
Mx is a theorem, so is
III. In any theorem,
IIIcan be replaced by
UUcan be dropped from any theorem.
In the rules,
- the word "theorem" is synonym for what I call "MIU-string" earlier in the post;
- the variable x stands for any MIU-substring.
See here for examples, and for additional details.