[FOM] Re: pom/fom directions

[Harvey Friedman]

Reply to Corfield. 

On 10/18/03 6:39 AM, "David Corfield"
<david.corfield at philosophy.oxford.ac.uk> wrote:

> I thought I had made it clear on page 50 that I don't think the Robbins
> problem is important. Trouble is automated theorem provers don't
> have too many other successes to report, discounting projects like Mizar to
> prove what we already know.

At the moment, and likely for quite a while, the most promising direction of
the two will be proof checking, rather than finding new proofs. There is,
however, a lot of work being done on proving new theorems in plane Euclidean
geometry. Although this is very beautiful, it is rather limited.

I wrote extensively on the FOM about my view as to the great vital
importance of proof checking, to be ultimately used to support the
development of verified software.

Such ideas are very well known to the specialists in proof checking, or
"proof assistants".

Having looked more closely at this area of "proof assistants", I have a
better understanding of where they are with this, and the obstacles that
need to be overcome. My enthusiasm for the area has been reinforced.

The big overarching difficulty, as I see it, is to get a good handle on just
what steps in an already well understood proof are "obvious". This is
important because presently, working with proof assistants is just too
cumbersome - one has to spell out a lot of obvious things. I am talking
about obviousness at the early undergraduate level, not at the professional
level. 

I did get some research plans down on paper (with some help), concerning
this "obviousness" problem, and took some preliminary steps. However, I
haven't got down to the time consuming part of implementing these plans.
They involve the examination of lots of data.

There is the main division of special purpose obviousness, and general
purpose obviousness. I think that there is room for major advances on both
fronts. 

In special purpose obviousness, one considers various important mathematical
contexts and develops special tools for those contexts that make the proof
assistant more capable of seeing what is really "obvious".

In general purpose obviousness, one uncovers general features of
mathematical reasoning, independent of context, that can be used to make the
proof assistant more capable of seeing what is really "obvious", regardless
of contexts.

We are talking about quite ordinary kinds of obviousness. We are not talking
about mathematically rich notions of obviousness. Routine obviousness only.

And what good is this?

E.g., in the vast preponderance of real world computer programming, any
proof one has in mind that the program is correct is generally
mathematically uninspiring, made of obvious steps, one after another.
 
> I found the case illuminating in that even in the unpromising, albeit very
> short, syntactical trace of the EQP prover, a real mathematician such as
> Louis Kauffman desperately searches for meaning. It throws into stark
> contrast the drive for certainty and the drive for explanation.

Please elaborate on your point, even if it has been spelled out in your
book. 

What you call the "drive for certainty" is an extremely rich, deep, and
clear motivation of great practical import which is not only a motivating
theme for work on proof assistants, but also in verification generally, and
also computer security.

These vast areas of computer science owe a lot to classical f.o.m., and in
fact are pursued in ways that are very much allied with classical f.o.m. The
fundamental divisions between syntax and semantics are similar, with careful
definitions by induction both on the syntactic and the semantic side.

So it is clear what the "drive for certainty" means and what it has led to,
and probably what it will lead to.

In the cases you wish to cite, what does the "drive for meaning" mean and
what has it led to, and what will it lead to?

Harvey Friedman