Re: Article in Scientific American
- From: Chris Smith <cdsmith@xxxxxxx>
- Date: Tue, 26 Dec 2006 08:27:07 -0700
T.H. Ray <thray123@xxxxxxx> wrote:
Can you clarify what you mean by that? If the
computer gives a proof,
then the statement is provable. However, if the
computer simply prints
out "true", then how does that "not not prove" the
theorem?
The computer proof of a theorem actually rests on
assumptions that not only is the theorem provable, but
that it is not not provable. I.e., without an algorithm to
verify a proof, we hand check the proof for logical
gaps.
Err, well, if you can hand check the proof for logical gaps, then it
doesn't fit into this discussion. No one (that I've seen) is arguing in
this thread that a proof should be considered invalid merely because a
computer wrote it.
Because an algorithm may contain no logical gaps,
however, how does one know that the proof that a
proof-checker produces is not merely proof of the validity
of the proof-checker's algorithm?
I'm not sure what you're saying. If you want to bring proof-checkers
into this discussion, then you'll need to explain what you are saying
more clearly. A proof that is checked for validity by a computer is, of
course, still a proof. The discussion here is more about whether
relying on the output of a computer as a critical component of a proof
is valid.
If you mean that the computer proof-checker will check a proof
constructed by a computer, that implies that the computer first produces
a proof that can be checked. Presumably that proof itself would be
published, rather than the source code of the program that created it.
Then we're still okay. No problems there. Perfectly valid.
This case differs from the case in which computer aid
is enlisted to calculate, or to recognize. The Appel-
Haken proof of the 4C Theorem, e.g., assumed the validity
of the computer proof only to the extent that the
computer algorithm was able to recognize the identified
finite set of maps.
So that latter case is, indeed, the one we are discussing.
Oh, yes, they do pertain in a most important way. You
can't simply ignore Montgomery-Smith's point that
agreement among computer methods increases the probability
that a specific computer proof is true.
The point was only that using different operating systems or different
compilers will tend to mitigate the possibility of compiler or operating
system bugs. I didn't ignore it. In fact, you responded to my answer,
which is that catching bugs by observing results amounts to only
accepting a disproof of some part as a refutation of a proof. Testing
on different operating systems and compilers only catches a small
portion of even these flaws. I can guarantee that there are lots of
bugs that don't manifest themselves merely by running code on a variety
of operating systems or compilers.
With a traditional proof, if there is any gap whatsoever in the logical
reasoning, someone is likely to read the proof and see it eventually,
and the proof will be fixed or rejected. This is true even when every
individual statement of the proof is correct. I think that's a good
standard, so I can't like relaxing it just because someone decided to
use a computer.
If you mean something more by "agreement among computer methods" (which
is a rather odd phrase for building a program with two different
compilers, so I suspect you mean to imply something more), then please
specify what you mean.
The question of whether a computer verification, of a
computer proof, proves more than the validity of the
algorithm that produces the answer, is significant.
It may be significant, but it's not under discussion here. I pretty
much accept without question that successful computer verification of
actual proofs makes them more likely to be correct. If you want to
discuss it, be my guest. If that's all that you're intending to
discuss, then please be more clear that you're bringing up a new
discussion; it sounds like you're replying to me, here.
In fact, you will find that I agree with your position,
that a computer as theorem prover leaves a lot to be
skeptical about.
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
.
- Follow-Ups:
- Re: Article in Scientific American
- From: T.H. Ray
- Re: Article in Scientific American
- References:
- Re: Article in Scientific American
- From: Chris Smith
- Re: Article in Scientific American
- From: T.H. Ray
- Re: Article in Scientific American
- Prev by Date: Re: bundles
- Next by Date: Re: (geometric problem) Explain with the proper equation
- Previous by thread: Re: Article in Scientific American
- Next by thread: Re: Article in Scientific American
- Index(es):
Relevant Pages
|
