You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
260 lines
10 KiB
260 lines
10 KiB
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN//2.0">
|
|
<HTML>
|
|
<HEAD>
|
|
<TITLE>Learning about QED</TITLE>
|
|
</HEAD>
|
|
<BODY>
|
|
<H1>
|
|
A Survey of QED and Related Topics
|
|
</H1>
|
|
<ADDRESS>
|
|
<A href="http://www.hal.com/~connolly">Daniel W. Connolly</A><BR>
|
|
updated $Date: 1998/05/21 20:30:59 $, created 10 Oct 1994
|
|
</ADDRESS>
|
|
<H2>
|
|
What is QED?
|
|
</H2>
|
|
<BLOCKQUOTE>
|
|
<EM>1. What Is the QED Project and Why Is It Important?</EM>
|
|
<P>
|
|
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.
|
|
<ADDRESS>
|
|
<A HREF="ftp://info.mcs.anl.gov/pub/qed/manifesto">The QED Manifesto</A>
|
|
May 15, 1994
|
|
</ADDRESS>
|
|
</BLOCKQUOTE>
|
|
<P>
|
|
See also:
|
|
<UL>
|
|
<LI>
|
|
<A href="ftp://ftp.cli.com/home/boyer/qedmail.Z">archive of QED mailing
|
|
list</A> (200K compressed).
|
|
<LI>
|
|
<A href="http://www.comlab.ox.ac.uk/archive/formal-methods.html">The World-Wide
|
|
Web Virtual Library: Formal Methods</A>
|
|
</UL>
|
|
<H2>
|
|
Observations from a Newcomer
|
|
</H2>
|
|
<P>
|
|
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.
|
|
<P>
|
|
As much as I enjoy studying formal systems, I make my living an an engineer
|
|
deploying ordinary broken technology. <EM>Anybody have a copy of Dijstra's
|
|
<A HREF="http://altavista.digital.com/cgi-bin/query?pg=q&what=web&fmt=.&q=%2Bdijkstra+%2B%22A+Discipline+of+Programming%22">"A
|
|
Discipline of Programming" </A>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:</EM>
|
|
<BLOCKQUOTE>
|
|
Sad Remark
|
|
<P>
|
|
Since 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.
|
|
</BLOCKQUOTE>
|
|
<P>
|
|
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.
|
|
<P>
|
|
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.
|
|
<P>
|
|
I read recently (<EM>foo! can't find a reference</EM>) 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.
|
|
<P>
|
|
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.
|
|
<P>
|
|
But first, let's explore some of the design issues of QED, as I understand
|
|
them. <EM>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.</EM>
|
|
<H3>
|
|
Foundations: What Rests On What?
|
|
</H3>
|
|
<P>
|
|
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.
|
|
<P>
|
|
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.
|
|
<P>
|
|
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 <EM>not</EM> be a theorem at all
|
|
in another system. <EM>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?</EM>
|
|
<P>
|
|
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.
|
|
<P>
|
|
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.
|
|
<P>
|
|
So it turns out to be quite important to share a common ground.
|
|
<H3>
|
|
Constructionist vs. Little Theories vs. Higher Order Logic
|
|
</H3>
|
|
<P>
|
|
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.
|
|
<P>
|
|
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 <EM>metamathematical arguments</EM>
|
|
to be represented in the formalism. <EM>I may be missing some subtleties
|
|
here.</EM>
|
|
<P>
|
|
The <EM>little theories</EM> 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.
|
|
<P>
|
|
Care must be taken to ensure that using theories together in this way doesn't
|
|
compromise the soundness of the system (<EM> I believe Larch and similar
|
|
systems (resolution based systems?) do address this issue</EM>), 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. <EM>How does
|
|
the intuitionistic school of thought relate?</EM>
|
|
<P>
|
|
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.
|
|
<H3>
|
|
Human-Computer Interfaces, Linguistics, and Visualization
|
|
</H3>
|
|
<UL>
|
|
<LI>
|
|
How do we capture all these proofs into the knowledge base? Can they be
|
|
translated from systems like HOL and Mizar? Can we develop software that
|
|
translates proofs from natural languages like English into our formal system?
|
|
<LI>
|
|
How do we deal with constructs like definite description? (e.g. "let x the
|
|
minimum integer in the set.")
|
|
<LI>
|
|
What about mnemonic formulas like F=ma and E=mc^2?
|
|
</UL>
|
|
<H2>
|
|
Automated Reasoning Systems
|
|
</H2>
|
|
<DL>
|
|
<DT>
|
|
<A href="ftp://sail.stanford.edu/pub/clt/ARS/">Database of Automated reaoning
|
|
systems </A>
|
|
<DD>
|
|
by Carolyn Talcott, Computer Science Department, Stanford University, Stanford
|
|
CA 94305, <TT>clt@sail.stanford.edu</TT>
|
|
<DT>
|
|
<A href="http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html">NuPrl</A>
|
|
<DD>
|
|
The documentation and theories of NuPrl have been organized for browsing
|
|
from WWW clients.
|
|
<DT>
|
|
<A href="http://www.comlab.ox.ac.uk/archive/formal-methods.html">The World-Wide
|
|
Web Virtual Library: Formal Methods</A>
|
|
<DD>
|
|
The Formal Methods page references many more systems, including Nqthm and
|
|
HOL.
|
|
<H2>
|
|
Applications
|
|
</H2>
|
|
<UL>
|
|
<LI>
|
|
SRC Research Report 114<BR>
|
|
<CITE><A href="http://www.research.digital.com/SRC/publications/src-rr-114.html">
|
|
Automated Proofs of Object Code for a Widely Used
|
|
Microprocessor</A></CITE><BR>
|
|
Yuan Yu October 5, 1993 122 pages
|
|
</UL>
|
|
<H2>
|
|
History of Formal Systems
|
|
</H2>
|
|
<P>
|
|
These are terms that are significant to the history of this project and of
|
|
formal systems.
|
|
<DL>
|
|
<DT>
|
|
Peano Postulates
|
|
<DD>
|
|
The five axioms that characterize natural numbers, addition, and multiplication.
|
|
Really Old. I dunno how old.
|
|
<DT>
|
|
Euclid's 5 Axioms of plane geometry
|
|
<DD>
|
|
Lots have folks have tried to express one of these in terms of the other
|
|
four. Nobody succeeded -- in fact, I believe it is provably impossible to
|
|
do so. But the effort was not a waste: non-euclidean geometry is in many
|
|
ways more interesting than euclidean...
|
|
<DT>
|
|
ZF
|
|
<DT>
|
|
ZFC
|
|
<DT>
|
|
Zermelo-Fraenkel Set Theory
|
|
<DD>
|
|
I believe this is a term for the informal collection of notions collectively
|
|
known as "set theory" or "classical set theory".
|
|
<P>
|
|
While the notions are convenient and powerful, they must be used carefully
|
|
to avoid paradoxes, like Russell's paradox:
|
|
<P>
|
|
<EM> Let <B>A</B> be the set of all sets that are not members of themselves.
|
|
Is <B>A</B> a member of <B>A</B> or not?</EM>
|
|
<DT>
|
|
<EM>Principia Mathematica</EM>, Russell & Whitehead
|
|
<DD>
|
|
One of the first efforts to exhaustively and formally codify mathematics.
|
|
<DT>
|
|
Gödel's theorem
|
|
<DD>
|
|
<EM>Every formal systems is either incomplete or inconsistent.</EM> This
|
|
theorem guarantees that mathematicians will never be obsolete :-)
|
|
<DT>
|
|
The halting problem
|
|
<DD>
|
|
There is no algorithm that will decide for an arbitrary computer program
|
|
whether that program halts or computes forever. This result is similar to
|
|
Gös theorem, which could be restated as "There is no algorithm to decide
|
|
whether an arbitrary formula represents a theorem."
|
|
<DT>
|
|
Bourbaki
|
|
<DD>
|
|
Another effort to codify mathematics.
|
|
</DL>
|
|
</DL>
|
|
</BODY></HTML>
|