[FOM] 187:Grand Unification 2 - saving human lives

[Victor Makarov]

On Tuesday, 8 July 2003 12:11:58, Roger Jones wrote:

>On Wednesday 02 July 2003  3:39 pm, Harvey Friedman wrote:
> > This is a continuation of posting #186, and puts the proof
> > checking project into a wider perspective.
>...
> > What is needed is an appropriate mathematically friendly
> > functional programming language ...
>
>...
>
>I'm afraid that Harvey continues to "re-invent the wheel" with
>this line of enquiry.
>...
>I wholly approve of Harvey's new found interest
>in this problem domain, but I doubt that he has yet
>found a way in which his talents can make a difference.
>
>Roger Jones

I can not agree that "Harvey continues to "re-invent the wheel"". From 
recent Harvey Friedman's postings on proof checking actually follows that 
his goal is (in particular) to design a practical formal mathematical 
language - the input language of his proof-checking system ("an appropriate 
mathematically friendly functional programming language" can be a 
sublanguage of a practical formal athematical language).

Have we  invented this "wheel" -- that is, a widely accepted practical 
formal mathematical language? Certainly, not yet. Let me cite Samuel Buss  
(The Prospects for Mathematical Logic in the Twenty-First Century, in "The 
Bulletin of Symbolic Logic, Vol. 7, Issue 2 (June 2001), p. 181":

Prediction 3. Computer databases of mathematical knowledge will contain, 
organize, and retrieve most of the known mathematical literature, by

                                      2030 +- 10 years.

   The first step in fulfilling this prediction is to design a formal 
language which can faithfully represent mathematical objects and 
constructions in a flexible, extensible way. (End of citation).

(Prediction 1 is that the P versus NP problem will be solved by 2010 +- 10 
years and Prediction 3 is that "there will be limited but significant 
progress in artificial intelligence by 2050 +- 30 years).

Obviously, the problem of the design of a practical formal mathematical 
language is so important that we should just welcome any person (and, 
especially, prominent logicians) trying to suggest some hints how to solve 
this problem. But Roger Jones is also right that a lot of people have been 
working in this direction and much of their work deserves to be aware of.

Victor Makarov              http://home.nyu.edu/~yvm204/vm/vm.htm

_________________________________________________________________
Tired of spam? Get advanced junk mail protection with MSN 8. 
http://join.msn.com/?page=features/junkmail