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