[FOM] Re:Certainty (Ideas in Proof Checking)

[Harvey Friedman]

Reply to Piper 6:32PM 6/23/03.

>
>     I agree with Dr. Friedman in that we should develop a standard formal
>notation and that, yes, there will be great difficulties in developing a
>standard informal notation, but this should be a central aim of at least some
>FOMers.


>I don't personally believe that a primary
>task of mathematicians is to verify proofs.

I agree. But there is a deep question here concerning the general feeling that

1) mathematics has a special kind of "absolute certainty" not 
attained by other disciplines;

2) there is an absolutely objective standard of mathematical rigor.

There are various subtle differences in just how one can reasonably 
construe 1) and 2), including issues of actual construction.

I have no doubt that many mathematicians, at least at the 
subconscious level, do not appreciate the enormous power of 
formalisms, and don't believe that there can be a real notion of 
actual complete proof. There is the "idea" that formalisms are in 
some sense fake, not helping us create any new mathematics, nor 
providing any insight into the nature of existing mathematics. 
However, mathematicians are not good at communicating about such 
matters, as they do not regard such issues as legitimate parts of 
their professional life. Also, working with formalisms and core 
mathematical logic is sufficiently different in conceptual spirit 
from core mathematics, that an inherent distrust develops at the 
subconscious level, where mathematicians actually acquire the desire 
that formalisms be worthless. It takes substantial extramathematical 
abilities to perceive the subtleties involved in formalisms, to 
evaluate them, improve them, and see what is accomplished and not 
accomplished by them.

So we have the ironic situation that the world's greatest producers 
of (deep) mathematics by far - professional mathematics - are 
clueless when it comes to carrying on even an intelligent 
conversation about issues such as 1) and 2).

So one reason for coming to grips with 1) and 2) from various 
dimensions such as the one I am currently writing about, is to raise 
the level of discourse about the fundamental nature of mathematics 
and mathematical activity, as well as provide lots of stimulation for 
philosophers.

But there is another, perhaps more important, reason for this work. 
It is an absolute prerequisite for a major assault on the following 
problem:

3) completely overhaul programming methodology so that not only is 
the development of large programs in the new methodology far easier 
than it is now, but also the development of formally verified code 
during the development stage becomes feasible, and even cost 
effective, for critical programs. Efficiency is to remain 
substantially in tact.

Accomplishing 3) requires not only an extremely successful 
implemented form of what I am trying to do now, but also a complete 
overhaul of existing programming methodology.

Incidentally, the entire computer revolution shows over and over 
again the extreme power of formalism, and the extreme importance of 
mathematical modelling of discrete phenomena. Both of these 
directions have not been championed by professional mathematicians.

>I do however believe that there is
>such a thing as certainty and that it can, in principle, be 
>verified. This would
>seem to be a secondary task for a universal or standard formalism, the primary
>task being to communicate mathematical ideas and proofs.

I am deeply concerned with both tasks. In any major overhaul of 
software development, there must be universal standards for the 
specification of software that are highly flexible and understandable 
and powerful. Doing this for the communication of mathematical 
information is an obvious first step of great independent interest. 
E.g., it will support the UMD (universal mathematical database).

>
>     I do have a question concerning the proof program Dr. Friedman is
>describing. I actually have several. One, is this a real program 
>being developed
>by you or your colleagues or is it some sort of grand idea that may come to be
>in the near future?

It is based on ideas I have thought about for a long time, but never 
organized properly. The FOM seems like a great place to flesh these 
ideas out, and enforce discipline on me to state them clearly, and 
improve them in real time.

>     Two, I like the idea of forcing predicates or functions or theorems to be
>absurd and I can tell how this will be useful to the philosopher in making
>arguments (formal or informal) but I am not sure this will be terribly useful
>for any interesting mathematics.

The thesis is this: it is completely straightforward, if you 
understand an easy proof, to argue completely negatively - in fact, 
perhaps easier. Remember, I am relying on LEMMA ENRICHMENT, which 
means that the REAL IDEAS come up in the form of the statement of the 
completely natural, understandable, lemmas. So proofs are quite 
straightforward - but perhaps NOT so straightforward that the 
computer can find them without help from the user.

Actually, if you examine the approach in posting #184 (and #185...), 
it will be clear that there is a lot of forward, positive reasoning 
going on within the unfinished modules. So, in fact, large portions 
of these proofs WILL be forward looking when they are naturally 
forward looking.

