Some Objections to the Idea of the QED Project and Some Responses
- 1 Paradoxes, Incompatible Logics, etc.
- 2 Intellectual property problems.
- 3 Too much mathematics.
- 4 Mechanically checked formality is impossible.
- 5 If QED were feasible, it would have already been underway several decades ago.
- 6 QED is too expensive.
- 7 Good mathematicians will never agree to work with formal systems.
- 8 The QED system will be large, and hence, unreliable.
- 9 The cooperation of mathematicians is essential but mathematicians will have no incentive to help.
- 10 QED would divert resource more profitably employed in support of the verification of hardware and software.
- 11 The notion that interesting mathematics can ever, in practice, be formally checked is a fantasy
-
-
Objection 1: Paradoxes, Incompatible Logics, etc. Anyone familiar
with the variety of mathematical paradoxes, controversies, and
incompatible logics of the last hundred years will realize that it is
a myth that there is certainty in mathematics. There is no
fundamentally justifiable view of mathematics which has wide support,
and no widely agreeable logic upon which such an edifice as QED could
be founded.
Reply to Objection 1:
Although there are a variety of logics, there is
little doubt that one can describe all important logics within an
elementary logic, such as primitive recursive arithmetic, about which
there is no doubt, and within which one can reliably check proofs
presented in the more controversial logics. We plan to build the QED
system upon such a `root logic', as we discuss below extensively. But
the QED system is to be fundamentally unbiased as to the logics used
in proofs. Or if there is to be a bias, it is to be a bias towards
universal agreement. Proofs in all varieties of classical,
constructive, and intuitionist logic will be found rigorously
presented in the QED system---with sharing of proofs between logics
where justified by metatheorems. For example, Godel showed how to
map theorems in classical number theory into intuitionist number
theory, and E. Bishop showed how to develop much of modern mathematics
in a way that is simultaneously constructive and classical. A
mathematical logic may be regarded as being very much like a model of
the world---one can often profit from using a model even if one
ultimately chooses an alternative model because it is more suited to
one's purposes. Furthermore, merely because some logic is so overly
strong as to be ultimately found inconsistent or so weak as to
ultimately fail to be able to express all that one hopes, one can
nevertheless often transfer almost all of the technique developed in
one logic to a subsequent, better logic.
-
-
Objection 2: Intellectual property problems. Such an enterprise as
QED is doomed because as soon as it is even slightly successful, it
will be so swamped by lawyers with issues of ownership, copyright,
trade secrecy, and patent law that the necessary wide cooperation of
hundreds of mathematicians, computer scientists, research agencies,
and institutions will become impossible.
Reply to Objection 2: In full cognizance of the dangers of this
objection, we put forward as a fundamental and initial principle that
the entirety of the QED system is to be in the international public
domain, so that all can freely benefit from it, and thus be inspired
to contribute to its further development.
-
-
Objection 3: Too much mathematics. Mathematics is now so large that
the hope of incorporating all of mathematics into a system is utterly
humanly impossible, especially since new mathematics is generated
faster than it can be entered into any system.
Reply to Objection 3:
While it is certainly the case that we imagine
anyone being free to add, in a mechanically checked, rigorous fashion,
any sort of new mathematics to the QED system, it seems that as a
first good objective, we should pursue checking `named' theorems and
algorithms, the sort of things that are commonly taught in
universities, or cited as important in current mathematics and
applications of mathematics.
-
-
Objection 4:
Mechanically checked formality is impossible. There is
no evidence that extremely hard proofs can be put into formal form in
less than some utterly ridiculous amount of work.
Reply to Objection 4:
Based upon discussions with numerous workers in
automated reasoning, it is our view that using current proof-checking
technology, we can, using a variety of systems and expert users of
those systems, check mathematics at within a factor of ten, often much
better, of the time it takes a skilled mathematician to write down a
proof at the level of an advanced undergraduate textbook. QED will
support proof checking at the speeds and efficiencies of contemporary
proof-checking systems. In fact, we see one of the benefits of the
QED project as being a demonstration of the viability of
mechanically-assisted (-enforced) proof-checking.
-
-
Objection 5: If QED were feasible, it would have already been
underway several decades ago.
Reply to Objection 5:
Many of the most well-known projects related to
QED were commenced in an era in which computing was exorbitantly
expensive and computer communication between geographically remote
groups was not possible. Now most secretaries have more computing
power than was available to most entire QED-related projects at their
inception, and rapid communication between most mathematics and
computer science departments through email, telnet, and ftp has become
almost universal. It also now seems unlikely that any one small
research group can, alone, make a major dent in the goal of
incorporating all of mathematics into a single system, but at the same
time technology has made widespread collaboration entirely feasible,
and the time seems ripe for a larger scale, collaborative effort. It
is also worth adding that research agencies may now be in a better
position to recognize the Babel of incompatible reasoning systems and
symbolic computation systems that have evolved from a plethora of
small projects without much attention to collaboration. Then perhaps
they can work towards encouraging collaboration, to minimize the lack
of interoperability due to diversity of theorem-statement languages,
proof languages, programming languages, computing platforms, quality,
and so on.
-
-
Objection 6: QED is too expensive.
Reply to Objection 6:
While this objection requires careful study at
some point, we note that simply concentrating the efforts of some
currently-funded projects could go a long way towards getting QED off
the ground. Moreover, as noted above, students could contribute to
the project as an integrated part of their studies once the framework
is established, presumably at little or no cost. We can imagine a
number of professionals contributing as well. In particular, there is
currently a large body of tenured or retired mathematicians who have
little inclination for advanced research, and we believe that some of
these could be inspired to contribute to this project. It may be a
good idea to have a QED governing board to recognize contributions.
-
-
Objection 7:
Good mathematicians will never agree to work with formal
systems because they are syntactically so constricting as to be
inconsistent with creativity.
Reply to Objection 7: The written body of formal logic rightly
repulses most mathematical readers. Whitehead and Russell's Principia
Mathematica did not establish mathematics in a notation that others
happily adopted. The traditional definition of formal logics is in a
form that no one can stand to use in practice, e.g., with function
symbols named f1 , f2 , f3 , ...
The absence of definitional principles
for almost all formal logics is an indication that from the
beginning, formal logics became something to be studied (for
properties such as completeness) rather than to be used by humans, the
practical visions of Leibniz and Frege notwithstanding. The
developers of proof checking and theorem-proving systems have done
little towards making their syntax tolerable to mathematicians. Yet,
on this matter of syntax, there is room for the greatest hope.
Although the subject of mechanical theorem-proving in general is beset
with intractable or unsolvable problems, a vastly improved
computer-human interface for mathematics is something easily within
the grasp of current computer theory and technology. The work of
Knuth on and the widespread adoption of by mathematicians and
mathematics journals demonstrates that it is no problem for computers
to deal with any known mathematical notation. Certainly, there is
hard work to be done on this problem, but it is also certainly within
the capacity of computer science to arrange for any rigorously
definable syntax to be something that can be conveniently entered into
computers, translated automatically into a suitable internal notation
for formal purposes, and later reproduced in a form pleasant to
humans. It is certainly feasible to arrange for the users of the QED
system to be able to shift their syntax as often as they please to any
new syntax, provided only that it is clear and unambiguous. Perhaps
the major obstacle here is simply the current scientific reward
system: precisely because new syntaxes, new parsers, and new
formatters are so easy to design, little or no credit (research,
academic, or financial) is currently available for working on this
topic. Let us add that we need take no position on the question
whether mathematicians can or should profit from the use of formal
notations in the discovery of serious, deep mathematics. The QED
system will be mainly useful in the final stages of proof reporting,
similar to writing proofs up in journals, and perhaps possibly never
in the discovery of new insights associated with deep results.
-
-
Objection 8: The QED system will be so large that it is inevitable
that there will be mistakes in its structure, and the QED system will,
therefore, be unreliable.
Reply to Objection 8:
There is no doubt considerable room for error
in the construction of the QED system, as in any human enterprise. A
key motivation in Babbage's development of the computer was his
objective of producing mathematical tables that had fewer errors than
those produced by hand methods, an objective that has certainly been
achieved. It is our experience that even with the primitive proof
checking systems of today, errors made by humans are frequently found
by the use of such tools, errors that would perhaps not otherwise be
caught. The standard of success or failure of the QED project will
not be whether it helps us to reach the kingdom of perfection, an
unobtainable goal, but whether it permits us to construct proofs
substantially more accurately than we can with current hand methods.
In defense of the QED vision, let us assert that we believe that room
for error can be radically reduced by (a) expressing the full
foundation of the QED system in a few pages of mathematics and (b)
supporting the development of essentially independent implementations
for the basic checker. It goes without saying that in the development
of any particular subfield of mathematics, errors in the statements of
definitions and other axioms are possible. Agreement by experts in
each mathematical subfield that the definitions are `right' will be a
necessary part of establishing confidence that mechanically checked
theorems establish what is intended. There is no mechanical method
for guaranteeing that a logical formula says what a user intuitively
means.
-
-
Objection 9: The cooperation of mathematicians is essential to
building the QED edifice of proofs. However, because it is likely to
remain very tedious to prove theorems formally with mechanical proof
checkers for the forseeable future, mathematicians will have no
incentive to help.
Reply to Objection 9:
To be developed, QED does not need to attract
the support of all or most mathematicians. If only a tenth of one
percent of mathematicians could be attracted, that will probably be
sufficient. And in compensation for the extra work currently
associated with entering formal mathematics in proof checking systems,
we can point out that some mathematicians may find the following
benefit sufficiently compensatory: in formally expressing mathematics,
one's own thoughts are often sharply clarified. One often achieves an
appreciation for subtle points in proofs that one might otherwise skim
over or skip. And the sheer joy of getting all the details of a hard
theorem `exactly right', because formalized and machine checked, is
great for many individuals. So we conjecture that enough
mathematicians will be attracted to the endeavor provided it can be
sufficiently organized to have a real chance of success.
-
-
Objection 10:
The QED project represents an unreasonable diversion of
resources to the pursuit of the checking of ordinary mathematics when there is
so much profitably to be done in support of the verification of hardware and
software.
Reply to Objection 10:
Current efforts in formal, mechanical hardware and
software verification are exceptionally introspective, focusing upon internal
matters such as compilers, operating systems, networks, multipliers, and
busses. From a mathematical point of view, essentially all these verifications
fall into a tiny, minor corner of elementary number theory. But eventually,
verification must reach out to consider the intended effect of computing
systems upon the external, continuous world with which they interact. If one
attempts to try to verify the use of a DSP chip for such potentially safety
critical applications as telecommunications, robot vision, speech synthesis, or
cat scanning, one immediately sees the need for such basic engineering
mathematics as Fourier transforms, not something at which existing verification
systems are yet much good. By including the rigorous development of the
mathematics used in engineering, the QED project will make a crucial
contribution to the advance of the verification of computing systems.
-
-
Objection 11: The notion that interesting mathematics can ever, in
practice, be formally checked is a fantasy. Whitehead and Russell
spent hundreds of pages to prove something as trivial as that 0 is not 1.
The notion that computing systems can be verified is another
fantasy, based upon the misconception that mathematical proof can
guarantee properties of physical devices.
Reply to Objection 11: That many interesting, well-known results in
mathematics can be checked by machine is manifest to those who take
the trouble to read the literature. One can mention merely as
examples of mathematics mechanically checked from first principles:
Landau's book on the foundations of analysis, Girard's paradox,
Rolle's theorem, both Banach's and Knaster's fixed point theorems,
the mean value theorem for derivatives and integrals over Banach-space
valued functions, the fundamental counting theorem for groups, the
Schroeder-Bernstein theorem, the Picard-Lindelof theorem for the
existence of ODEs, Wilson's theorem, Fermat's little theorem, the law
of quadratic reciprocity, Ramsey's theorem, Godel's incompleteness
theorem, and the Church-Rosser theorem. That it is possible to verify
mechanically a simple, general purpose microprocessor from the level
of gates and registers up through an application, via a verified
compiler, has been demonstrated. So there is no argument
against proof-checking or mechanical verification in principle, only
an ongoing and important engineering debate about cost-effectiveness.
The noisy verification debate is largely a comedy of misunderstanding.
In reaction to a perceived sanctimony of some verification
enthusiasts, some opponents impute to all enthusiasts grandiose claims
that complete satisfaction with a computing product can be established
by mathematical means. But any verification enthusiast ought to admit
that, at best, verification establishes a consistency between one
mathematical theory and another, e.g., between a formal specification
of intended behavior of a system and a formal representation of an
implementation, say in terms of gates and memory. Mathematical proof
can establish neither that a specification is what any user `really
wants' nor that a description of gates and memory corresponds to
physical reality. So whether the results of a computation will be
pleasing to or good for humans is something that cannot be formally
stated, much less proved.
created 31/12/95 modified 13/1/96