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?

×

Problem Loading...

Note Loading...

Set Loading...