>Correct me if I am wrong, but if we have a
>formal system capable enough to express number theoretic relations, 
>shouldn't we
>arrive at statements in number theory that will not be absurd to the computer?

I think you are missing some fundamental points. The absurdity of 
F(A) is the same as the truth of T(A) is the same as the truth of A.

Arguing negatively provides a unidirectional mode that supports 
extreme modularity and the banishment of any possibility of errors, 
and relieves the requirement that one knows where one is in the proof.

There is simply a mad SCRAMBLE to bull forward and get that 
contradiction! All of life is suppressed, momentarily, for just that 
SUBLIME explosive contradiction!!

I believe that it will prove spectacularly effective. But that has 
NOT BEEN DEMONSTRATED YET with appropriate examples.

Also LEMMA ENRICHMENT will prove to be spectacularly effective, so 
that all proofs are ALMOST TRIVIAL. And also the WILD CARD rule, 
which has great psychological benefits, knowing in advance that you 
will never have to remember just what you have left undone for later 
work - the computer will catch up with you later!! You can run, but 
you can't hide!!!

NOTE: ALL OF THESE IDEAS EXIST IN AT LEAST SCATTERED FORM FOR PERHAPS 
TWO THOUSAND YEARS.

I'm trying to put them together properly into a single unified 
system, taking advantage of the computer age.

>What I mean by this is, assuming F(A) for some number theoretic 
>statement A does
>not guarantee a tree model with "closed branches", i.e. there will be some
>branches of the tree undecided and so we cannot say whether F(A) is absurd or
>T(A) is absurd, and hence we can have no certainty (I'm not sure 
>this the right
>word I would like to use here) of either case. I feel like this is closely
>related to the halting problem. If this doesn't make sense right 
>now, feel free
>to write me back so that I can clarify.

This is not correct. The rules of proof underlying this approach are 
well known to be sound and complete.

Suppose you are trying to prove a Lemma that YOU have created and 
know how to PROVE on the basis of earlier statements from the RECORD. 
That means that you know what to IMPORT from the record so that the 
Lemma in question logically follows from the imports, in the usual 
sense of (some version of) predicate calculus. Then you know that 
this extremely user friendly variant of the Beth tableaux method must 
halt. That is from the completeness theorem for Beth tableaux.

Perhaps you are mistaken: your Lemma does NOT follow logically from 
the previous record, or you don't know what to import and manipulate 
from the previous record. Then, of course, your issue comes to the 
fore. But then you are supposed to rethink what's in your head, and 
come up with some more Lemmas, or modify them, or get help from a 
better mathematician, etcetera.

>     Three, in light of what I have just said, I am a little unclear as to
>whether or not this ideal program of yours is intended to simply verify or
>simply to construct proofs.

Verify, only.

Obviously, you can't verify any normally written prose in the 
Journals, or even on FOM (smile). So the "professional proofs" in 
Journals must be recast in another form. If you want, you can call 
this recasting, "constructing proofs".

>I believe you imply that it will be useful to
>construct proofs, but I can only guess that it will help in constructing only
>trivial proofs.

I think that there is a chance that if this is done really well, 
there may be a NEW STANDARD of exposition adopted that is of at least 
EDUCATIONAL value - in addition to philosophical importance, use for 
overhaul of programming methodology, etc - and perhaps it might be 
seen to be of PROFESSIONAL value to getting the proofs in 
particularly useful forms, with this ENFORCED LEMMA ENRICHMENT. After 
all, many of these enriching lemmas are SHARPER results, that would 
lie buried in a complicated proof in normal expositions, and may well 
become useful in expected ways. Certainly that is my personal 
experience, since I only publish LEMMA ENRICHED proofs these days. 

>Perhaps I am being impatient, but I would like very much to know
>what you mean by "TRIVIAL". I am very intrigued to see if your conception of
>trivial is solely related to the complexity of a given statement A or if it
>encompasses the informal notion of triviality, which to me says "little or no
>effort (mental or physical) is required on the part of the mathematician in
>proving A.  In either case, I would be glad to hear your reply.

Just FORMALLY trivial. All trivial proofs can be FOUND by a computer 
in a reasonable amount of time. That is not the definition, but that 
is a consequence of the definition. It is still a bit too early for 
me to propose a good definition of TRIVIAL. I need to do some 
EXPERIMENTS first.

Harvey Friedman