[godel2.l]
[Show that a formal system of complexity N]
[can't prove that a specific object has]
[complexity > N + 4696.]
[Formal system is a never halting lisp expression]
[that output pairs (lisp object, lower bound]
[on its complexity). E.g., (x 4) means]
[that x has complexity H(x) greater than or equal to 4.]
[Examine pairs to see if 2nd element is greater than lower bound.]
[Returns false to indicate not found, or pair if found.]
define (examine pairs lower-bound)
if atom pairs false
if < lower-bound cadr car pairs
car pairs
(examine cdr pairs lower-bound)
(examine '((x 2)(y 3)) 0)
(examine '((x 2)(y 3)) 1)
(examine '((x 2)(y 3)) 2)
(examine '((x 2)(y 3)) 3)
(examine '((x 2)(y 3)) 4)
[This is an identity function with the size-effect of]
[displaying the number of bits in a binary string.]
define (display-number-of-bits string)
cadr cons display length string cons string nil
[This is the universal Turing machine U followed by its program.]
cadr try no-time-limit 'eval read-exp
[Display number of bits in entire program.]
(display-number-of-bits
append [Append prefix and data.]
[Display number of bits in the prefix.]
(display-number-of-bits bits '
[Examine pairs to see if 2nd element is greater than lower bound.]
[Returns false to indicate not found, or pair if found.]
let (examine pairs lower-bound)
if atom pairs false
if < lower-bound cadr car pairs
car pairs
(examine cdr pairs lower-bound)
[]
[Main Loop - t is time limit, fas is bits of formal axiomatic system read so far.]
let (loop t fas) [Run formal axiomatic system again.]
let v debug try debug t 'eval read-exp debug fas
[Look for theorem which is pair with 2nd element > # of bits read + size of this prefix.]
let s (examine caddr v debug + length fas 4696)
if s car s [Found it! Output first element of theorem and halt. Contradiction!]
if = car v success failure [Surprise, formal system halts, so we do too.]
if = cadr v out-of-data (loop t append fas cons read-bit nil)
[Read another bit of the formal axiomatic system.]
if = cadr v out-of-time (loop + t 1 fas)
[Increase time limit]
unexpected-condition [This should never happen.]
[]
(loop 0 nil) [Initially, 0 time limit and no bits of formal axiomatic system read.]
) [end of prefix, start of formal axiomatic system]
bits ' display'(x 4881)
) [end of entire program for universal Turing machine U]