Delivery-Date: 
Date: Wed, 25 May 94 17:46:35 -0600
From: Randall Holmes <holmes@diamond.idbsu.edu>
To: boyer@cli.com, hagiya@is.s.u-tokyo.ac.jp
Subject: Re: Notes
Cc: Chet.Murthy@inria.fr, John.Harrison@cl.cam.ac.uk, 
    TRYBULEC%PLBIAL11.BITNET@anlvm.ctd.anl.gov, Toby.Walsh@loria.fr, 
    beeson@cats.ucsc.edu, bill@ora.on.ca, 
    hilbert!dahn@compu735.mathematik.hu-berlin.de, holmes@diamond.idbsu.edu, 
    jackson@cs.cornell.edu, jt@linus.mitre.org, kunen@cs.wisc.edu, 
    lusk@mcs.anl.gov, mccune@mcs.anl.gov, overbeek@mcs.anl.gov, 
    piotr@cs.ualberta.ca, qed@mcs.anl.gov, staples@cs.uq.oz.au, 
    uribe@cs.stanford.edu, wachter@itd.nrl.navy.mil, waldinge@ai.sri.com, 
    wos@mcs.anl.gov
Message-ID: <"swan.cl.cam.:096910:940525235337"@cl.cam.ac.uk>

Dear Dr. Boyer (and QED list),

My notes on the QED workshop follow.

					--Randall Holmes

Institutional: QED should be a standards body.  It needs to provide a
standard low-level language for theorems and proofs (PRA) for which a
proof checker can easily be written.  It needs to provide a standard
"object language" reflecting current mathematical practice, although
it should allow for the evolution of dialects of the standard object
language and (politically important!) coexistence with alien object
languages (constructive systems, for example).

If a single object language were wanted, I would suggest constructive
type theory, with a "filter" (the double negation interpretation)
provided so that it would look like classical type theory, which is
not far from standard mathematical practice.

Another candidate for an object language: Mac Lane set theory (Z with
delta-zero comprehension (all quantifiers bounded) -- equivalent to
ZFC with all quantifiers bounded in comprehension and replacement.
equivalent in strength to the theory of types and adequate for
classical math short of higher set theory).  Constructive Mac Lane set
theory with filter?

It also needs to maintain the database itself and standards for the
user interface.  My feeling is that a "pyramid" (a grand edifice) is
not necessary; promulgate standards for local databases to be plugged
into a network?  I believe that if the standards body exists and does
its job, and the existing automated reasoning projects "plug in", the
growth of the database will take care of itself!

a slogan in the margin of my copy of the Manifesto:  guerilla QED.

The user interface requires the development of a high-level language
(something that looks rather like natural language; it would be nice
if its structure were designed so that it could be converted
painlessly from stilted formal English to stilted formal French,
German, Chinese, etc. without meddling with its fundamental structure)
in which naive users (including computer naive mathematicians and
mathematically naive computer scientists) could talk to the system,
read theorems and proofs and enter theorems and proofs into the system
without knowing very much about the underlying system.

Also include facilities for graphing and the use of diagrams.

The user should proceed through the following layers in encountering
the system:

Library of results, couched in high-level language and standard math
notation, organized sensibly by field with references to related
results.

Libary of proofs; from each theorem there should be the opportunity to
look at its proof at different levels of complexity.  The decision as
to how much to display at each level should be largely under human
control but it might be somewhat subject to automation?

Interaction with theorem provers:  A naive user should be able to
encounter a prover superficially (talking in high-level language);
he should be able to enter a tutorial which will teach him to be a
sophisticated user.

Submission of results: it should be possible to submit results proven
on the system to "editors" at various levels, from high school and
hobbyist projects through master's level development of existing
theories not yet implemented through genuine new research results.

The meta-logic equivalent to PRA: I suggest that it should be a
predicative type theory with a theory of syntactical objects at the
base (theory of syntactical objects = roughly a theory of finite tree
structures).  I have promised details in the relatively near future.
It should be in effect a programming language (with polymorphism in
the type system) as well as a logical theory; this will facilitate the
"bootstrapping" of results about proofs in "PRA" to procedures
allowing the skipping of many steps in later proofs in "PRA"
(verification of derived inference rules by reflection).  A version of
the proof checker can be written in the algorithmic part of the
theory.

It should be a meta-logic but also should be interpretable in most
object languages!  (allowing further reflection? -- what about object
languages strong enough to prove stronger meta theorems than PRA can
prove; should such an object language be allowed to prove metatheorems
for its own consumption?)

Mizar may be considered a trial run of part of QED; it has the
high-level language and the proof checker in preliminary versions.  It
lacks powerful automated reasoning techniques and the sophisticated
low-level language with reflection projected for QED.  Mizar does
operate on proof objects, apparently!

The Mizar logic is weak (first-order logic) but augmented with axioms
of a powerful set theory (which could be weakened or replaced with
something else; could the base logic be made constructive?).  The
logic is structured analogously to the way papers are written.

Aside:  a standard _linear_ notation for communicating math in ASCII
files might be an outgrowth of QED!

There was dispute about the amount of "blow-up" which would occur in
translating proofs between existing prover projects; I think that a
"dumb" approach working mechanically through the root logic would be
bad, but that a heuristic approach using known common features of
particular pairs of theories might make proof translations feasible.


QED should include a software library, considering part of the market.
QED software should include specifications and proofs of verification
of specifications where possible.  My comments on the meta-logic
suggest that it might include a standard pseudo-code for expressing
algorithms?

The QED user interface should be usable at a level where educational
applications are possible (down to high school, perhaps?)

The existence of the core of QED will promote its growth.  As Mizar
has already done, it will provide a formal context for doing Master's
theses.  People educated using QED at all levels will be more inclined
to use formal methods when faced with math and C.S. problems.

The project which Boyer has suggested of rebuilding 19th century math
will dictate the development of a standard object language
(ZFC-based?) reflecting the common experience of non-computer-oriented
mathematicians. 

The issue of recognition of QED work at all levels:  do this at all
levels at once.  Master's projects build established areas, research
effort for original results in areas where this is fruitful,
acknowledge efforts of students and/or hobbyists at lower levels.

To start up, bilateral projects.  My favorite idea is collaboration
between HOL (probably closest to standard object language of the
prover projects) and Mizar (closest to the QED core of any project).
Boyer-Moore seems to be a prototype tool for working with the very low
level of the core missing from Mizar.  A three-tier project?

Another project: a translation from one prover project down through
Mizar and up through Mizar to another prover project and vice versa;
set up bilateral communication.

Current incompatibilities will probably not arise again if project
takes off; future prover projects will take QED interface into account
at the outset.

Theories which do not produce proof objects need to produce proof
objects.