Re: Article in Scientific American


I'm not sure that we're even talking about the same
thing any more. My
argument was that the simple fact that some computer
program printed
some output should not be seen as a proof. I
actually have no problem
with proofs produced by computers (so long as they
are actual proofs),
nor with computers verifying the validity of an
existing proof, whether
or not it was itself produced by a computer. As I
said earlier in the
thread, the test ought to be whether the result of
the whole exercise is
something that could be read as a complete argument
without the
computer's involvement.

That is, suppose the computer were shown to be
entirely unreliable
tomorrow. If you have an actual proof that was
produced and/or verified
by that computer, then you perhaps examine it more
closely to find
flaws; and if you don't find any, you can feel lucky.
If you have to
reject portions of the proof out of hand, then you
never had a proof to
begin with.

It is the potential for the computer to
become a theorem producer that forces me to think
in terms
of not not provable. Why? Because heretofore we
have
known no way to differentiate "provable" from "not
not
provable." They are logically equivalent -- to us.

They are logically equivalent, period, at least in
any first-order
system. I honestly don't know what you're getting
at. The distinction
I brought up was between "not provable" and
"disprovable". There is no
distinction between "provable" and "not not
provable".

--
Chris Smith

Okay, if you don't get it, you don't get it. I thought
you might be trying to go deeper on the issue of
computer proofs than "what you see is what you get." A
mere printout judged as a printout.

Apparently not. So forget it.

Tom
.

Relevant Pages