How can we enable a LISP expression to know itself? Well, it's very easy once you've seen the trick! Consider the LISP function f(x) that takes x into (('x)('x)). In other words, f assumes that its argument x is the lambda expression for a one-argument function, and it forms the expression that applies x to x. It doesn't evaluate it, it just creates it. It doesn't actually apply x to x, it just creates the expression that will do it.
You'll note that if we were to evaluate this expression (('x)('x)), in it x is simultaneously program and data, active and passive.
Okay, so let's pick a particular x, use f to make x into (('x)('x)), and then run/evaluate the result! And to which x shall we apply f? Why, to f itself!
So f applied to f yields what? It yields f applied to f, which is what we started with!! So f applied to f is a self-reproducing LISP expression!
You can think of the first f, the one that's used as a function, as the organism, and the second f, the one that's copied twice, that's the genome. In other words, the first f is an organism, and the second f is its DNA! I think that that's the best way to remember this, by thinking it's biology. Just as in biology, where a organism cannot copy itself directly but needs to contain a description of itself, the self-reproducing function f cannot copy itself directly (because it cannot read itself—and neither can you). So f needs to be given a (passive) copy of itself. The biological metaphor is quite accurate!
So in the next section I'll show you a LISP run where this actually works. There's just one complication, which is that what can reproduce itself, in LISP just as in real life, depends on the environment in which the organism finds itself.
(f f) works in an environment that has a definition for f, but that's cheating! What I want is a stand-alone LISP expression that reproduces itself. But f produces a stand-alone version of itself, and that is the actual self-reproducing expression. (f f) is like a virus that works only in the right environment (namely in the cell that it infects), because it's too simple to work on its own.
So, finally, here is the LISP run illustrating all this. I hope you like it, and that it convinces you that it was worth the effort to learn LISP! After you understand this LISP run, I'll show you Gödel's proof.
LISP Interpreter Run
[[[[[
A LISP expression that evaluates to itself!
Let f(x): x -> (('x)('x))
Then (('f)('f)) is a fixed point.
]]]]]
[Here is the fixed point done by hand:]
(
'lambda(x) cons cons "' cons x nil
cons cons "' cons x nil
nil
'lambda(x) cons cons "' cons x nil
cons cons "' cons x nil
nil
)
expression ((' (lambda (x) (cons (cons ' (cons x nil)) (cons
(cons ' (cons x nil)) nil)))) (' (lambda (x) (cons
(cons ' (cons x nil)) (cons (cons ' (cons x nil))
nil)))))
value ((' (lambda (x) (cons (cons ' (cons x nil)) (cons
(cons ' (cons x nil)) nil)))) (' (lambda (x) (cons
(cons ' (cons x nil)) (cons (cons ' (cons x nil))
nil)))))
[Now let's construct the fixed point.]
define (f x) let y [be] cons "' cons x nil [ y is ('x) ]
[return] cons y cons y nil [ return (('x)('x)) ]
define f
value (lambda (x) ((' (lambda (y) (cons y (cons y nil)))
) (cons ' (cons x nil))))
[Here we try f:]
(f x)
expression (f x)
value ((' x) (' x))
[Here we use f to calculate the fixed point:]
(f f)
expression (f f)
value ((' (lambda (x) ((' (lambda (y) (cons y (cons y ni
l)))) (cons ' (cons x nil))))) (' (lambda (x) (('
(lambda (y) (cons y (cons y nil)))) (cons ' (cons
x nil))))))
[Here we find the value of the fixed point:]
eval (f f)
expression (eval (f f))
value ((' (lambda (x) ((' (lambda (y) (cons y (cons y ni
l)))) (cons ' (cons x nil))))) (' (lambda (x) (('
(lambda (y) (cons y (cons y nil)))) (cons ' (cons
x nil))))))
[Here we check that it's a fixed point:]
= (f f) eval (f f)
expression (= (f f) (eval (f f)))
value true
[Just for emphasis:]
= (f f) eval eval eval eval eval eval (f f)
expression (= (f f) (eval (eval (eval (eval (eval (eval (f f)
)))))))
value true
End of LISP Run
Elapsed time is 0 seconds.
Turing's proof and mine do not depend on the inner structure of the formal axiomatic system being studied, but Gödel's proof does. He needs to get his hands dirty, he needs to lift the hood of the car and poke around in the engine! In fact, what he needs to do is to confuse levels and combine the theory and its metatheory. That's how he can construct a statement in the theory that says that it's unprovable.
In Gödel's original proof, he was working in Peano arithmetic, which is just a formal axiomatic system for elementary number theory. It's the theory for the natural numbers and plus, times, and equal. So Gödel used Gödel numbering to arithmetize metamathematics, to construct a numerical predicate Dem(p,t) that is true iff p is the number of a proof and t is the number of the theorem that p proves.
Gödel did it, but it was hard work, very hard work! So instead, I'm going to use LISP. We'll need a way to express metamathematical assertions using S-expressions. We'll need to use S-expressions to express proofs and theorems. We need to construct a LISP function (valid-proof? x) that returns the empty list nil if x is not a valid proof, and that returns the S-expression for the theorem that was demonstrated if x is a valid proof. I won't actually define/program out the LISP function valid-proof?. I don't want to get involved ``in the internal affairs'' of a particular formal axiomatic system. But you can see that it's not difficult. Why not?
Well, that's because Gödel numbers are a difficult way to express proofs, but S-expressions are a very natural way to do it. An S-expression is just a symbolic expression with explicit syntax, with its structure completely indicated by the parentheses. And it's easy to write proof-checking algorithms using LISP functions. LISP is a natural language in which to express such algorithms.
So let's suppose that we have a definition for a LISP function (valid-proof? x). And let's assume that the formal axiomatic system that we're studying is one in which you can talk about S-expressions and the value of an S-expression. Then how can we construct a LISP expression that asserts that it's unprovable?
First of all, how can we state that an S-expression y is unprovable? Well, it's just the statement that for all S-expressions x, it is not the case that (valid-proof? x) is equal to y. So that's easy to do. So let's call the predicate that affirms this is-unprovable. Then what we need is this: a LISP expression of the form (is-unprovable (value-of XXX)), and when you evaluate the LISP expression XXX, it gives back this entire expression. (value-of might more accurately be called lisp-value-of, just to make the point that we are assuming that we can talk about LISP expressions and their values in our formal axiomatic system.)
So we're almost there, because in order to do this we just need to use the fixed-point trick from before in a slightly more complicated manner. Here's how:
LISP Interpreter Run
[[[[[
A LISP expression that asserts that it itself is unprovable!
Let g(x): x -> (is-unprovable (value-of (('x)('x))))
Then (is-unprovable (value-of (('g)('g))))
asserts that it itself is not a theorem!
]]]]]
define (g x)
let (L x y) cons x cons y nil [Makes x and y into list.]
(L is-unprovable (L value-of (L (L "' x) (L "' x))))
define g
value (lambda (x) ((' (lambda (L) (L is-unprovable (L va
lue-of (L (L ' x) (L ' x)))))) (' (lambda (x y) (c
ons x (cons y nil))))))
[Here we try g:]
(g x)
expression (g x)
value (is-unprovable (value-of ((' x) (' x))))
[
Here we calculate the LISP expression
that asserts its own unprovability:
]
(g g)
expression (g g)
value (is-unprovable (value-of ((' (lambda (x) ((' (lamb
da (L) (L is-unprovable (L value-of (L (L ' x) (L
' x)))))) (' (lambda (x y) (cons x (cons y nil))))
))) (' (lambda (x) ((' (lambda (L) (L is-unprovabl
e (L value-of (L (L ' x) (L ' x)))))) (' (lambda (
x y) (cons x (cons y nil))))))))))
[Here we extract the part that it uses to name itself:]
cadr cadr (g g)
expression (car (cdr (car (cdr (g g)))))
value ((' (lambda (x) ((' (lambda (L) (L is-unprovable (
L value-of (L (L ' x) (L ' x)))))) (' (lambda (x y
) (cons x (cons y nil))))))) (' (lambda (x) ((' (l
ambda (L) (L is-unprovable (L value-of (L (L ' x)
(L ' x)))))) (' (lambda (x y) (cons x (cons y nil)
)))))))
[Here we evaluate the name to get back the entire expression:]
eval cadr cadr (g g)
expression (eval (car (cdr (car (cdr (g g))))))
value (is-unprovable (value-of ((' (lambda (x) ((' (lamb
da (L) (L is-unprovable (L value-of (L (L ' x) (L
' x)))))) (' (lambda (x y) (cons x (cons y nil))))
))) (' (lambda (x) ((' (lambda (L) (L is-unprovabl
e (L value-of (L (L ' x) (L ' x)))))) (' (lambda (
x y) (cons x (cons y nil))))))))))
[Here we check that it worked:]
= (g g) eval cadr cadr (g g)
expression (= (g g) (eval (car (cdr (car (cdr (g g)))))))
value true
End of LISP Run
Elapsed time is 0 seconds.