###
Technical Report: DCC-97-9

On the number of lines of theorems in 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

The MIU formal system, introduced by Hofstadter
is a relatively simple example of a formal axiomatic system
where the length of proofs can be studied in some detail.
Denote by l(t) and L(t) respectively the largest and smallest
number of lines of a minimum proof of a theorem with t symbols.
We show that l(t) is \Omega(\log t) and that L(t)
is \Omega(t/\log t) and O(t).

**Keywords:** Formal Systems, Complexity of proofs.