Re: Article in Scientific American

T.H. Ray <thray123@xxxxxxx> wrote:
I am not quite sold. Montgomery-Smith's context was
that of computers checking computers.

I am not aware of such a context. The context was a discussion of
whether a computer program should be considered to constitute a proof,
in the sense that the program is run and if it prints "true", then that
is considered sufficient evidence that the theorem is true without
requiring additional proof.

Yes, but the probability of the computer program being correct does
increase it if it is run on different computers with different
compilers, operating systems, etc.<<

That sure sounds like not not provable to me.

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 rest of your post is unintelligible to me. I don't mean that as a
casual dismissal; I did try to read and understand it; it just appears
to be a lot of generally true statements (with the exception of the
phrase "or among computer proofs", which seems to beg the question) that
don't pertain to this discussion.

Again, the question was whether the existence of a computer program that
outputs "true" should be considered a proof. I argued that it should
not. My reason is that unlike in the case of a proof, the bulk of the
program code is not read by other mathematicians as a primary means of
understanding why the statement is true. Aside from being a significant
difference in practical utility in itself, this means that errors in the
program are likely to be found only if they give verifiably incorrect
output. That is equivalent to the theorem being disprovable. We've
lost the potential that someone just realizes a gap in the reasoning
even though the theorem is still true; or that the theorem is not
disprovable but also not provable, so the program "proves" it in error,
but no one will ever notice that fact.

Hence, relying on observed fact, that a computer program prints some
output, as a proof amounts to subjecting the theorem to a less strong
standard of truth, over sufficiently large spans of time.

[I'll again point out that if you write a computer program that produces
a proof, then I have no problem with that proof, so far as it really
does prove the proposition. Furthermore, if you (a) write a computer
program, then (b) prove that it prints "true" only if the theorem is
true, then (c) prove that it prints "true"; then I have no problem with
the proof. It's only when step (c) is verified by empirical observation
rather than proven that the "proof" is questionable, in my view...
though in either case, there's probably a more straight-forward way to
write the proof.]

--
Chris Smith
.

Relevant Pages

  • =?iso-8859-1?q?Re:_Torkel_Franz=E9n_is_dead?=
    ... people reason well in non-mathematical contexts." ... I took into account the context, and none of your discussion of the ... rather only that they do not have a talent for formal logic. ... don't have an APTITUDE for symbolic logic. ...
    (sci.logic)
  • Re: OT: Lets Take the Religion out of Christmas
    ... >> meaning if it requires arithmetic but cant use such arithmetic. ... and that is what non-provable means in this context. ... then there is no "reason" for the statement. ... > Your invocation of the incompleteness theorem is typical of many ...
    (sci.electronics.design)
  • Re: 50 years later, Marvin Minsky still doesnt get it
    ... And for some reason which I can't grasp, you seem to think this is ... The result is that the associations developed over experience answer the ... the knowledge updates that need to happen are not evenly ... the most likely knowledge updates needed for any new context. ...
    (comp.ai.philosophy)
  • Re: speeding
    ... the fact that *I* brought it up isn't a good reason for declaring ... distinct interpretations, depending on context (as of course most ... distinctions in interpretation depend on context). ... rarely if ever is there any confusion as to what it refers to. ...
    (uk.rec.driving)
  • Re: The truth about NFL contracts.
    ... It's almost always the case, and you've proven it to be true in this case, that when someone resorts to those tactics, they know they're wrong, they know they have no defense, and so all they can do is to take snipets of what someone else posted completly out of context and try to structure some sort of story which was never the case. ... Too fucking bad, bitch. ... players) will not change. ... *Therefore* means *for that reason*, and so the previous statementis the whole reason for the one you posted you fucking moron. ...
    (alt.sports.football.pro.ne-patriots)