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 |
xI → xIU | Changing any terminal I to IU | MII → MIIU |
M x → M xx | Double the string after M | MIU → MIUIU |
xIII y → xU y | Replace three I s with an U | MIIIU → MUU |
xUU 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:
MU
theorem, i.e, what is the sequence of transformation rules that will take you from MI
to MU
?MIU
system decidable, i.e, is there a computer program to decide if a given string is a theorem?