Technical Report: DCC-97-8

The Theorems of the Formal System MIU

Armando B. Matos

Departamento de Ci�ncia de Computadores & LIACC
Faculdade de Ci�ncias, Universidade do Porto
Rua do Campo Alegre, 823 4150 Porto, Portugal

September 1997

---

Abstract

We show that, in the MIU formal system introduced by Hofstadter every word mx where x is a sequence of u's and i's having a number of i's which is not a multiple of 3, is a theorem. We give an algorithm that outputs a standard proof of every such word.

Keywords: Formal Systems, Complexity of proofs.

---