Re: Transactions: good or bad?
Date: Fri, 13 Jun 2003 10:02:38 -0700
Message-ID: <bccvvt$hsj03$1_at_ID-152540.news.dfncis.de>
Alfredo Novoa wrote:
> Costin Cozianu <c_cozianu_at_hotmail.com> wrote in message news:<bcaktl$h5o40$1@ID-152540.news.dfncis.de>...
>
>
>>That's non-sense. Go read good old Dijkstra if you can't read Girard in >>French.
>
>
> Dijkstra has lots of writting, can you be more specifical?
>
Well, I don't have the exact number at hand but he wrote:
"The question whether machines can think is as ill posed as the question whether submarines can swim."
> I have not big problems with French. I will look for Girard, but you
> could read this:
>
> Artificial Intelligence: A Philosophical Introduction
> by Jack Copeland (Paperback - November 1993)
>
> http://www.amazon.com/exec/obidos/tg/detail/-/063118385X/qid=1055496292/sr=1-1/ref=sr_1_1/104-6927268-4867955?v=glance&s=books
>
> There is a second hand copy for $10. It worths a while.
>
No 10$ can compare with my time reading a good book versus my time reading a book that does not profit me. Any book with philosophy in its title raises my high level of suspicion.
To quote Dijsktra, again:
"It seems there are societies in which philosophers still have some
intellectual standing"
>
>>Huh, computer make elegant proofs ? You gotta be kidding. I'm affraid >>you fall in the same kind of ignorance you accusing others of.
>
>
> Are you sure?
>
> Are you aware of the state of the art in automated proving?
>
No, but I'm aware of the basics of logic and foundations of mathematics. According to people like Dijkstra, Girard and others, this alone should allow you to draw the conclusions that computers "don't think".
Computers can help people prove theorems, solve problems,etc, it will never be the caser that computers (the way we understand them now) will create mathematics.
> Here is a little example:
>
> http://ai.eecs.umich.edu/people/durfee/courses/492winter97/handouts/NY%20Times%20article
>
> It is from 1996 and is not the only case.
What a splendid "popularization of science" marketing paper written by a
dumb journalist.
>
> More examples:
>
> http://www-unix.mcs.anl.gov/AR/new_results/
> http://www.cs.cornell.edu/Nuprl/PRLSeminar/PRLSeminar01_02/Nogin/PRLseminar7b.pdf
>
Yes, sure. I see a lot of proof checkers, symbolic calculation engines, etc. Those are fine pieces of software. Most of them rely heavily on essential human input inm being able to "prove".
Otherwise a computer is not able to decide when he's on a wrong, infinite path (aka the Halting Problem).
> IMO computers are better equipped for symbolic logic than humans. It
> is only a time issue, perhaps a lot of time.
>
Computers are very well equiped to perform calculations. As such they might be able to verify and sometimes even construct (albeit with essential human help) calculational proofs. To quote J.Y Girard "l'ordinateur n'est qu'un cyber-cretin".
Otherwise try to think how you'll hand over first order logic and Peanno's axioms, and have a computer demonstrate say Fermat's Theorem, or even come up with a good primality testing algorithm.
It's provably impossible to create such a software that will take any sufficiently expressive formal system, a proposition in the system and *reliably* come up with the decision whether that proposition is a theorem or not.
The logical conclusion is that all we are talking about is computer assisted proofs.
As a matter of fact it seems from all the examples you presented that when they published the papers it was the humans who took credit for the precious few results that their computers could infer :) Isn't that kind of telling ?
When I'll see the first computer to take the decision to submit a paper to a scientific journal, all by itself, then I'll reconsider my position.
>
> Regards
> Alfredo
best,
Costin
Received on Fri Jun 13 2003 - 19:02:38 CEST