- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Fabien BESNARD <Fabien.BESNARD.domain.name.hidden>

Date: Fri, 12 May 2000 00:16:16 +0200

I suggest changing the thread, since it's a new subject.

*>L over some finite alphabet A, and in
*

*>particular, *this language is finite*.
*

This is not consistent with what you say later.

*>I'll explain why I think these assumptions are okay. Basically, we could
*

*>let A = {0,1}, and if we assume that any mathematical text could be
*

*>translated into, say, LaTex or some other appropriate system for
*

*>representing maths, every mathematical text can be reduced to a sequence
*

*>of bits. The language L we are refering to, then, would consist of the
*

*>languange of all text files which LaTex compiles into a piece of correct
*

*>mathematics (which has already been written, note!).
*

But there is an infinite number of such files.

*>Now the big question is, what's so special about this language L?? Is
*

*>*anything* special about it? In particular, given some such finite
*

*>language L, how would we decided whether it is mathematics or not? Do
*

*>these questions make sense??? :)
*

They all make sense, and have been extensively worked on (except that I

don't see why you insist on your language being finite)

The answer is yes : you can run a program telling you if a mathematical

demonstration written in a formal language and using formal logic is correct

or not. The problem is that, except for very very simple theorems, no one

can really write math proofs in a formal language. So automatic

demonstration (which is a well developped branch of computer science) can't

be applied to "real" maths.

*>I suspect that the language is to some extent unimportant. After all, any
*

*>finite language can be recognised by a finite state automata, and who
*

*>would like to claim that mathematics is nothing but structures recognised
*

*>by FSA's?
*

In principle, it is...and it is not ! What these automata tell you is that

the derivation of a theorem is correct or not. But this demonstration relies

on the axioms of the theory. So the choice of axioms is crucial, and these

automata will never tell you if you have chosen a good system of axioms for

what you had in mind (they can sometimes tell you that the system is

inconsistent if they happen to meet such an inconsistence, but that's all).

*>From the formal point of view the axioms have no meaning, they are just
*

sentences in your language, but for a mathematician they have an intuitive

meaning (which may or may not be right).

*>It seems to me that the only way of reconsiling this is by
*

*>accepting that, when someone reads a mathematical text, we are performing
*

*>*computations*, and it is this additional structure, along with the
*

*>language, which is important.
*

I don't know if this is what you have in mind, but when you read a math

text, you do a lot of things : accept to use notations which are obviously

ambiguous, use many times the same name to call different things, fill the

blanks in every proof with trivialities the author did not care to write

down, and finally, write the proof yourself when the author says "this is

obvious" (almost 50 percent of the time) !

---------------------------------------------------------------

Fabien Besnard

http://perso.wanadoo.fr/fabien.besnard

Received on Thu May 11 2000 - 15:36:36 PDT

Date: Fri, 12 May 2000 00:16:16 +0200

I suggest changing the thread, since it's a new subject.

This is not consistent with what you say later.

But there is an infinite number of such files.

They all make sense, and have been extensively worked on (except that I

don't see why you insist on your language being finite)

The answer is yes : you can run a program telling you if a mathematical

demonstration written in a formal language and using formal logic is correct

or not. The problem is that, except for very very simple theorems, no one

can really write math proofs in a formal language. So automatic

demonstration (which is a well developped branch of computer science) can't

be applied to "real" maths.

In principle, it is...and it is not ! What these automata tell you is that

the derivation of a theorem is correct or not. But this demonstration relies

on the axioms of the theory. So the choice of axioms is crucial, and these

automata will never tell you if you have chosen a good system of axioms for

what you had in mind (they can sometimes tell you that the system is

inconsistent if they happen to meet such an inconsistence, but that's all).

sentences in your language, but for a mathematician they have an intuitive

meaning (which may or may not be right).

I don't know if this is what you have in mind, but when you read a math

text, you do a lot of things : accept to use notations which are obviously

ambiguous, use many times the same name to call different things, fill the

blanks in every proof with trivialities the author did not care to write

down, and finally, write the proof yourself when the author says "this is

obvious" (almost 50 percent of the time) !

---------------------------------------------------------------

Fabien Besnard

http://perso.wanadoo.fr/fabien.besnard

Received on Thu May 11 2000 - 15:36:36 PDT

*
This archive was generated by hypermail 2.3.0
: Fri Feb 16 2018 - 13:20:06 PST
*