In Douglas Hofstadter's book, Godel, Escher, Bach, he proposes the following puzzle about formal systems.
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||Changing any terminal |
|Double the string after |
|x||Replace three |
|x||Remove an occurence of double |
MU a theorem?
Guessing the answer to this problem is not very difficult. However, an interested problem solver could explore this questions:
MUtheorem, i.e, what is the sequence of transformation rules that will take you from
MIUsystem decidable, i.e, is there a computer program to decide if a given string is a theorem?