Re: Transactions: good or bad?

"Costin Cozianu" <c_cozianu_at_hotmail.com> wrote in message news:bcl0p3$k8tsm$1_at_ID-152540.news.dfncis.de...
> Bob,
>
> You claim that Alfredo didn't go over into philosophical grounds, I
> think it is the other way around. Indeed, in his first post he only
> claimed that computers do make proofs, and on the face of it, his claim
> is trivially true.

Then you could have simply accepted the statement on the face of it and avoided philosophy altogether.

> However the context of this discussion if you actually bother to read
> was the problem whether computers can create proofs of correctness, or
> incorrectness for that mater, for programs written by humans.

I am fully aware of the context of the discussion, and the context in no way alters what Alfredo actually said.

> This would
> require computers to solve problems no less general than an universal
> theorem solver. This is known (proven) to be impossible.

Why, then, did you not simply state the limitations of automated theorem proving? Why did you introduce the philosophical arguments of Girard and Dijkstra instead?

> Even if we restrict the theorem solving capability to what humans can
> do, it is also well beyond the frontier of current science

This is pure conjecture. Computers have proved superior in some cases to humans for proving theorems, which is a statement of fact for which we have empirical evidence previously cited in this thread.

>, and if we
> want to talk about beliefs of what science will do in the future we can
> go no further than to Hilbert, otherwise a brilliant mathematician, who
> held very strong *beliefs* about his program, beliefs which have been
> refuted only too soon after they were expressed.
>
> It is obvious given the state of the science so far that computer
> proving is less general than human proving.

It is not obvious to me, and you have presented nothing but handwaving in support of your assertion.

> To quote J.Y. Girard: "Automatique proof ne fonctionne pas et ne
> fonctionnera jamais" (automatic proof doesn't work and it will never
> work).

Much to Girard's embarassment (I am sure), computers have gone and contradicted his belief.

> This is not a belief this a scientific statement coming from
> probably the most important logician of our times.

Since computers have already contradicted the assertion by proving theorems that stumped humans for decades, Girard's statement is demonstrably belief and not science.

> It should be obvious
> both to you and to Alfredo that he knows about computerized proofs, but
> what he means is that computer will never be able to solve mathematical
> problems with the same generality as humans are capable of.

Girard is welcome to his faith. I remain agnostic on the issue.

> Furthermore, both you and Alfredo expressed the philosophical belief
> that human brain is in no way different than computers

Ahem. Where, exactly, did I express this extraordinary belief?

> Both of you made trivial mistakes, like the ones with the game of chess,
> the last one you asked "Where's your proof that all chess games halt ?"
> . If I were to respond to that I'd have to consider you either
> incompetent or in trolling mode. The mission of a chess playing program
> is to decide the next best move and in so doing also evaluate a
> position, to which the problem whether there are infinite chess games is
> totally irrelevant.

Unless a chess game halts, it is infinite in the dimension of time. I think that makes my question quite competent, informed and legitimate.

> The same can be said of the situation where I
> claimed that mathematicians extend their models to which you reply that
> computers extends their theorem base, if you can't see the distinction,
> I frankly can't waste my time much longer.

Nobody asked you to waste anybody's time. You are welcome to stop at your leisure.

> You should also take notice that "I disagree" with your characterization
> that I transformed this in a pissing match, and with regards to your :
>
> "you might move the discussion in the direction of something truly
> illuminating. And who knows? You might inspire some anonymous lurker to
> pursue a path that leads to some truly important result."
>
> I can only say that it has to get worse before it gets beter, there's no
> illuminating to be had in a piss poor exchange of trivialities, and I
> truly pitty the anonymous lurker who deludes himself that he can find
> truly important results departing from Usenet discussions.

Well, you surprise and disappoint me, Costin. You lack either the balls or the intellectual honesty after all. Received on Tue Jun 17 2003 - 03:32:50 CEST