[godel.l]
 
[Show that a formal system of lisp complexity H_lisp (FAS) = N]
[cannot enable us to exhibit an elegant S-expression of]
[size greater than N + 419.]
[An elegant lisp expression is one with the property that no]
[smaller S-expression has the same value.]
[Setting: formal axiomatic system is never-ending lisp expression]
[that displays elegant S-expressions.]
 
[Idea is to have a program P search for something X that can be proved]
[to be more complex than P is, and therefore P can never find X.]
[I.e., idea is to show that if this program halts we get a contradiction,]
[and therefore the program doesn't halt.]
 
define (size-it-and-run-it exp)
    cadr cons display size display exp
         cons eval exp
              nil
 
(size-it-and-run-it'
+ 5 15
)
 
(size-it-and-run-it'
 
[Examine list x for element that is more than n characters in size.]
[If not found returns false.]
let (examine x n)
    if atom x  false
[]
[   if < n size car x  car x     <=== Change This So Something Interesting Will Happen!]
[]
    if < 1 size car x  car x
    (examine cdr x n)
 
[Here we are given the formal axiomatic system FAS.]
let fas 'display elegant-expression   [Insert FAS here preceeded by "'".]
 
[N = the number of characters in this program including the FAS.]
let n display + 419 size display fas  [N = 419 + |FAS|.]
 
[Loop running the formal axiomatic system.]
let (loop t)                          []
  let v display try display t fas nil [Run the formal system for T time steps.]
  let s (examine caddr v n)           [Did it output an elegant s-exp larger than this program?]
  if s eval s                         [If found elegant s-exp bigger than this program,]
                                      [run it so that its output is our output. Contradiction!]
  if = failure car v (loop + t 1)     [If not, keep looping,]
  failure                             [or halt if formal system halted.]
                                      []
(loop 0)                              [Start loop running with T = 0.]
                                      []
) [end size-it-and-run-it]