From: Lee Corbin (lcorbin@rawbw.com)
Date: Mon Jun 30 2008 - 23:16:02 MDT
John Clark wrote
> The trouble with first order logic isn't that it can't prove EVERYTHING,
> the problem is that it can do almost NOTHING. It is a toy logical system
> weak as tea invented long ago by professional logicians because at the
> time a grown up logical system was too complicated to think about.
You exaggerate somewhat: quite a few parts of mathematics
can be handled (or axiomatized) nicely by first order logic,
but I certain agree with the rest of your statements:
> But yes it's true, Gödel himself proved in his PHD that it's consistent and
> complete, that is to say any true statement that can be expressed within
> it can be derived from its axioms and rules of inference and no false
> statements can be. When Gödel discovered his completeness proof it
> caused little splash because for years most assumed it was probably true
> and most didn't care a lot about first order logic one way or the other
> because it's so weak it can't even do arithmetic.
Actually, people cared very much about first order logic; too
much, in fact, from our perspective. There are a couple of reasons:
one, there had been so many rude shocks in the late 19th and
early 20th century, that many people were just suspicious of
any ideas that couldn't be extremely firmly grounded. This also
lead to positivism and a lot of other nonsense. Second, obsession
with first order logic was in effect endorse by Bourbaki, and got
quite a further impetus after the second world war.
> About a year later Gödel came out with his incompleteness proof that
> showed any logical system with a finite number of symbols that was
> powerful enough to do arithmetic can't be consistent and complete.
> Nobody was expecting that and it did make a splash.
Right. It took a while, though. For several years, many outstanding
mathematicians, including Hilbert, just didn't get the hang of what
Gödel was saying. Some very famous ones, like Zermelo, went
to their graves still dismissing out of hand Gödel's results. And at
the height of his fame, Wittgenstein also dissed the Gödel theorems
as irrelevant.
> So regarding mind your objections would be correct if Mr. Jupiter Brain
> worked according to first order logic, but Babbage couldn't even make
> his Analytical Engine if he used that.
I think Stuart is saying something of the same kind of thing I am,
but highly capable intelligences won't "work" by any formal
logic. It's too slow and in most cases completely pointless.
Bourbaki, for example, admitted in one of their books that
without using abbreviations, it would take on the order of ten
thousand symbols to express (in their formal system) the
cardinal number 1. In 2002 some guy proved they were
pretty far off. He proved that it would take on the order of
10^12 symbols in their system to express the cardinal number one!
> You also say that Gentzen came up with a system that could
> do arithmetic that was consistent and complete, and that's true,
I think that that's irrelevant. You don't need "systems" to do
mathematics, or even arithmetic. Very low IQ children can
often do arithmetic just fine (if they do all their homework,
that is, and expend quite a bit of diligence). They don't
axiomize their thinking. We don't axiomize our thinking.
It seems bizarre to me that any intelligent system would.
Most of the confusion over this came from misguided attempts
to try to use Gödel's results to give human beings some assurance
that they could do something that machines can't---which, as
everyone on this list knows, is patent nonsense. Lucas and
Penrose are just two of many dozens of prominent people
who've tried. Again, I recommend Torkel Franzen's superb
book.
> but Gentzen's system needs an infinite number of symbols;
> so unless you're postulating an infinite and not just
> astronomically large mind Gentzen is irrelevant. For any
> mind you actually expect to build Gödel's Incompleteness
> theorem is very relevant indeed.
As I said, I agreed heartily with the bulk of your post. But
here you seem to go off the rails, in several ways. So what
if you *potentially* require infinitely many symbols? That
objection is parallel to someone objecting that Turing
Machines require infinitely long tapes. One would, for example,
never make the mistake of considering numbers on the order
of 10^1000 being useless because they require 1000 or so
symbols---so if transfinite arithmetic has uses (and some theorems
indeed are best proved using transfinite numbers), it by no means
implies that an infinity of integers (or symbols) need be actually
used.
But more importantly, you seem here to revert to the idea that
some mind we actually build will be tied to first order logic
somehow. Else why do you say "For any mind you actually
expect to build Gödel's Incompleteness theorem is very
relevant indeed."
Okay so Stuart said
>> Please give a specific example of something
>> a goal orientated AI would fail at, because
>> of Godel-type considerations.
and you reply
> There are an INFINITE number of such problems, but Turing proved there
> is no way in general to determine if any specific problem is of that
> nature or not, and that can cause trouble. One possible example of an
> impossible goal is "Prove the Goldbach conjecture to be true or find a
> counter example to show it is false". And if Goldbach is not one of
> those true but un-provable statements you can be certain there are an
> infinite number of similar statements that are.
Well, hell, we know of many proofs that *must* exist, but which
we cannot get our hands on---or to use your language of "goals",
sure there are many even *possible* goals that supremely intelligent
minds far beyond ours will still fail on. Yes, you're right: Of course
there will be infinitely many Gödel-type sentences that have no
formal proofs in a particular system, but what difference does
it really make if even something as simple as Goldbach's conjecture
is among them? AIs can be plenty smart without getting hung up
on hard problems.
Lee
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:01:03 MDT