[FOM] Re:Certainty (Ideas in Proof Checking)
friedman at math.ohio-state.edu
Tue Jun 24 00:18:22 EDT 2003
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
>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
But there is another, perhaps more important, reason for this work.
It is an absolute prerequisite for a major assault on the following
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
>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
>Correct me if I am wrong, but if we have a
>formal system capable enough to express number theoretic relations,
>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.
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
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
More information about the FOM