Re: Transactions: good or bad?

From: Costin Cozianu <c_cozianu_at_hotmail.com>
Date: Sun, 15 Jun 2003 08:44:08 -0700
Message-ID: <bci44j$j85o4$1_at_ID-152540.news.dfncis.de>


Alfredo,

Get your facts in order , read more about foundations of mathematics and logic and maybe we can continue the discussion later. Philosophical debates are a waste of time, especially if your continue to claim that Mathematics is not a science and if you "think" or "believe" chess game is infinite, when even the most elementrary Mathematical skills should allow you to see the obvious.

Until then I just posted some rebuttals if you're curious, but I'm in no mood and have no interest to continue the discussion at this level.

Cheers,
Costin

Alfredo Novoa wrote:
> Costin Cozianu <c_cozianu_at_hotmail.com> wrote in message news:<bcfed9$idmcu$1@ID-152540.news.dfncis.de>...
>

>>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.

>
>
> A computer can emulate the behavior of a small neuron network without
> any problem.
>

This is unsupported speculation, not science. Your "philosophers" should teach you better than this.

> A neuron has input lines, output lines and a signal processing logic.
> It is an analogic processor.
>
> We know pretty well how a neuron work.
>

Obviously your claims are just hot air, since we're very far from "real" or "unreal" AI. We don't really know how neurons work. We know that they transmit signals, but that's not the bottom line.

>

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

>
>
> Perhaps, but what is sure is that there is not any scientific theory
> that might give us a hint that we can not construct intelligent
> computers.
>

Modern mathematics gives us plenty.

>

>>>>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. 

>
>
> They deserve and have a lot more intellectual standing than Dijkstra.
>

That's non-sense.The above figures might have greater pop-cult status among the kibitz, but that has nothing to do with what we're talking about. Within Mathematics we don't talk about "intellectual standing" and Dijkstra is a mathematician with *essential* contributions, and many of them programmer will still play catch-up with, for decades.

What he was refering to in the context is that philosophy is not a science and philosophical arguments have nothing to do (therefore no intellectual standing) within a science, and especially within Mathematics. All philosophical endevors in Math have been proven wrong one way or the other.

Read "Scientisme et obscurantisme" for a very funny account.

>

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

>
>
> I have readen one called Les fondements des mathematiques and his
> opinions against theorem proving are not very well founded.
>
> "que le lenguage informatique es déterministe - il s'exécute dans un
> ordre précis"
>
> It is a complete nonsense.
>

Why don't you write him a nice letter.

Girard is one of the greates mathematicians of our time, and his contributions are widely used by computer scientists (in particular all relvant books on programming languages, formal methods and a few other domains cite his System F and the more recent contributions).

What I suspect is that you don't have the necessary mathematical background to understand what he writes, otherwise you'd come up with a real argument.

Trashing doesn't come close to an argument, and while Girard is justified at anytime to dismiss Alfredo Novoa's opinionated nonsense as trash , the reverse does not hold.
>

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

>

>
> It is not finite if you don't limit the number of turns, and a
> complete search is unfeasible. A chess problem is not very different
> to a theorem proof.
>

I can understand your lack of knowledge in Math, but this non-sense you just wrote is unexcusable, especially after trashing Girard.

Read my leaps: chess has a finite model, chess *is* finite. If you're not able to see the obvious, you come borderline to trolling.

>

>>>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.

>
>
> Even if it was true (you can not prove it and we don't know what to
> think is), it is not the case of all theorems.
>

It is the case for more than enough theorems, those that counts. It is so much the case, that a computer will not "find" a proof unless it is launched by a mathematician in a particular domain, and on a particular theorem, where the mathematician who launched the program, either knows for sure that the search is finite, or knows or has good reasons to believe that the particular resolution mechanism utilized by the program will find the proof.

Give the computer Peanno's axiomatic construction, and let him solve modern algebraic problems, and it'll blow smoke.

>

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

>
>
> Brute force and other search approaches are not limited to finite
> models, and if you have proved something the method used does not
> care.
>
> Human proving is also a search. Humans are good restricting the
> search.
>

