QED.html 10.5 KB

Raw Blame History Permalink

<!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&amp;what=web&amp;fmt=.&amp;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&ouml;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&ouml;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 &amp; Whitehead
      <DD>
	One of the first efforts to exhaustively and formally codify mathematics.
      <DT>
	G&ouml;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&ouml;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>