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
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.