Re: Transactions: good or bad?

Alfredo Novoa wrote:
<snip ... >
> What are neurons if not little computers?
>

You don't know that they are computers. As a matter of fact now computer has come even remoteyl close to what neurons can do.

Nor even is there any scientific theory that might give us a hint that we'll be able to construct intelligent computers.

>
>>Any book with philosophy in its
>>title raises my high level of suspicion.
>
>
> Books like Rusell's Introduction to Mathematical Philosophy? :)
>

Yes. I haven't read it nor have any plans to. One has to pick and choose what he reads.

Given that I'm professional software engineer I prefer Mathematics that has nothing to do with Philosophy, which is a non-science and is a waste of time. As soon as you introduce Philosophy into Math (not to mention of people who want to introduce it in Software Engineering), shit happens

>
>>To quote Dijsktra, again:
>>
>>"It seems there are societies in which philosophers still have some
>>intellectual standing"
>
>
> Philosophers like Rusell, Wittgenstein, Popper, etc?
>

Especially the guys like them. It looks to me that you haven't read Gyrard's papers on the history of logics and foundations of mathematics.

>
>>>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.
>
>
> Saying that computers can not make proofs is like saying that
> computers can not play chess. It is an every day reality.
>

Playing chess is not a proof. For all the programs we are talking about , playing chess is a search in a finite model.

>
>>According to people like Dijkstra, Girard and others, this alone should
>>allow you to draw the conclusions that computers "don't think".
>
>
> But a computer does not need to think in order to prove a theorem or
> to find a stalemate in five movements.

Exactly he only neeeds to compute. In order to prove Pythagora's theorem you have to think.

> And computers don't think is
> not the same as computers can't think.
>
> "Conjectures best suited to this approach are combinatorial
> problems in new areas of mathematics, where human intuitions are less
> well developed, [Wos,
> 1993]. The Robbins Algebra conjecture is a good example. Brute force
> search through all the
> various possibilities is often an appropriate approach to such
> problems | and machines are much
> better suited to brute force solutions than humans."
>
> "A. Bundy. Survey of Automated Deduction 1999"
>

Oh, great. So you admit to confusing search in a finite model with proving.

>
>>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.
>
>
> I still don't see any argument. But you are now talking about creating
> mathematics. Your former assertion was computers can not prove
> theorems and is evident it is against reality.
>

Against what reality ?

> It is very easy to create a software which proves not very trivial
> boolean algebra theorems.
>

Yes, but we are not talking trivialities here.

> Talking a little about databases :-)
>
> "The response to a query is a theorem. The process of deriving the
> theorem from the axioms is a proof. The proof is made by manipulating
> symbols according to agreed mathematical rules. The proof [that, is
> the query result!] is as sound and consistent as the rules
> are."(emphasis mine). A DBMS, then, is a deductive logic system: it
> derives new facts from a set of asserted facts.<snip>"
>
> http://www.pgro.uk7.net/fp1e.htm
>

It has no bearing on the discussion. A database is pre-programmed for certain calculations. That's nto the same with creating proofs, which is how the discussion started.

>
>>What a splendid "popularization of science" marketing paper written by a
>>dumb journalist.
>
>
> IMO it is a good science divulgation article in a prestigious (a
> little less prestigious this on days }:-) newspaper.
>
It doesn't change the fact that the article has no value.

>
>>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".
>
>
> Proof checkers and proof makers. You see only what you want to see.
>
> Most of human proof makers also rely heavily on other human inputs. I
> don't see the problem.
>

The difference is that humans create mathematics. Computers do not. Humans create computers.

> Human lemma selection is not essential but it saves a lot of search
> time. Only axioms and rules are essential inputs.
>

Do you know the Halting problem ?

>
>>Otherwise a computer is not able to decide when he's on a wrong,
>>infinite path (aka the Halting Problem).
>
>
> It is not an unsolvable problem. Humans have similar problems
> sometimes.
>
> Humans are not near of being perfect theorem provers either.
>

No. Humans are creative theorem provers.

>
>>Computers are very well equiped to perform calculations.
>
>
> Computations is a better word.
>
No, it is not.,
>
>>might be able to verify and sometimes even construct (albeit with
>>essential human help) calculational proofs.
>
>
> Finally you have admited that they construct proofs :-)
>
>
>>To quote J.Y Girard
>>"l'ordinateur n'est qu'un cyber-cretin".
>
>
> A cyber-cretin which is able to beat Kasparov and to prove simple
> theorems and other not so simple.
>

The cyber-cretin is able to beat Kasparov in the same way it will beat you in a "who's adding faster" test. And it's the same way it "proves" rather trivial theorems.

Actually the guy who really does the proof, is the mathematician who fed the specification in the computer and who made the *intelligent* decision that the problem admits a resolution in the calculation model of the particular theorem prover.

Otherwise, you can send a computer in an infinite loop as easy as 1+1=2
>
>>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.
>
>
> Why?
>

Well, go read up a serious book on logic. Or you can start with Girard's articles.

> I don't think there is anything supernatural in the human mind. If we
> can think other machines also could. But you don't need to be
> self-concious in order to prove a theorem.
>

You don't "believe" there's anything supernatural. And you don't know , you only "believe" you are a machine.

You need to be intelligent. And we don't know exactly what intelligence is, but we know for sure that computers don't have it.

>>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.
>
>
> You are mixing very different things.
>

No, it is you who are mixing very different things. You should educate yourself in modern logic and proof theory.

>
> Regards
> Alfredo

Best,
Costin Received on Sat Jun 14 2003 - 17:21:02 CEST