You obviously have not done enough Math to know this is trivially false. A human will extend the model he's working with if needed, a computer is not.

>

>>>It is very easy to create a software which proves not very trivial
>>>boolean algebra theorems.
>>
>>Yes, but we are not talking trivialities here.

>
>
> Then you are talking only about very hard to solve theorems. You were
> not specific.
>

The discussions started with the claim that you can construct an AI system that will prove your programs, or at least that will be able to generate an exhaustive set of test for your programs.

While that might be feasible if you annotate the programs with proofs, it was obvious the discussion was about generic plain vanilla programs.

This makes the theorem proving involved hard enough for all intents and purposes.
>

>>Do you know the Halting problem ?

>
>
> More or less.
>
> http://www.wikipedia.org/wiki/Halting_problem
>
> It is a problem for humans too, but we can stablish heuristic halt
> conditions.
>

No, it is not a problem for humans bevause we have not established that humans can be modelled by Turing Machines.

> Lots of humans fail trying to prove some theorems, and some proofs are
> found when humans are looking for other things.
>

That's what computers don't do.

>

>>No. Humans are creative theorem provers.

>
>
> Kasparov said that Deep Blue made several creative movements, and
> computers have proven theorems which mathematicians thougth they were
> reserved for creative theorem provers.
>

Very "creative" indeed. Creative by means of an exhaustive partial search.

Are we talking fantasies here ?

> It was not proved that we can not construct creative computers, but
> creativity is not always the only way. Automated theorem proving
> progres a lot faster than strong artificial intelligence.
>

Oh, strong AI has been largely discredited as a scientific hoax by now. And the progress, while significant for theorem provers as human helpers, when considered from your absurd theories that there's no difference in principle between computers as mathematicians and humasn as mathematicians, well, that progress is not even good enough to

>>>>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.

>
>
> If you meant we can not create a software which can solve ALL theorems
> then of course, but humans can not either.

Humans can decide which theorems are important and which are not, which are worth pursuing and which are not, which reasearch direction should be abandoned altogether.

>>>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.

>
>
> Well, acording to Popper we can not prove any scientific theory with
> certainty, they can only be shown to be true beyond a reasonable
> doubt, the only certainty is in disproving scientific theories.
>

You don't "prove" emipirical theories. We were talking about formal theories here. Popper told you the difference ?

> Do you think the human mind is supernatural? :-)
>

You haven't explained what's your definition of super-natural, but for all intents and pruposes human brain is part of what common language calls it "nature". That's as far as I'll go with you into philosophical junk.
>

>>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.

>
>
> But this could change (or not). If you don't know what intelligence is
> then you can not prove we can not construct an intelligent machine
> ever.
>

Within the current definition of computing machines (Turing equivalent that is), it's been proven "beyond a reasonable doubt".
>

>>>>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.

>
>
> Which ones?
>

Search in finite models with proof.

> You are mixing the hability of proving theorems with the motivations
> and desires for sending a paper to a scientific journal.
>
> You don't need to know what a scientific journal is in order to prove
> a theorem.
>

No. You need to be able to understand what theorems are significant and what theorems are not interesting. A journal will publish only interesting theorems. A human scientist will generally send to publication only articles that he deems intersting and having a chance to be published. He will also write the article skipping over obvious proofs, or over less obvious but mechanical and unsubtle proofs (putting them in Appendix eventually), and so on so forth. Valuating and communicating knowledge, that is.

In so doing humans enhance their ability to construct Mathematics over an infinite domain of all the junk that may otherwise come out by mechanizing axioms and inference rules.

And as far as empirical science goes, this human knowledge has a lot to show for it. AI has nothing to show for in comparison and from a proper scientific perspective. As we say in Romania they have a part of a wheel, they need to finnish the wheel, have 3 more, a cart and a horse .

They might have something in the future or they might not. Any "debate" over that is piss poor fight over "beliefs". Ain't gonna go there. You can shout your beliefs as loud as you want, I frankly don't care.

> By the way mathematics are not science.
>

The BS statement of the month. Received on Sun Jun 15 2003 - 17:44:08 CEST

Original text of this message