From: Lee Corbin (lcorbin@tsoft.com)
Date: Mon Sep 02 2002 - 16:03:23 MDT
Hal writes
> Lee Corbin writes [about Giu1i0 Pri5c0's remarks, not Rudy Rucker's]
>
> > No, I think that this exaggerates what Godel's proof implies. We, because
> > of our realism, or our belief in the existence of numbers, or by going to
> > a higher formal system than the system in which some axioms are written,
> > can see that certain things are true even though those things *cannot*
> > be proven from those axioms (i.e., in the original formal system).
> >
> > Perhaps soon, (2040?), there will be a formal system based on a finite
> > number of axioms, which will nonetheless proceed to make conjectures,
> > and study our universe and us, and be altogether vastly wiser than
> > we are. It too will understand Godel's theorem, and it will have a
> > proof, as do we, of the theorem using metamathematics (like we do) to
> > prove its results. So a formal system can be just as powerful as we are.
>
> I am confused about how a formal system can do all of these things.
> A formal system is passive; it is a set of rules which ultimately allow
> you to determine whether a given proof of a theorem is valid. Lee's
> description sounds like an AI program.
Thanks very much for critically examining my claims. While I
think I'm right, one can never tell for sure whether one is
BS'ing even oneself in sufficiently difficult territory. I'll
start by laying out my thoughts and then respond to your points.
Indeed, I attribute the same capabilities to the formal axiom
system that I do to a program. Here it's a little hand-wavy:
the Church-Turing thesis (my paraphrase that I believe to be
equivalent, check the web) is that anything effectively
computable in any way whatsoever can be computed by a Turing
machine. It also happens that any function calculable by a TM
is also a type of function called (general) recursive, and
vice-versa.
The crucial element: every such recursive function is
*representable* in a sufficiently powerful formal system
incorporating arithmetic. "Recursive" means, in Hofstadter's
memorable phrase "every true instance is a theorem, and every
false instance is a non-theorem". For example, there is this
little axiom system called Q which has just seven axioms
(basically the Peano postulates, plus what "*" means as
multiplication). This is an incredibly weak system (it
can't even prove that x+y = y+x) but it happens to be
adequate for a huge range of arithmetical truths, and
seeing how all this works. I saw using Q how it comes
to pass that every recursive function is representable
and vice-versa. This ties in theorem-hood and all true
*instances*.
The clincher: Anything your computer can do is equivalent to
what a TM can do (even the infinite loops of your word-processor
and other non-halting programs, hopefully e.g. those of us
signed up for cryonics). And what results a TM can get to
are equivalent to recursive functions. Then, since recursive
functions are representable, all true instances are theorems.
That is, 36+21=57 is a theorem and is Fermat's Four Squares
Theorem, (although it has a lot of "for all's and "there exists"
in it). Therefore, it seems, any result that your computer can
get to is a theorem of some axiom system that can do recursive
functions.
The caveats: I don't yet *thoroughly* understand all those
steps anywhere near as well as I want to, and so my gratitude
again for forcing this out into the open.
The best book is "Computability and Logic", by Boolos and
Jeffrey. In fact, it was personally recommended to me by
Hofstadter himself, when he responded in 1986 to my complaint
that I had failed to find how to express "b is a power of 10"
(and so did everyone I knew). Since then, I have personally
validated that it is the best book. It's also used in many
top universities, not that the poor undergraduates (even the
ones who get A's) can often articulate three weeks later the
wringer that their mind's been through.
> What exactly is the relationship between a program, whether AI or
> something else, and a mathematical formal system? Is there a one-to-
> one correspondence between formal systems and computer programs?
That's what I gather.
> I can imagine how to write a computer program to implement a given
> formal system. Armed with the axioms and rules of inference, and given a
> proposed proof, it can go through each step of the proof and mechanically
> check whether that step follows from all of the previous steps, using
> the various axioms and inference rules. At the end it can produce output
> indicating whether the proof, and hence the proposed theorem, is valid or
> invalid. This is a mechanical, finite process and no doubt many programs
> have been written over the years to implement such proof checkers.
> This shows that there is a mapping from formal systems to programs.
Yes. Moreover, it can grind out all theorems (any one eventually)
by systematically using the axioms and the rules of inference.
> However, such programs would seemingly be only a subset of all possible
> programs. Most programs do not work by reading in axioms and then
> checking a proposed theorem. This word processor which is allowing me
> to type my message doesn't seem to fit into that structure at all.
>
> The question is then whether there is a mapping in the other direction,
> from programs to formal systems. Is it the case that for any program, we
> can define a formal system which is somehow isomorphic to the program?
> How would that work; would each step of the program be like adding
> another line to a proof in the formal system? The axioms would somehow
> be derived from the program source code, and the description of the
> hardware architecture?
My guess: consider each action of the program as "output",
and consider this to be a computable function; as such, it's
also a recursive function. It's also then a representable
function. So (I take it) there has to exist a set of axioms
(probably a very standard set unless your computer is claiming
to see and understand some problematical string like the G
string in Godel's theorem which makes a startling remark about
itself, and insinuates things about its own axioms and what
can be got from them). I further guess that the mathematical
logicians clearly *see* that all this is true, whereas it's
still pretty vague to me.
> If this is possible, so that in particular an AI program would
> correspond to a formal system, and that AI program began making
> mathematical conjectures and proofs just like we do, it doesn't seem
> like the program would be basing its proofs on its own formal system.
All of our usual proofs can be reduced to complete formalism.
They've done remarkable reductions already, as someone pointed
out in a related thread right here last year. The Fundamental
Theorem of Algebra has now been completely reduced (grep for
FTA). Godel's proof is an exception; you can't get to it with
ordinary axioms. (It's true but unprovable by the usual axioms.)
While, as you say, such an AI program *would not* be basing
its *formal* proofs on its own formal system, it would be
basing them (I believe) on the standard axioms, much like
mathematicians would do if forced to. That is, every
mathematician believes that his results *could* be done
formally by the usual axioms, unless he or she is messing
around with weird stuff like G.
So I claim that the busy AI can get to all the proofs that
we can, and it can also argue convincingly for things like
Godel's Theorem (like we do). Moreover, all the usual
results it gets (like interactive programs and so on) are
also obtainable from the usual axioms, but unlike FTA, are
**extremely** difficult to formalize. (The FTA was only
*extremely* difficult to formalize.)
> If there is a formal system defining this program, it would presumably
> be enormously complex, at least as complex as the program itself, which
> for human-level AI would probably be billions of bytes long at least.
As I say (sorry for the repetition) I think that the formal
system would be the familiar one, and that the particular
behavior of the program would reflect just a certain subset
of all the choices of all the inferences that could be made.
Know anything about ProLog? I don't, but I've gathered that
it is manifestly equivalent to a set of axioms.
Now, what do we do with the program who announces twenty
minutes after we turn it on, "Say, I've just found an interesting
'theorem' that can't possibly be a theorem. It's true but
not provable." Besides telling it about Godel, do we infer
that it's based on non-usual axioms? I don't think so. If
we command, "Okay, now formalize your proof, at whatever the
time and cost", then does the machine concoct a new axiom
embedded in meta-mathematics, or just formalize meta-mathematics?
I suppose so.
> It's one thing to look at a single page of axioms and see that it is
> "obviously" consistent. But how can you do so when looking at a
> million pages of axioms? That is far beyond the abilities of a human
> mathematician, or those of a near-human-level AI.
It's not obvious, looking at even a few axioms. No one actually
knows if the Zermelo-Frankel axioms are consistent, for example.
It's admitted that we are proceeding on blind faith that they are
indeed consistent, and also the fact that in 80 years no one has
found a problem. (Some say that this is only because people
aren't *trying* to find a problem.) And, as you know, there
can't be a proof of their consistency.
> And furthermore, what does it mean for the formal system specifying a
> piece of software to be consistent or inconsistent? Here I come back
> to the question of what exactly it means to say that a program "is" a
> formal system. With mathematical formal systems, consistency is easy to
> define: T and ~T cannot both be theorems, where ~ means "not". This is
> purely a syntactic definition. There can be no strings of characters,
> both of which are accepted as valid proofs by the formal system, and for
> which the last lines are identical except that one has the ~ in front
> of it.
>
> How would you apply this to a program? What does it mean for it to
> be consistent or inconsistent? Somehow the theorems or proofs of the
> formal system must be identified with the program state; and then what
> does the "not" symbol "~" mean?
Fantastically good question. My guess: First, suppose that the
program did what the mathematicians haven't been able to do, and
found an embarrassment in the usual axioms. Well, that's one
thing, and we all can drop math and descend to philosophy (and
if that fails, we follow Bertrand Russell right down to politics).
Now instead, let's suppose that the program obtained a contradiction
while trying to prove things formally, and one of its new-fangled
axioms was involved. So much for that axiom. But now the hard
case, that you're perhaps really asking about: what if the program's
execution happens to be equivalent to an inconsistent axiom system?
IF I'm right in my above claims, then this reduces to one of the
easier cases: after all, the usual axioms capture its behavior,
and the only way we'd know is if one day the AI says "I have bad
news for you. I can formally prove T and ~T. Worse, this may
explain a slight inconsistency in my views that the Democrats
have been talking about."
> Summing up, it seems to me that Godel's theorem does not apply in quite
> the same way to an AI program as it does to the Peano axioms that describe
> the integers. The whole question of consistency vs. completeness has
> to be judged on very different terms when dealing with such a complex
> system, and it's not clear what inconsistency even means in this case.
>
> I think there is a tendency to confuse the formal system which describes
> the AI with the one that the AI is using to make its mathematical proofs,
> as though an inconsistent AI is one that starts with the Peano axioms
> and manages to prove that 1=2.
As I say, I think they're really the same thing, in all the
normal cases. Just one *formal* system, really. The rest
of the apparently human behavior of the AI, its hunches,
conjectures, flawed proofs (it says "Doh!" from time to
time, like we do), comes from the usual axioms, but at a
low level beneath the consciousness of the program by a
perhaps somewhat arbitrary choice of which one to invoke
next in the sequence of groping for results (for thinking).
You're right: there are two levels here, but I recall
Hofstadter's large picture of 2+2=5 made up of little
tiny 2+2=4's, an image that helps me right here.
Lee
This archive was generated by hypermail 2.1.5 : Sat Nov 02 2002 - 09:16:38 MST