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.

---