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.