koen@ut-emx.UUCP (Billy Koen) (06/07/90)
Update on HELP.GOEDEL.LISP
Excuse the lengthy post. Only *yesterday*, I posted
an urgent appeal for the statement and construction of Goedel's
proof in LISP. I immediately got an avalance of E-mail asking
me to forward any responses I got because they were interested
in the problem. Please post any additional answers and comments
on the Net to save me the trouble. Thanx to all who have helped.
(Sorry for the *smart quotes* in post)
Notably, Dr. Bobrow, himself, sent this message:
"The assignment was much simpler. It was to find a Lisp function
that was its own fixed point. That is, find the function such that
(f f) --> f.
This is a step on the way to what you are looking for.
You never did turn in that assignment.
danny bobrow"
****************************************************
(Graduate students take note. Your professors have long memories
of nearly 30 years!)
****************************************************
Alex Kean writes:
" The following memo from MIT has a chapter (12, pp 137-148)
describing Godel's incompleteness theorm using S-expressions:
@techreport{levin74,
author = "Michael Levin",
title = "{Mathematical Logic for Computer Scientists}",
number = 131,
type = "Technical Report",
note = "Project MAC",
institution= "MIT",
year = 1974
}
Alex Kean <kean@cs.ubc.ca>
****************************************************
Drew McDermott writes:
Anyway, here's a handout I have used here at Yale that is *almost*
what you want. It would be a lot prettier if TeXified, but then it
wouldn`t e-mail so well.
Goedel's Theorem (copyright 1990, Drew McDermott):
This proof of Goedel's Theorem is due to Michael Levin, and appears
in Mathematical Logic for Computer Scientists, MIT Project MAC
Tech Report 131
(1974)
Actually, Levin proves Goedel's result for a different kind of
theory than Goedel used. But this turns out not to matter. The
theorem is that, if arithmetic is omega-consistent, then it is not
strongly complete, i.e., that there is a statement such that neither it nor its negation is a theorem. By "arithmetic" here we mean a rich
system that contains Peano's postulates, plus analogous postulates
for Lisp:
~atom(cons(x,y))
cons(w,x) = cons(y,z) => w=y & x=z
For any open formula P with one free variable x:
(forall x(atom(x) => P(x))
& forall (x,y) (P(x) & P(y) => P(cons(x,y))))
=> forall x P(x)
Instead of 0, we have an indefinite number of atomic constants,
including the empty list, written [], numbers and atomic symbols
written as upper-case strings (e.g., FOO). We abbreviate cons(x,cons(y,...[])) as list(x,y,...), and we abbreviate list(constant,constant,...,constant) as
[constant constant ... constant], as in [FOO [BAZ]]. The brackets keep
the constant language separate from the logical language. We will
use the standard Lisp term "S-expression" to refer to constant terms drawn from this language.
In addition, we allow recursive definitions of new functions and
predicates, provided that they "count down" to atoms in a way that guarantees halting:
forall (x,y) (atom(y) => foo(x,y) = ...)
forall (x,y1,y2) (foo(x,cons(y1,y2))
= ... foo(x,y1) ...foo(x,y2) ...)
Goedel would not have recognized this kind of thing, but if we're
going to use logic for knowledge representation we need at least this
kind of power. The advantage, of course, is that we get a
transparent sort of "Goedel numbering," in which terms of the
language stand for expressions in the language. If you've ever
programmed in Lisp, you've been using this encoding for years
(and in fact McCarthy invented the familiar Lisp notation as a kind
of Goedel numbering). We just map variables to atoms, function
calls to lists (i.e., f(a,b) becomes [F A B]), etc. To avoid ambiguity,
constants, written in uppercase in the actual first-order language,
are now wrapped with QUOTE. So foo(x,X) is coded by the term [FOO X [QUOTE X]].
Now we can define the function subquote(x,y,z), which produces an
S-expression that is a copy of z except that it contains [QUOTE x]
in place of every occurrence of y in unquoted subexpressions of z.
forall (x,y,z) (atom(z) => (subquote(x,y,y) = list(QUOTE,x))
& (~y=z => subquote(x,y,z) = z))
forall (x,y,z1,z2)
(~z1=QUOTE => subquote(x,y,cons(z1,z2))
= cons(subquote(x,y,z1),
subquote(x,y,z2)))
forall (x,y,z)
(subquote(x,y,cons(QUOTE,z)) = cons(QUOTE,z))
For example, we can prove that
subquote(A,B,[FOO B [QUOTE B]]) = [FOO [QUOTE A] [QUOTE B]].
Although it's more work, we can define aproof(p,f), such that
it is provable that aproof(p,f) if p is the S-expression encoding
a proof of the formula encoded by f; and ~aproof(p,f) is
provable if p is an S-expression that isn't such a proof. And we can
of course define append(l1,l2), which is the concatenation of two lists.
Now let $1 be a list encoding the definitions of subquote,
aproof, and append. (It will include the S-expression encoding
of the definition of subquote just given, including something like
[FORALL [X Y Z] [IF [ATOM Z] [AND [= [SUBQUOTE ...]]]]].)
Let alpha be the formula
~exists x (aproof(append($1,x),subquote(y,Y,y)))
Note that Y occurs as a constant, whereas y is a variable. And $1
is a big S-expression that should actually be plugged in, except
that we are too lazy; if we did plug it in, alpha would actually
be a couple of pages long, and contain a constant S-expression
laying out the definitions of subquote, aproof, and append. The
term append($1,x) then denotes a proof consisting of all that stuff
followed by further proof lines x. Hence alpha states that, given
an S-expression y, there is no proof of that form of the formula you
get by substituting [QUOTE y] for Y in y.
Let alpha* be the S-expression encoding alpha, to wit,
[NOT [EXISTS X [APROOF [APPEND [QUOTE $1] X]
[SUBQUOTE Y [QUOTE Y] Y]]]]
Let beta be the statement obtained from alpha by substituting
alpha* for the free variable y:
~exists x (aproof (append($1,x), subquote(alpha*,Y,alpha*)))
and let beta* be its S-expression encoding:
[NOT [EXISTS X [APROOF [APPEND [QUOTE $1] X]
[SUBQUOTE [QUOTE alpha*]
[QUOTE Y]
[QUOTE alpha*]]]]]
Now self-referentiality begins to appear. The subquote term in
beta can be proven equal to beta*
|- subquote(alpha*,Y,alpha*) = beta*
But we can make this substitution in beta itself, so we can prove
|- beta <=> ~exists x (aproof(append($1,x),beta*))
If beta is provable, then there is a constant S-expression encoding
its proof; call it the-proof. It must be the case that
aproof(append($1,the-proof),beta*) is provable as well,
and hence we have proven there exists a proof of beta*, and hence
~beta is provable.
But if ~beta is provable, then (exists x (aproof(append($1,x),beta*)))
would be provable. If arithmetic is omega-consistent, there must be
some actual S-expression $2 such that it is not provable that
~aproof(append($1,$2),beta*)
But aproof and append are functions that "always halt," or rather,
in this context, have the property that, for constant S-expression
arguments, either aproof(.,.) is provable or its negation is. Hence
aproof(append($1,$2),beta*) must be provable. Hence beta must be
provable.
In either case the system is inconsistent. Therefore neither beta
nor ~beta is provable.
Does it matter that we have used Lisp instead of arithmetic?
Presumably not. For one thing, the standard model of Lisp is as intuitively graspable as the standard model of Peano arithmetic.
(Only it consists of all finitely constructable S-expressions.) It seems incredible that there are true facts about this simple domain that
cannot be proven within Lisp. Note that the fact beta is indeed true,
since there is no S-expression that encodes a proof of it.
In addition, the key idea in this proof is that you can simulate
substitution for variables within the terms of the language. So you
would expect any sufficiently rich theory to suffer from this
problem, and Goedel showed that Peano arithmetic was sufficiently
rich, even if we dispense with S-expressions and use ordinary
numbers instead.
****Special thanx to Drew McDermott. I worked at Project Mac and
am sure that I have seen this note. I vaguely remember the
finasse about ****transparent sort of "Goedel numbering," etc.****
and finally, Walter Daugherity suggested,
"Douglas Hofstadter wrote a series of three articles fro Scientific
American on LISP which as I recall also included an outline of the
47-level hierarchy to prove Goedel's Theorem."
I have located those articles in the Feb, March, and April, 1983
issues but find no mention of Goedel's proof. Perhaps other writing
of Hofstadter will turn it up.
Thank you, Billy Koen
koen@emx.utexas.edu