[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]