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.