LISP program-size complexity II

We present the information-theoretic incompleteness theorems that arise in a theory of program-size complexity based on something close to real lisp. The complexity of a formal axiomatic system is defined to be the minimum size in characters of a lisp definition of the proof-checking function associated with the formal system. Using this concrete and easy-to-understand definition, we show (a) that it is difficult to exhibit complex S-expressions, and (b) that it is difficult to determine the bits of the lisp halting probability ωlisp. We also construct improved versions ω″lisp and ω″lisp of the lisp halting probability that asymptotically have maximum possible lisp complexity. © 1992.