1. What Is the QED Project and Why Is It Important?QED is the very tentative title of a project to build a computer system that effectively represents all important mathematical knowledge and techniques. The QED system will conform to the highest standards of mathematical rigor, including the use of strict formality in the internal representation of knowledge and the use of mechanical methods to check proofs of the correctness of all entries in the system.
The QED Manifesto May 15, 1994
See also:
I have only recently been exposed to the QED project. My training in formal systems consists of a few undergraduate courses in logic, automata theory, topology, and symbolic computation, plus independent study of books like Hofstadter's G.E.B. and various papers available on the internet.
As much as I enjoy studying formal systems, I make my living an an engineer deploying ordinary broken technology. Anybody have a copy of Dijstra's "A Discipline of Programming" handy? There's a blurb in the back called "Sad Note" that would make a perfect quote here. Ah! Thanks to Olle Jarnefors, here it is:
Sad RemarkSince then we have witnessed the proliferation of baroque, ill-defined and, therefore, unstable software systems. Instead of working with a formal tool, which their task requires, many programmers now live in limbo of folklore, in a vague and slippery world, in which they are never quite sure what the system will do to their programs. Under such regretful circumstances the whole notion of a correct program -- let alone a program that has been proven to be correct -- becomes void. What the proliferation of such systems has done to the morale of the computing community is more than I can describe.
Building complex systems on top of poorly specified technology is the bane of my existence. I see QED as a way to "spread the word" about formal systems and their impact on quality.
And I am something of an expert in the theory and practice of the emgerging phenomenon known as the World-Wide Web. I think that the World-Wide Web might be just the vehicle to deploy QED.
I read recently (foo! can't find a reference) that there is evidence that the more members of a community are familiar with a base of knowledge, the easier it is to teach individuals in the community that knowledge. I don't recall the explanation -- perhaps the old "osmosis" joke isn't such a joke after all.
In any case, it is my hope that deploying the QED knowledge base over WWW and similar technologies will lead to broader understanding and usage of formal systems not just in science, but in engineering, and perhaps education, law, and business.
But first, let's explore some of the design issues of QED, as I understand them. I'm afraid my understanding of a lot of this stuff is somewhat shallow. I hope that folks will clarify some of this stuff for me.
The whole point of a formal system is to reduce complex notions in terms of simple notions. Any proof, no matter how formal and detailed, rests on some system of axioms and rules of inference.
On the one hand, it would appear that any proof in formal system X could be translated to formal system Y: first, prove that each of the axioms of system Y is a theorem in X; then, prove that each theorem derived from an inference rule in Y is a theorem in X.
But this is not the case in theory nor in practice. Gödel's theorem says that there are undecidable propositions in any formal system. It turns out that the undecidable propositions follow from the axioms and inference rules, so that a theorem in one system may not be a theorem at all in another system. Hmmm.. does this turn out to be an issue in practice, or are the undecidable propositions in, for example, HOL largely the same as those in Nqthm?
More likely, the formula may be a theorem in both systems, but the proof of the system in X may not be a valid proof in Y because Y's inference rules are weaker than (or just different from) X's.
But most importantly, the cost of translating theorems between systems, plus the cost of proving that these tranlations are correct, along with the cost of documenting and supporting multiple logics runs counter to the goal of sharing proofs.
So it turns out to be quite important to share a common ground.
One popular maxim states that any specification that won't fit on one page is too complicated and will be misunderstood. Toward that end, the constructionistic school of thought argues that the system should be built from a simple system of just a few symbols -- primitive recursive arithmetic (PRA), for example.
Experience with Nqthm suggests that such a system should be powerful to support "diagonal" techniques analagous to Gödel numbering which would allow new proof techniques and inference rules to be "compiled" or "bootstrapped" into the system. This allows so called metamathematical arguments to be represented in the formalism. I may be missing some subtleties here.
The little theories school of thought says that it's not so important that all proofs share the same ground system. The important part is that the proof is sound, i.e. that the conclusions follow from the premises. So a proof begins not with a primitive logic, but by selecting well known "little theories" such as the group theory axioms, or the 13 postulates of real analysis, or the definition of a topology.
Care must be taken to ensure that using theories together in this way doesn't compromise the soundness of the system ( I believe Larch and similar systems (resolution based systems?) do address this issue), and it's not clear that the little theories strategy allows for diagonal techniques. But it does seem to be a more natural way of doing mathematics. How does the intuitionistic school of thought relate?
Another strategy altogether is to start with higher order logic in the system. This strategy trades simplicity and comprehensibility of the ground logic for powerful expressive capability. I gather that metamathematical arguments can be expressed without need for diagonal techniques in a system built on higher order logic.
These are terms that are significant to the history of this project and of formal systems.
While the notions are convenient and powerful, they must be used carefully to avoid paradoxes, like Russell's paradox:
Let A be the set of all sets that are not members of themselves. Is A a member of A or not?