[godel3.l]
 
[Show that a formal system of complexity N]
[can't determine more than N + 9488 + 6912]
[= N + 16400 bits of Omega.]
[Formal system is a never halting lisp expression]
[that outputs lists of the form (1 0 X 0 X X X X 1 0).]
[This stands for the fractional part of Omega,]
[and means that these 0,1 bits of Omega are known.]
[X stands for an unknown bit.]
 
[Count number of bits in an omega that are determined.]
define (number-of-bits-determined w)
    if atom w 0
    + (number-of-bits-determined cdr w)
      if = X car w
         0
         1
[Test it.]
(number-of-bits-determined '(X X X))
(number-of-bits-determined '(1 X X))
(number-of-bits-determined '(1 X 0))
(number-of-bits-determined '(1 1 0))
 
[Merge bits of data into unknown bits of an omega.]
define (supply-missing-bits w)
    if atom w nil
    cons if = X car w
            read-bit
            car w
    (supply-missing-bits cdr w)
[Test it.]
cadr try no-time-limit '
let (supply-missing-bits w)
    if atom w nil
    cons if = X car w
            read-bit
            car w
    (supply-missing-bits cdr w)
(supply-missing-bits '(0 0 X 0 0 X 0 0 X))
'(1 1 1)
cadr try no-time-limit '
let (supply-missing-bits w)
    if atom w nil
    cons if = X car w
            read-bit
            car w
    (supply-missing-bits cdr w)
(supply-missing-bits '(1 1 X 1 1 X 1 1 1))
'(0 0)
 
[Examine omegas in list w to see if in any one of them]
[the number of bits that are determined is greater than n.]
[Returns false to indicate not found, or what it found.]
define (examine w n)
    if atom w false
    if < n (number-of-bits-determined car w)
       car w
       (examine cdr w n)
[Test it.]
(examine '((1 1)(1 1 1)) 0)
(examine '((1 1)(1 1 1)) 1)
(examine '((1 1)(1 1 1)) 2)
(examine '((1 1)(1 1 1)) 3)
(examine '((1 1)(1 1 1)) 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
 
append [Append missing bits of Omega to rest of program.]
 
[Display number of bits in entire program excepting the missing bits of Omega.]
(display-number-of-bits
 
append [Append prefix and formal axiomatic system.]
 
[Display number of bits in the prefix.]
(display-number-of-bits bits '
 
[Count number of bits in an omega that are determined.]
let (number-of-bits-determined w)
    if atom w 0
    + (number-of-bits-determined cdr w)
      if = X car w
         0
         1
 
[Merge bits of data into unknown bits of an omega.]
let (supply-missing-bits w)
    if atom w nil
    cons if = X car w
            read-bit
            car w
    (supply-missing-bits cdr w)
 
[Examine omegas in list w to see if in any one of them]
[the number of bits that are determined is greater than n.]
[Return false to indicate not found, or what it found.]
let (examine w n)
    if atom w false
[]
[   if < n (number-of-bits-determined car w)  <==== Change n to 1 here so will succeed.]
[]
    if < 1 (number-of-bits-determined car w)
       car w
       (examine cdr w n)
 
                              []
[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 determines more than]
 [   (c + # of bits read + size of this prefix)]
 [bits of Omega.  Here c = 9488 is the constant in the inequality]
 [   H(Omega_n) > n - c]
 [(see omega3.l and omega3.r).]
 []
 let s (examine caddr v + 9488 debug + length fas 6912)
 if s (supply-missing-bits s) [Found it! Merge in undetermined bits, output result, 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]
 
[Toy formal system with only one theorem.]
bits 'display '(1 X 0)
 
) [end of prefix and formal axiomatic system]
 
'(1) [Missing bit of Omega that is needed.]