From qedowner Mon Apr 12 17:38:34 1993
Received: by antares.mcs.anl.gov id AA25256
(5.65c/IDA1.4.4 for qedoutgoing); Mon, 12 Apr 1993 17:23:22 0500
Received: from donner.mcs.anl.gov by antares.mcs.anl.gov with SMTP id AA25248
(5.65c/IDA1.4.4 for ); Mon, 12 Apr 1993 17:23:20 0500
MessageId: <199304122223.AA25248@antares.mcs.anl.gov>
To: qed@mcs.anl.gov
Subject: Let's start
Date: Mon, 12 Apr 1993 17:23:19 0500
From: Rusty Lusk
Sender: qedowner
Precedence: bulk
Now that the flurry of signing up has slowed down (139 people are on this
list), perhaps we should start the discussion. Anyone who is still unclear
about what QED is can fetch "The QED Manifesto" by anonymous ftp to
info.mcs.anl.gov. Take the file manifesto from the directory pub/qed. It
is a plain ascii file.
QED is an intriguing idea. Now we (all 139 of us) need suggestions on how to
transform it from an idea into a project. The floor is now open. You can
send to everyone on the mailing list by addressing your mail to
qed@mcs.anl.gov
Regards,
Bob Boyer & Rusty Lusk
P.S. The qed mailing list is being maintained by a program called majordomo,
and a number of services can be accessed by sending mail to
majordomo@mcs.anl.gov
For example, to find out who else is on the list, send
who qed
To delete yourself from the list, send
unsubscribe qed
If you forget almost everything, send
help
From qedowner Tue Apr 13 10:32:49 1993
Received: by antares.mcs.anl.gov id AA11770
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 10:12:41 0500
Received: from saturn.wwc.edu by antares.mcs.anl.gov with SMTP id AA11758
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 10:12:22 0500
Subject: Re: QED, Bourbaki and Mathematica
To: qed@mcs.anl.gov
Date: Tue, 13 Apr 93 8:19:47 PDT
From: Ted Ashton
InReplyTo: ; from "Zdzislaw Meglicki" at Apr 13, 93 1:50 pm
XMailer: ELM [version 2.3 PL11]
MessageId: <9304130819.aa10002@saturn.wwc.edu>
Sender: qedowner
Precedence: bulk
... good stuff deleted ...
> The interface is a very important issue too. The technology nowadays is
> sufficiently advanced to allow mathematicians the use of real
> mathematical notation. It should not be necessary to type "\int" for an
> integral: an appropriate integral icon should be available and draggable
> onto the workspace.
Agreed. Yet let's not forget those of us who find it much faster and more
automatic to type \int. With the technology available, it should be also
possible to create an interface in which everything that can be done by mouse
can also be done by keyboard. It might be worthwhile to store stuff in, say,
TeX format for the benefit of those who want to send copies of stored info to
those who don't have access to qed.
... more good stuff deleted ...
> Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au,
> Automated Reasoning Program  CISR, and Plasma Theory Group  RSPhysS,
> The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601,
> Australia, fax: (Australia)62490747, tel: (Australia)62490158

Ted Ashton (ashted@wwc.edu)
Campus Computer Center (509) 5272307
Walla Walla College
College Place, WA 99324 "The slide rule liveth still."
From qedowner Tue Apr 13 10:45:52 1993
Received: by antares.mcs.anl.gov id AA12105
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 10:25:55 0500
Received: from lutra.mcs.anl.gov by antares.mcs.anl.gov with SMTP id AA12095
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 10:25:53 0500
From: Bill McCune
Received: by lutra.mcs.anl.gov (4.1/GeneV4)
id AA01463; Tue, 13 Apr 93 10:25:52 CDT
Date: Tue, 13 Apr 93 10:25:52 CDT
MessageId: <9304131525.AA01463@lutra.mcs.anl.gov>
To: qed@mcs.anl.gov
Subject: response to Meglicki
Sender: qedowner
Precedence: bulk
(I'm sorry about my previous, misdirected message.)
Zdzislaw Gustav Meglicki writes:
> The three issues mentioned above: knowledge data base, user interface,
> and language seem to me to be quite fundamental to the project.
I hope that there will be many implementations associated with QED,
with different types of knowledge bases, different user interfaces,
and written in different programming languages. Of course there will
have to be (at some level) a common language for formulas, proofs, etc.,
but that seems like a small issue once the base logic is fixed.
It seems to me that the fundamental issues are the goals of the project
and the base logic.
Bill McCune

 William W. McCune  email: mccune@mcs.anl.gov 
 MCS221  phone: (708) 2523065 
 Argonne National Laboratory  FAX: (708) 2525986 
 Argonne, IL 604394844  
 U.S.A.  

Replied: Wed, 14 Apr 1993 12:57:51 0500
Replied: "Gene Rackow "
From qedowner Tue Apr 13 14:48:36 1993
Received: by antares.mcs.anl.gov id AA16001
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 13:38:28 0500
Received: from skeeve.mcs.anl.gov by antares.mcs.anl.gov with SMTP id AA15994
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 13:38:27 0500
From: Gene Rackow
Received: by skeeve.mcs.anl.gov (4.1/GeneV4)
id AA04604; Tue, 13 Apr 93 13:38:26 CDT
Date: Tue, 13 Apr 93 13:38:26 CDT
MessageId: <9304131838.AA04604@skeeve.mcs.anl.gov>
To: qed@mcs.anl.gov
Subject: manifest
Sender: qedowner
Precedence: bulk
For those of you on the list that do not have internet access, I have
added the manifest to the majordomo server. You can now send
a message to "majordomo@mcs.anl.gov" with a body of "manifest qed"
to get the current manifesto file.
Gene
From qedowner Tue Apr 13 15:06:00 1993
Received: by antares.mcs.anl.gov id AA16249
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 13:56:23 0500
Received: from optima.CS.Arizona.EDU by antares.mcs.anl.gov with SMTP id AA16242
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 13:56:21 0500
Received: from leibniz.CS.Arizona.EDU by optima.cs.arizona.edu (5.65c/15) via SMTP
id AA15873; Tue, 13 Apr 1993 11:56:18 MST
Date: Tue, 13 Apr 1993 11:56:17 MST
From: "Richard Schroeppel"
MessageId: <199304131856.AA23651@leibniz.cs.arizona.edu>
Received: by leibniz.cs.arizona.edu; Tue, 13 Apr 1993 11:56:17 MST
To: qed@mcs.anl.gov
Subject: comments
Sender: qedowner
Precedence: bulk
This manifesto should be signed.
You didn't provide any contact information!
I'd suggest posting the "who" list now, and annually.
Could some knowledgable person provide a capsule review of
work already done? No sense starting in a vacuum. There
may be public domain work available that's worth using,
or existing proofs worth converting. If the existing work
is proprietary, perhaps the owners could be persuaded to
donate portions. We need to know what's worked, and what hasn't.
My personal language preferences are (1) editor of your choice for
proof creation, including Emacs & WordPerfect (2) Lisp for turning
that proof into a checkable file (3) C for checking the lowlevel
proof, based on matching character strings. The lowlevel checker
should be simple enough that it can be easily implemented in several
languages, including C & Fortran, and perhaps even assembly code.
(This, on the theory that the less complex software you believe,
the better.) The spec for the checker should be unambiguous, so that
anyone can implement a checker from the spec, and expect it to work.
Ideally, the lowlevel checker is only a few pages of code; it's
required that it be totally understandable in detail by a single person.
The lowlevel data files should be human readable, and include comments
with the highlevel proof. The working character set should be emailable.
Rich Schroeppel rcs@cs.arizona.edu
From qedowner Tue Apr 13 15:24:34 1993
Received: by antares.mcs.anl.gov id AA16520
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 14:15:03 0500
Received: from life.ai.mit.edu by antares.mcs.anl.gov with SMTP id AA16508
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 14:14:58 0500
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI4.10) id AA08247; Tue, 13 Apr 93 15:14:55 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI4.10) id AA00347; Tue, 13 Apr 93 15:14:54 EDT
Date: Tue, 13 Apr 93 15:14:54 EDT
MessageId: <9304131914.AA00347@spock>
To: mccune@mcs.anl.gov
Cc: qed@mcs.anl.gov
InReplyTo: Bill McCune's message of Tue, 13 Apr 93 10:25:52 CDT <9304131525.AA01463@lutra.mcs.anl.gov>
Subject: the base logic
Sender: qedowner
Precedence: bulk
One idea is that we simply collect a library of files of theorems.
Each file would be in some language, such as the BoyerMoore logic,
HOL, nuPRL or Ontic (our language). I am confident that I could write
a simple routine that would translate definitions and theorems from any
of these languages into Ontic. This would make it possible to extend
the machine verified library by building on the work of other groups.
Each group could use whatever tools they like best. Also, the ability
to translate between foundational languages could bypass the need for
a single base logic.
Unfortunately, a multilingual approach would weaken the claim to
correctness  no single monolithic proof would exist for all
theorems in the library. I personally think the reduction in
certainty is worth it, especially in getting the project going in the
short term. Is there a depository somewhere of BoyerMoore, HOL,
and/or nuPRL thoerems? At some point I would like to try translating
existing libraries into Ontic so we can build on them further.
David McAllester
From qedowner Tue Apr 13 15:44:26 1993
Received: by antares.mcs.anl.gov id AA16805
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 14:36:05 0500
Received: from life.ai.mit.edu by antares.mcs.anl.gov with SMTP id AA16793
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 14:36:00 0500
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI4.10) id AA08830; Tue, 13 Apr 93 15:35:55 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI4.10) id AA00351; Tue, 13 Apr 93 15:35:55 EDT
Date: Tue, 13 Apr 93 15:35:55 EDT
MessageId: <9304131935.AA00351@spock>
To: qed@mcs.anl.gov
Subject: a multilingual approach
Sender: qedowner
Precedence: bulk
I should have said that theorems from any group that I did not mention
would, of course, be nice to also have in a repository. I am not
quite sure how I would use the theorems proved by resolution provers
unless they were translated into some foundational language. I'm not
sure how to use first order validities. What kind of mathematical
objects does a particular validity talk about? Figuring this out
automatically from the statement of the validity seems difficult. I
would like libraries to contain statements like "every finite Abelion
group is isomorphic to a product of cyclic subgoups". How would this
be phrased as a first order validity? Given appropriate higher order
definitions this theorem can be formalized more or less as stated.
Of course I can see no objection to collecting libraries of first
order validities, I am just not sure how to use them. Perhaps the
IMPS notion of a "little theory" is relevant here. A little theory is
a signature, a set of axioms, and a set of consequences. I probably
could translate any IMPS theory directly into a set of Ontic theorems.
(Please let me know if I have misrepresented IMPS).
David McAllester
From qedowner Tue Apr 13 17:25:32 1993
Received: by antares.mcs.anl.gov id AA18968
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 16:10:54 0500
Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA18961
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 16:10:51 0500
Received: from circe.mitre.org by linus.mitre.org (5.61/RCF4S)
id AA12832; Tue, 13 Apr 93 17:10:49 0400
PostedDate: Tue, 13 Apr 93 17:10:38 0400
Received: by circe.mitre.org (5.61/RCF4C)
id AA10474; Tue, 13 Apr 93 17:10:40 0400
MessageId: <9304132110.AA10474@circe.mitre.org>
To: dam@ai.mit.edu (David McAllester)
Cc: qed@mcs.anl.gov
Subject: Re: a multilingual approach
InReplyTo: Your message of "Tue, 13 Apr 93 15:35:55 EDT."
<9304131935.AA00351@spock>
XPostalAddress: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730
XTelephoneNumber: 617 271 2654; Fax 617 271 3816
Date: Tue, 13 Apr 93 17:10:38 0400
From: guttman@linus.mitre.org
Sender: qedowner
Precedence: bulk
> From: dam@ai.mit.edu (David McAllester)
> Subject: a multilingual approach
[paragraph deleted]
> Of course I can see no objection to collecting libraries of first
> order validities, I am just not sure how to use them. Perhaps the
> IMPS notion of a "little theory" is relevant here. A little theory is
> a signature, a set of axioms, and a set of consequences. I probably
> could translate any IMPS theory directly into a set of Ontic theorems.
I think one of the advantages of the little theories version of the
axiomatic method is this: The little theory is a natural unit for
interchanging results. By organizing mathematics into a network of
relatively fine theories, it lets us see exactly what assumptions we
must discharge to justify using a particular group of theorems in a
different framework.
Josh
From qedowner Tue Apr 13 18:14:00 1993
Received: by antares.mcs.anl.gov id AA19649
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 16:40:41 0500
Received: from swan.cl.cam.ac.uk by antares.mcs.anl.gov with SMTP id AA19641
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 16:40:35 0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP6.4) to cl; Tue, 13 Apr 1993 22:40:29 +0100
To: QED
Subject: Formalizability as a Criterion for Mathematical Rigour
Date: Tue, 13 Apr 93 22:40:18 +0100
From: John Harrison
MessageId: <"swan.cl.ca.893:13.04.93.21.40.32"@cl.cam.ac.uk>
Sender: qedowner
Precedence: bulk
The influence of Bourbaki on the accepted structure of mathematics surely goes
beyond a few bits of arcane terminology like "quasicompact", and has
substantially altered the emphasis placed on certain areas, e.g. uniform spaces
and filters. I suggest that a project of formalization like QED might effect
similar changes.
If certain areas seem hard to formalize in the QED system, it may not point to
a flaw in QED (whatever it turns out to be), but rather indicate that the
mathematical notions concerned have not been established with sufficient rigour
and clarity, and should be redeveloped in a careful way, or subsumed in a more
abstract, and therefore simpler, theory. (Perhaps the development of algebraic
geometry this century is a good example.) It is a commonplace in Computer
Science that formal semantics of programming languages should be used in
language design, e.g.
"The hitch is that defining a language a posteriori, i.e. after its
design has been frozen by the existence of implementations and users,
can hardly improve it. To create a good programming language,
semantics must be used a priori, as a design tool that embodies and
extends the intuitive notion of uniformity."
(John C. Reynolds in [2])
Is it stretching an analogy too far to hope for a similar attitude to the
formalization of mathematics?
Of course this is not to deny that a dogmatic faith in a particular
foundational system is much worse than a dogmatic faith in existing
mathematics. Indeed, various foundational programmes have had to modify their
original goals a little in order to formalize actual mathematics. For example,
the logicists Russell and Whitehead stretched the notion of `logical' to
incorporate the Axiom of Infinity; the formalist Gentzen stretched the concept
of `finitary' to attain a consistency proof for arithmetic. Intuitionists
tended to be less flexible, but they were intent not on codifying existing
mathematics, but with creating a new mathematics.
John Harrison (jrh@cl.cam.ac.uk)
P.S. Since the name Bourbaki is bandied about a lot here, I thought I'd point
out an interesting article by Adrian Mathias [1] criticizing their attitude to
logical and set theoretic foundations (as distinct from their development of
mathematical structures).
[1] A. Mathias, "The Ignorance of Bourbaki".
Math. Intelligencer, a few years ago.
[2] R. D. Tennant, "Semantics of Programming Languages".
Prentice Hall International Series in Computer Science 1991.
From qedowner Tue Apr 13 20:40:50 1993
Received: by antares.mcs.anl.gov id AA21469
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 18:56:09 0500
Received: from panther.cs.uidaho.edu by antares.mcs.anl.gov with SMTP id AA21462
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 18:56:05 0500
Received: from localhost by panther.cs.uidaho.edu with SMTP id AA02373
(5.65c/IDA1.4.4 for qed@mcs.anl.gov); Tue, 13 Apr 1993 17:06:22 0700
MessageId: <199304140006.AA02373@panther.cs.uidaho.edu>
To: qed@mcs.anl.gov
Cc: guttman@linus.mitre.org
Subject: Re: a multilingual approach
InReplyTo: Your message of Tue, 13 Apr 93 17:10:38 0400.
<9304132110.AA10474@circe.mitre.org>
Date: Tue, 13 Apr 93 17:06:21 0700
From: "Phil Windley"
XMts: smtp
Sender: qedowner
Precedence: bulk
On Tue, 13 Apr 93 17:10:38 EDT, guttman@linus.mitre.org wrote:
+
 > From: dam@ai.mit.edu (David McAllester)
 > Subject: a multilingual approach

 [paragraph deleted]

 > Of course I can see no objection to collecting libraries of first
 > order validities, I am just not sure how to use them. Perhaps the
 > IMPS notion of a "little theory" is relevant here. A little theory is
 > a signature, a set of axioms, and a set of consequences. I probably
 > could translate any IMPS theory directly into a set of Ontic theorems.

 I think one of the advantages of the little theories version of the
 axiomatic method is this: The little theory is a natural unit for
 interchanging results. By organizing mathematics into a network of
 relatively fine theories, it lets us see exactly what assumptions we
 must discharge to justify using a particular group of theorems in a
 different framework.
Josh,
Just to clear up a few definitions, please review for us what you mean by
"little theories." Are these the same as parametrized modules (PVS, EHDM,
OBJ3), abstract theories (HOL), and others whoch I'm not as familiar with,
but seem similar?
I suspect that one problem that we're all going to have is language; not
the object language of the theorem provers, but English.
phil
Phillip J. Windley, Asst. Professor  windley@cs.uidaho.edu
Laboratory for Applied Logic  windley@panther.cs.uidaho.edu
Department of Computer Science 
University of Idaho  Phone: 208.885.6501
Moscow, ID 83843  Fax: 208.885.6645
From qedowner Tue Apr 13 20:45:44 1993
Received: by antares.mcs.anl.gov id AA21541
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 19:01:52 0500
Received: from arp.anu.edu.au by antares.mcs.anl.gov with SMTP id AA21533
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 19:01:44 0500
Received: by arp.anu.edu.au id AA14285
(5.65c/IDA1.4.2.9 for qed@mcs.anl.gov); Wed, 14 Apr 1993 10:01:35 +1000
Received: from Messages.7.15.N.CUILIB.3.45.SNAP.NOT.LINKED.arp.anu.edu.au.sun4.41
via MS.5.6.arp.anu.edu.au.sun4_41;
Wed, 14 Apr 1993 10:01:34 +1000 (EST)
MessageId:
Date: Wed, 14 Apr 1993 10:01:34 +1000 (EST)
From: Zdzislaw Meglicki
To: qed@mcs.anl.gov
Subject: goals and the base logic
Sender: qedowner
Precedence: bulk
Bill McCune writes:
> I hope that there will be many implementations associated with QED,
> with different types of knowledge bases, different user interfaces,
> and written in different programming languages. Of course there will
> have to be (at some level) a common language for formulas, proofs, etc.,
> but that seems like a small issue once the base logic is fixed.
> It seems to me that the fundamental issues are the goals of the project
> and the base logic.
The impression I got from reading the "Manifesto" was that the goal of
the QED would be to undertake a Bourbaki like project using computer
reasoning as its basis. If that is the case then, I would expect, some
kind of a uniform approach both with respect to the tools and basic
logic should emerge. The beauty of Bourbaki is that such a unified
approach as to the basic logic (set theory) and methodology was agreed
upon and used methodically by all participants of the project. This
resulted in quite a monumental work which had a great impact on XXth
century mathematics. Would anything less than that be worth doing?
Although I may be quite mistaken here, I think that unless real
mathematicians are attracted to QED and begin to use it for their normal
work, the project will be doomed. Hence the need to come up with user
environments, basic logic, and programming language which would be
acceptable to that end user, i.e., the mathematician. Likewise, the need
to develop a unified approach. To have a collage of various systems,
various logics, various languages would hardly be any different from
what we already have today. Why call it QED?
Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au,
Automated Reasoning Program  CISR, and Plasma Theory Group  RSPhysS,
The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601,
Australia, fax: (Australia)62490747, tel: (Australia)62490158
From qedowner Tue Apr 13 23:20:50 1993
Received: by antares.mcs.anl.gov id AA23617
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 21:36:14 0500
Received: from xenon.csl.sri.com by antares.mcs.anl.gov with SMTP id AA23610
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 21:36:12 0500
Received: by xenon.csl.sri.com id AA08110
(5.65b/IDA1.4.3 for qed@mcs.anl.gov); Tue, 13 Apr 93 19:36:19 0700
Date: Tue, 13 Apr 93 19:36:19 0700
From: Pat Lincoln
MessageId: <9304140236.AA08110@xenon.csl.sri.com>
To: qed@mcs.anl.gov
InReplyTo: David McAllester's message of Tue, 13 Apr 93 15:14:54 EDT <9304131914.AA00347@spock>
Subject: the base logic
Sender: qedowner
Precedence: bulk
> From: dam@ai.mit.edu (David McAllester)
> ...I am confident that I could write
> a simple routine that would translate definitions and theorems from any
> of these languages into Ontic.
> ...Also, the ability
> to translate between foundational languages could bypass the need for
> a single base logic.
Something that should be considered with regard to this approach is
the difficulty of translating proofs between dissimilar systems.
Difficult theorems and their proofs in some theory could be encoded so
that "THEOREM is proved by PROOF in THEORY" is a (relatively) easily
checked theorem of the base logic of QED, as the manifesto suggests
for nonconstructive set theory. This `one level removed' approach
does move the problem of translation between systems into a more
formal arena, but it doesn't really finesse the problem of translating
proofs since it requires writing a proof checker for each theory in
QED. It also suggests a paradigm of interaction where one proves
their theorems in Ontic, PVS, Otter, BMTP, etc, in the usual way, and
then translates the completed proof, theorem, and theory into QED for
a kind of validation. Some social process must check the translation
as well as the QED proof checker. Such a use of QED makes the choice
of base logic less important since end users never need peek under the
hood of their axiom system (at the translation of those axioms into
QED base logic). However, this approach seems less exciting than what
the Manifesto describes, and is not as bootstrappable as the direct
method David suggests.
Patrick Lincoln
From qedowner Wed Apr 14 00:01:03 1993
Received: by antares.mcs.anl.gov id AA24106
(5.65c/IDA1.4.4 for qedoutgoing); Tue, 13 Apr 1993 22:17:06 0500
Received: from cli.com by antares.mcs.anl.gov with SMTP id AA24098
(5.65c/IDA1.4.4 for ); Tue, 13 Apr 1993 22:17:03 0500
Received: by CLI.COM (4.1/1); Tue, 13 Apr 93 22:11:58 CDT
Date: Tue, 13 Apr 93 22:16:48 CDT
From: Robert S. Boyer
MessageId: <9304140316.AA08792@axiom.CLI.COM>
Received: by axiom.CLI.COM (4.1/CLI1.2)
id AA08792; Tue, 13 Apr 93 22:16:48 CDT
To: qed@mcs.anl.gov
Subject: references
ReplyTo: boyer@CLI.COM
Sender: qedowner
Precedence: bulk
I think that there is a pretty diverse group of people listening, so
when things like named computer systems that not everyone can be
expected to know about are first mentioned, a few pointers to the
literature or a few helpful definitions might be worth including. I
do hope that the diversity of the group continues to grow, especially
in the direction of including more mathematicians.
Bob
From qedowner Wed Apr 14 05:42:39 1993
Received: by antares.mcs.anl.gov id AA28787
(5.65c/IDA1.4.4 for qedoutgoing); Wed, 14 Apr 1993 04:04:54 0500
Received: from ice.ge.cnr.it by antares.mcs.anl.gov with SMTP id AA28778
(5.65c/IDA1.4.4 for ); Wed, 14 Apr 1993 04:04:26 0500
Received: from DECNETMAIL by ICE.GE.CNR.IT with PMDF#10000; Wed, 14 Apr 1993
11:02 MET
Date: Wed, 14 Apr 1993 11:02 MET
From: FORSTER@matgen.ge.cnr.it
Subject: Bourbaki/Mathias
To: qed@mcs.anl.gov
MessageId: <3CC0F1D94020052D@ICE.GE.CNR.IT>
XEnvelopeTo: qed@mcs.anl.gov
XVmsTo: ICE622::IN%"qed@mcs.anl.gov"
Sender: qedowner
Precedence: bulk
I'm glad john mentioned Mathias' article. It occurred to me as soon as i
started shuffling thru' the avalanche of QED stuff i found in my mailbox
this morning. It should be read as a warning, and is in any case full
of useful historical information you are unlikely to find anywhere else.
There is probably electronic copy floating around Cambridge somewhere.
If anyone wants one, they could try emailing ardm@sun1.mfo.unifreiburg.de
or if that fails send me a massage at pmms.cam.ac.uk (the address in this
header is inoperative from this afternoon) and i will try to put it in
some anonymous ftp domain.
Thomas Forster
From qedowner Wed Apr 14 06:45:37 1993
Received: by antares.mcs.anl.gov id AA00644
(5.65c/IDA1.4.4 for qedoutgoing); Wed, 14 Apr 1993 06:25:58 0500
Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA00637
(5.65c/IDA1.4.4 for ); Wed, 14 Apr 1993 06:25:55 0500
Received: from circe.mitre.org by linus.mitre.org (5.61/RCF4S)
id AA18447; Wed, 14 Apr 93 07:25:53 0400
PostedDate: Wed, 14 Apr 93 07:25:50 0400
Received: by circe.mitre.org (5.61/RCF4C)
id AA10713; Wed, 14 Apr 93 07:25:51 0400
MessageId: <9304141125.AA10713@circe.mitre.org>
To: qed@mcs.anl.gov
Cc: guttman@linus.mitre.org, farmer@linus.mitre.org, jt@linus.mitre.org
Subject: Re: a multilingual approach
InReplyTo: Your message of "Tue, 13 Apr 93 17:10:38 EDT."
<9304132110.AA10474@circe.mitre.org>
XPostalAddress: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730
XTelephoneNumber: 617 271 2654; Fax 617 271 3816
Date: Wed, 14 Apr 93 07:25:50 0400
From: guttman@linus.mitre.org
Sender: qedowner
Precedence: bulk
In my last message I mentioned IMPS and the "little theories" version
of the axiomatic method, but without explaining what I meant.
IMPS, an Interactive Mathematical Proof System, is an interactive
theorem prover intended for proofs in mathematics and software
assurance. It uses a simple type theory with partial functions (such
as division, undefined for 0 denominator) and subtypes (the integers
are a subtype of the reals, for instance). We have used IMPS to prove
a substantial collection of theorems including foundations of
analysis, some group theory, and various other areas. IMPS is
described in a paper forthcoming in the Journal of Automated
Reasoning. I would also be happy to send copies if you are
interested.
One of the distinctive characteristics of IMPS is its support for the
"little theories" version of the axiomatic theory. This contrasts
with the "big theory" version.
In the big theory version, the mathematician formalizes all of his
work within a single powerful theory, such as ZF set theory. Each
model of this big theory must be large enough to contain
representations of all the objects that will be of interest to the
mathematician.
In the little theories version, different results are proved in
different theories, which may have relatively sparse vocabulary and
small models. Mathematics done in different little theories may be
related by *theory interpretations*. A theory interpretation is a
syntactic translation from the language of one theory to the language
of another, with the proviso that *theorems* of the source theory get
mapped to theorems of the target theory. (To ensure that a
translation is an interpretation, it's enough to prove that the
*axioms* of the source theory map to theorems of the target, together
with a few other obligations that may depend on the logic.)
To reuse a theorem of one theory, one constructs an interpretation
and then gets the image of the source theorem as a theorem of the
target theory without further proof. For instance, to reuse a
theorem about metric spaces in a context concerning the reals, one
constructs an interpretation from the metric space theory to the
reals. This formalizes the idea that the reals "may be regarded as a
metric space" in suchandsuch a way.
As a more interesting example, consider the Knaster fixed point
theorem (which was recently formalized in Imps by Javier Thayer).
First we define monotonicity in the context of a theory of a partial
order written "prec" over objects in a universe uu:
(defconstant monotone
"lambda(f:[uu,uu], forall(x,y:uu, x prec y implies f(x) prec f(y)))"
(theory partialorder))
Then the fixed point theorem is stated and proved in the theory
(extending partialorder) completepartialorder:
(deftheorem knasterfixedpointtheorem
"forall(f:[uu,uu],
forsome(bot,top:uu, forall(x:uu, bot prec x and x prec top))
and
monotone(f)
implies
forsome(z:uu, f(z)=z))"
(theory completepartialorder)
(usages transportablemacete)
(proof ( ... )))
Many useful consequences follow from interpreting uu and prec to be,
for instance, sets and inclusion (such as the SchroederBernstein
theorem), or the reals and <= (for a different kind of intermediate
value theorem), or real functions.
The little theories approach is discussed in a paper called "Little
Theories", CADE11, 567580, written with my colleagues Bill Farmer
and Javier Thayer.
Josh
From qedowner Wed Apr 14 06:46:06 1993
Received: by antares.mcs.anl.gov id AA00557
(5.65c/IDA1.4.4 for qedoutgoing); Wed, 14 Apr 1993 06:17:34 0500
Received: from tuminfo2.informatik.tumuenchen.de by antares.mcs.anl.gov with SMTP id AA00539
(5.65c/IDA1.4.4 for ); Wed, 14 Apr 1993 06:16:45 0500
Received: from sunbroy14.informatik.tumuenchen.de ([131.159.0.114])
by tuminfo2.informatik.tumuenchen.de
with SMTP id <57709>; Wed, 14 Apr 1993 13:16:27 +0200
Received: by sunbroy14.informatik.tumuenchen.de id <8067>; Wed, 14 Apr 1993 13:16:06 +0200
From: Tobias.Nipkow@informatik.tumuenchen.de
To: FORSTER@matgen.ge.cnr.it
Cc: qed@mcs.anl.gov
InReplyTo: FORSTER@matgen.ge.cnr.it's message of Wed, 14 Apr 1993 12:02:00 +0200 <3CC0F1D94020052D@ICE.GE.CNR.IT>
Subject: Bourbaki/Mathias
MessageId: <93Apr14.131606met_dst.8067@sunbroy14.informatik.tumuenchen.de>
Date: Wed, 14 Apr 1993 13:16:04 +0200
Sender: qedowner
Precedence: bulk
ardm@sun1.mfo.unifreiburg.de = Adrian Mathias ?
Tobias
From qedowner Thu Apr 15 18:48:28 1993
Received: by antares.mcs.anl.gov id AA09746
(5.65c/IDA1.4.4 for qedoutgoing); Thu, 15 Apr 1993 18:28:01 0500
Received: from life.ai.mit.edu by antares.mcs.anl.gov with SMTP id AA09737
(5.65c/IDA1.4.4 for ); Thu, 15 Apr 1993 18:27:57 0500
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI4.10) id AA17180; Thu, 15 Apr 93 19:27:49 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI4.10) id AA00625; Thu, 15 Apr 93 19:27:49 EDT
Date: Thu, 15 Apr 93 19:27:49 EDT
MessageId: <9304152327.AA00625@spock>
To: qed@mcs.anl.gov
Subject: Verification systems
Sender: qedowner
Precedence: bulk
In an earlier message I named a variety of verification systems
that might be relevant to the QED project. Bob Boyer has suggested
that I give some more information and references to these systems.
The following list of systems relevant to QED is by no means meant
to be exhaustive, it is just the ones I mentioned in my earlier
message.
A more complete list of reasoning systems can be found in a database
constructed by Carolyn Talcott. The data base can be accessed via ftp
to sail.stanford.edu in the directory /pub/clt/ARS/. This directory
contains a README file.
I have taken some liberties in describing the following systems.
Authors of these systems (or anyone else) should feel free to correct
anything they think is wrong or misleading in these system
descriptions.
******************
1) HOL (Higher Order Logic) Pronounced as either as an acronym
(by pronouncing the letters) or as a word rhyming with "small"
(there was a recent discussion of this and apparent the world is
about 50% in each camp).
This is probably the most widely used verification system.
It is a "foundational" system in the sense that there is one
underlying logic with (arguably) a single intended model
(the universe of sets).
It uses a higher order logic with ML style polymorphism so that
one can define an identity function and apply it to itself. However
there is a straightforward set theoretic denotational semantics
(different occurances of "the identity function" denote identity
functions on different domains).
Although it is higher order and classical I believe it is somewhat weaker
than ZFC (I do not believe that one can prove that there exists a
family of sets containing an infinite set and closed under power set.
In other words, it is missing the axiom of replacement.) I am not
sure whether it contains the axiom of choice.
The interactive verification environment is a descendent of LCF (not
described here, but a common ancestor of many current systems). This
means that one proves theorems by backward chaining on goals using
"tactics" to transform any given goal into a set of subgoals. A
tactic is a user written procedure (satisfying machine checkable
soundness conditions relative to the foundational logic) that reduces
a given goal to subgoals sufficient to impy it. A tactic may perform
an arbitrary amount of automated theorem proving in trying to get a
small set of simplified subgoals. Simple goals are proven
automatically (reduce to no subgoals) by a variety of standard "low
level" tactics.
The most comon application of HOL is the verification of computer
hardware.
o M. Gordon.
HOL: A proof generating system for higherorder logic.
In G. Birtwistle and P. A. Subrahmanyam, editors,
VLSI Specification, Verification, and Synthesis.
Kluwer, 1987.
******************
2) The BoyerMoore prover (also known as NQTHM). This is probably
the second most widely used system. It is also foundational.
The logic consists of expressions definable in the pure (no side effects)
version of the programming language Lisp. These expressions have a fixed
meaning which can be defined via an operational semantics for Lisp.
The atomic formulas of this logic are equations between lisp terms
(such as (EQUAL (NUMBERP X) (TRUE))). The BoyerMoore dialect of
lisp does not allow closures (lambda expressions) and hence is strictly
first order.
Clearly this language can only be used to describe finite objects.
It is most effective when used for proving properties of primitive
recursive functions (the notion of primitive recursion being generalized
from natural numbers to Lisp data structures).
This is probably the most highly automated and effective foundational
verification system. It has been used to verify a large number of
theorems in elementary number theory. Like HOL it is also used for
verification. I believe that the BoyerMoore prover has been more widely
used than HOL in the verification of software. Thousands of programs have
been proven to meet specifications using the BoyerMoore prover. This
includes compilers, assemblers and C programs compiled to 68020 machine
instructions.
The user interface is "Socratic". By this I mean that the user types
a series of statements (called events). The system either accepts or
rejects each statement as it is given. If a statement is rejected it
must be broken down into "simpler" statements. If a statement is
accepted a new proof technique is installed (such as a rewrite rule)
that can be used to verify latter statements. Socratic proofs are
easier to "replay" under modified definitions than are the interaction
traces in LCF derived interfaces such as that of HOL. Socratic proofs
are also more human readable as proof texts.
The primary inference mechanism is term rewriting together with a
large collection of heuristics for performing mathematical induction.
Although the system is controled with user written rewrite rules
(entered as steps in a Socratic proof) there are no user defined
tactics in the sense of LCF.
@book{boyermooreacl,
author = {Boyer, Robert S. and Moore, J. Strother},
title = {A Computational Logic},
year = 1979,
publisher = {Academic Press},
ISBN = {0121229521},
comment = {description of logic, heuristics, and many examples}
}
@book{boyermooreaclh,
author = {Boyer, Robert S. and Moore, J. Strother},
title = {A Computational Logic Handbook},
year = 1988,
publisher = {Academic Press},
ISBN = {0121229505},
orderinfo = {This book may be ordered by calling Academic Press at
(800)3215068 or (314)5288110 for Alaska, Hawaii, Missouri or by writing
to the Academic Press Order Department, 465 S. Lincoln Drive, Troy, MO 63379.}
comment = {comprehensive user's manual}
}
******************
3) nuPRL (pronounced "new pearl"). This is a mature and fairly widely used
foundational system. The underlying logic is derived from Martin Lof type
theory and is based on the CurryHoward isomorphism between formulas and
types. This is sometimes called the "formulas as types" paradigm. This paradigm
is constructive  nuPRL is a constructivist foundational system.
The user interface is an LCF descendent based on user defined tactics
for goal reduction. It has been used to verify a variety of theorems in number
theory as well as hardware and software verification.
R. L. Constable et. al.
Implementing Mathematics with the Nuprl Proof Development System
Prentice Hall
1986
******************
IMPS was described in an earlier message. IMPS has an LCF like
interface and a foundational logic based on the "little theories"
method of organizing mathematical theorems. I believe that IMPS uses
higher order logic as a foundation. It seems likely that one could
translate theorem statements between HOL and IMPS in a direct
semanticspreserving manner. The same should be true of the other
systems in the Talcott data base (see above) that are based on higher
order logic.
******************
Ontic is our system. The logic is an extension of the semantics of
Lisp so that all objects denotable by formulas in ZFC can be denoted
by expression in this "Lisp". The foundational logic is somewhat
stronger than ZFC (it can prove the existence of an inaccessible
cardinal). The user interface is based on the text editor emacs 
one writes a natural deduction proof as a piece of text. A keyboard command
instructs the system to read the proof. The system either accepts the
proof or moves the cursor to the first step that it does not accept.
This is similar to the BoyerMoore style of socratic proof except
that the natural deduction style allows a context of suppositions
to be shared by all the steps in a branch of a case analysis.
No "procedural" information is associated with proof steps (in the
BoyerMoore system proof steps are anotated with instructions as
to how the information is to be used by the prover).
The inference mechansisms are constructed using a forward chaining
(bottom up) logic programming language. However, a single set of
inference mechanisms are used over all proofs and there are no
user defined tactics in the sense of LCF. An early version of this
system was used to verify the Stone representation theorem for Boolean
lattices.
This system is still highly experimental and not released. However a
draft user's manual can be getten by ftp from the machine
ftp.ai.mit.edu in the file /com/ontic/onticmanual.ps. This is a
user's manual but expert readers should be able to derive the set
theoretic denotational semantics from the description in the manual.
David McAllester
From qedowner Thu Apr 15 19:20:38 1993
Received: by antares.mcs.anl.gov id AA10740
(5.65c/IDA1.4.4 for qedoutgoing); Thu, 15 Apr 1993 19:18:14 0500
Received: from swan.cl.cam.ac.uk by antares.mcs.anl.gov with SMTP id AA10732
(5.65c/IDA1.4.4 for ); Thu, 15 Apr 1993 19:18:10 0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP6.4) to cl; Fri, 16 Apr 1993 01:18:04 +0100
To: QED
Subject: "Little Theories" and the base logic
Date: Fri, 16 Apr 93 01:18:00 +0100
From: John Harrison
MessageId: <"swan.cl.ca.855:16.04.93.00.18.08"@cl.cam.ac.uk>
Sender: qedowner
Precedence: bulk
I think the idea of "little theories" is a very good one.
I'm not sure exactly how it works in IMPS, but let's suppose for the sake of
argument that a little theory is a collection of theorems with certain "axioms"
as premisses. (Or equivalently, implicational theorems with the "axioms" as
antecedents.)
However it seems that for this to work properly, the "base" logic that strings
all these statements together has to be reasonably powerful. For example, lots
of interesting algebraic structures, e.g. realclosed fields, aren't finitely
axiomatizable in firstorder logic, so you would seem to be committed to some
form of higher order logic to accommodate them, or else to carrying set theory
around in all the theories. Is this true, or am I misunderstanding the idea?
John Harrison (jrh@cl.cam.ac.uk)
From qedowner Thu Apr 15 19:41:54 1993
Received: by antares.mcs.anl.gov id AA11201
(5.65c/IDA1.4.4 for qedoutgoing); Thu, 15 Apr 1993 19:39:57 0500
Received: from life.ai.mit.edu by antares.mcs.anl.gov with SMTP id AA11193
(5.65c/IDA1.4.4 for ); Thu, 15 Apr 1993 19:39:54 0500
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI4.10) id AA18633; Thu, 15 Apr 93 20:39:51 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI4.10) id AA00645; Thu, 15 Apr 93 20:39:51 EDT
Date: Thu, 15 Apr 93 20:39:51 EDT
MessageId: <9304160039.AA00645@spock>
To: qed@mcs.anl.gov
: bcc rlg, cwitty
Subject: a list of systems.
Sender: qedowner
Precedence: bulk
Here is a list of the systems that have entries in the Talcott data base.
(This is a listing of the directory sail.stanford.edu:/pub/tlc/ARS/Entries)
rwrwr 1 1437 2060 Feb 1 15:13 clam
rwrwr 1 1437 3848 Aug 3 1992 coq
rwrwr 1 1437 5360 Aug 10 1992 ehdm
rwrwr 1 1437 5327 Feb 2 10:16 elf
rwrwr 1 1437 6401 Jan 4 15:15 hol
rwrwr 1 1437 3884 May 15 1992 isabelle
rwrwr 1 1437 6277 Apr 30 1992 larch
rwrwr 1 1437 8004 Aug 10 1992 never
rwrwr 1 1437 6734 May 15 1992 nqthm
rwrwr 1 1437 2786 May 15 1992 nuprl
rwrwr 1 1437 5677 Apr 14 1992 obj3
rwrwr 1 1437 1936 Dec 5 15:22 otter
rwrwr 1 1437 3511 Feb 1 15:13 oyster
rwrwr 1 1437 4416 Apr 2 1992 pcnqthm
rwrwr 1 1437 5104 Dec 5 15:25 pvs
rwrwr 1 1437 2821 May 15 1992 rrl
rwrwr 1 1437 4373 Apr 4 1992 sdvs
rwrwr 1 1437 2713 Aug 10 1992 tableaux
rwrwr 1 1437 2205 May 15 1992 tps
From qedowner Thu Apr 15 21:29:42 1993
Received: by antares.mcs.anl.gov id AA13179
(5.65c/IDA1.4.4 for qedoutgoing); Thu, 15 Apr 1993 21:27:38 0500
Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA13171
(5.65c/IDA1.4.4 for ); Thu, 15 Apr 1993 21:27:35 0500
Received: from malabar.mitre.org by linus.mitre.org (5.61/RCF4S)
id AA28968; Thu, 15 Apr 93 22:27:31 0400
PostedDate: Thu, 15 Apr 93 22:27:28 0400
Received: by malabar.mitre.org (5.61/RCF4C)
id AA02239; Thu, 15 Apr 93 22:27:28 0400
Date: Thu, 15 Apr 93 22:27:28 0400
From: jt@linus.mitre.org
MessageId: <9304160227.AA02239@malabar.mitre.org>
To: qed@mcs.anl.gov
Subject: little theories
Cc: jt@linus.mitre.org, guttman@linus.mitre.org, farmer@linus.mitre.org
Sender: qedowner
Precedence: bulk
In reply to John Harrison's comment about `little theories', IMPS is
indeed committed to a form of higher order logic. There are, however,
a number of important differences between IMPS and HOL. For instance,
the IMPS logic allows undefined terms and partial functions on sorts
(which I do not believe HOL does.)
But the main characteristic of IMPS is one of style. IMPS is designed
to facilitate and encourage its users to develop mathematics as a
network of theories interrelated by theory interpretations. These are
the `little theories' mentioned by Josh Guttman earlier in the
discussion. In our development of the IMPS theory library so far, we
have aggressively exploited this strategy, we believe with some
success.
Javier Thayer
From qedowner Sun Apr 18 11:07:39 1993
Received: by antares.mcs.anl.gov id AA29605
(5.65c/IDA1.4.4 for qedoutgoing); Sun, 18 Apr 1993 11:02:02 0500
Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA29598
(5.65c/IDA1.4.4 for ); Sun, 18 Apr 1993 11:01:56 0500
Received: from circe.mitre.org by linus.mitre.org (5.61/RCF4S)
id AA20861; Sun, 18 Apr 93 12:01:52 0400
PostedDate: Sun, 18 Apr 93 12:01:50 0400
Received: by circe.mitre.org (5.61/RCF4C)
id AA02738; Sun, 18 Apr 93 12:01:51 0400
MessageId: <9304181601.AA02738@circe.mitre.org>
To: John Harrison
Cc: QED
Subject: Re: "Little Theories" and the base logic
InReplyTo: Your message of "Fri, 16 Apr 93 01:18:00 BST."
<"swan.cl.ca.855:16.04.93.00.18.08"@cl.cam.ac.uk>
XPostalAddress: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730
XTelephoneNumber: 617 271 2654; Fax 617 271 3816
Date: Sun, 18 Apr 93 12:01:50 0400
From: guttman@linus.mitre.org
Sender: qedowner
Precedence: bulk
John Harrison (jrh@cl.cam.ac.uk) writes:
> However it seems that for this to work properly, the "base" logic that strings
> all these statements together has to be reasonably powerful. For example, lots
> of interesting algebraic structures, e.g. realclosed fields, aren't finitely
> axiomatizable in firstorder logic, so you would seem to be committed to some
> form of higher order logic to accommodate them, or else to carrying set theory
> around in all the theories.
As Javier mentioned, our preference is certainly also for a form of
higher order logic. But it seems quite feasible that an
implementation (if for some reason it was wedded to first order logic)
could offer a mechanism for axiom schemes.
I don't know whether it would be workable to cover any very wide class
of axiomatizable (r.e.) first order theories. However, in practical
cases infinite sets of axioms have very simple structure (generally
just plugging any syntactic predicate into a hole). A first order
logic with predicate variables (but no quantification or other binding
on them, and with no variables of higher types than predicates) might
be suitable syntax. And I think it could be arranged to have just the
same metalogical properties as a more ordinary first order logic.
Josh
From qedowner Sun Apr 18 11:20:11 1993
Received: by antares.mcs.anl.gov id AA29752
(5.65c/IDA1.4.4 for qedoutgoing); Sun, 18 Apr 1993 11:17:15 0500
Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA29745
(5.65c/IDA1.4.4 for ); Sun, 18 Apr 1993 11:17:13 0500
Received: from circe.mitre.org by linus.mitre.org (5.61/RCF4S)
id AA21101; Sun, 18 Apr 93 12:17:12 0400
PostedDate: Sun, 18 Apr 93 12:17:10 0400
Received: by circe.mitre.org (5.61/RCF4C)
id AA02751; Sun, 18 Apr 93 12:17:11 0400
MessageId: <9304181617.AA02751@circe.mitre.org>
To: qed@mcs.anl.gov
Subject: Re: Verification systems
InReplyTo: Your message of "Thu, 15 Apr 93 19:27:49 EDT."
<9304152327.AA00625@spock>
XPostalAddress: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730
XTelephoneNumber: 617 271 2654; Fax 617 271 3816
Date: Sun, 18 Apr 93 12:17:10 0400
From: guttman@linus.mitre.org
Sender: qedowner
Precedence: bulk
David McAllester writes:
> [HOL] is a "foundational" system in the sense that there is one
> underlying logic with (arguably) a single intended model
> (the universe of sets).
> The BoyerMoore prover ... is also foundational.
> IMPS has ... a foundational logic based on the "little theories"
> method of organizing mathematical theorems.
Do Boyer and Moore think of NQTHM as foundational in the sense of
having a single intended model? I had thought they took the free
variables to range over any arbitrary structure satisfying the axioms
that might be in use.
In any case, if I understand what you mean by "foundational", then
"foundational" contrasts with the little theories approach. Theorems
proved in a theory of (say) a group are not about a single intended
model. Rather, they are about all structures that may satisfy the
group properties. Theory interpretation is a way of bringing these
resluts to bear on another class of models, when all of them exemplify
the properties of the source theory in a particular uniform way.
Or have I misunderstood what you had in mind by "foundational"?
Josh
From qedowner Sun Apr 18 12:39:08 1993
Received: by antares.mcs.anl.gov id AA00702
(5.65c/IDA1.4.4 for qedoutgoing); Sun, 18 Apr 1993 12:37:04 0500
Received: from cli.com by antares.mcs.anl.gov with SMTP id AA00695
(5.65c/IDA1.4.4 for ); Sun, 18 Apr 1993 12:37:01 0500
Received: by CLI.COM (4.1/1); Sun, 18 Apr 93 12:31:36 CDT
Date: Sun, 18 Apr 93 12:36:45 CDT
From: Robert S. Boyer
MessageId: <9304181736.AA13372@axiom.CLI.COM>
Received: by axiom.CLI.COM (4.1/CLI1.2)
id AA13372; Sun, 18 Apr 93 12:36:45 CDT
To: qed@mcs.anl.gov
Subject: Answer to a question, and further speculation on a QED foundation
ReplyTo: boyer@CLI.COM
Sender: qedowner
Precedence: bulk
Josh Guttman asks, in response to a remark by David McAllester,
Do Boyer and Moore think of NQTHM as foundational in the sense of
having a single intended model?
I feel a little bit queasy talking about `intension' in view of the
fact that all the consistent, recursively axiomatizable theories I
know about that include the primitive recursive functions admit
multiple models. But that reservation made, I would agree entirely
with David: I do think of the recursive functions I define with
Moore's and my prover Nqthm (A Computational Logic Handbook, Boyer and
Moore, Academic Press, 1988) as having, intuitively, all of the
specificity of ordinary programs. Technically, as Guttman rightly
points out, we leave room in our system for the addition of new data
types, and via that mechanism one could in principle go on to
axiomatize such theories as set theory, perhaps even using Matt
Kaufmann's skolemizer. And we also leave room via our
CONSTRAIN/FUNCTIONALLYINSTANTIATE mechanism for proving very limited
types of theorems about classes of functions rather than specific
functions. But if we are talking about ordinary, typical Nqthm use,
and within the spirit of informality, then I think that David is
entirely right.
I think McAllester is helpfully trying to put us at one end of the
typical theoremprover map, on the other end of which one might find a
resolution theoremprover to which one might well come from time to
time with an entirely fresh new set of axioms describing whatever one
wants  groups, fields, rings. Nqthm has not been used much in this
way, though I suppose it is capable of checking any first order,
resolution style proof. But probably much poorer than many provers at
finding such a proof.
To connect back to some points in the QED manifesto, I think of Nqthm
as being one of those provers with `too much code to trust'. There
are perhaps 5,000 to 10,000 lines of Nqthm that one would have to
prove correct in order to have the sort of confidence in the proofs it
finds that one might have in, say, a typical resolution style proof,
which can be checked with a very tiny checker.
On the other hand, a certain subset of the Nqthm logic is in the
spirit of Primitive Recursive Arithmetic (PRA). It seems to me
crucial that if the QED project is to have the support of the now very
wide constructivist community, then underlying QED must be some such
logic to which everyone can agree. In the past, the ordinary
mathematical community has probably regarded constructivism as being
of marginal significance. Perhaps the typical math department has at
most only one or two people who think about such issues as
constructivism. But the impact of computing on logic (and vice versa)
has had the effect that it would not surprise me if today half of the
people working on things like mechanical proof checking are of a
somewhat constructivist bent. A too clasically powerful base logic
would thus from the start perhaps leave out many potentially major
contributors to the QED project.
The key point, I think that classicist David Hilbert would say, is
that WE CAN ALL AGREE to present and discuss essentially all important
logics and theories in a `finitistic' format, such as PRA admits. (I
wouldn't be so bold to make such a sweeping claim if I weren't more or
less trying to repeat a point that Feferman has been making in recent
years in presenting his PRApowerful logic FS0.) We can all agree to
PRA proofs of many important metatheorems and of most automated
reasoning techniques (which typically are merely pieces of applied
proof theory). And the constructivists can even agree to propositions
such as that some string, say, P, is a proof of a theorem TH in ZF set
theory. But if we wire ZF or something classically quite strong at
the bottom of the QED edifice, the constructivists can't play.
I should temper my gospel fervor enthusiasm for PRA by observing that
while I agree with Tait (Finitism, J. of Philosophy, 1981, 78,
524546) that PRA is THE NECESSARY AND SUFFICIENT logic for talking
about logics and proofs, there exists at least someone who refuses to
believe in PRA (YesseninVolpin, The UltraIntuitionistic Criticism
..., Intuitionism and Proof Theory, NorthHolland, 1970, pp. 345).
But this fellow also refuses to believe in 10^12, which seems to fly
in the face of teraflops and terabyte memories.
Bob
There is no safety in numbers, or in anything else. Thurber.
From qedowner Sun Apr 18 14:08:37 1993
Received: by antares.mcs.anl.gov id AA01640
(5.65c/IDA1.4.4 for qedoutgoing); Sun, 18 Apr 1993 14:06:10 0500
Received: from cli.com by antares.mcs.anl.gov with SMTP id AA01633
(5.65c/IDA1.4.4 for ); Sun, 18 Apr 1993 14:06:08 0500
Received: by CLI.COM (4.1/1); Sun, 18 Apr 93 14:00:42 CDT
Date: Sun, 18 Apr 93 14:05:52 CDT
From: Robert S. Boyer
MessageId: <9304181905.AA13435@axiom.CLI.COM>
Received: by axiom.CLI.COM (4.1/CLI1.2)
id AA13435; Sun, 18 Apr 93 14:05:52 CDT
To: qed@mcs.anl.gov
Subject: Feferman FSO reference
ReplyTo: boyer@CLI.COM
Sender: qedowner
Precedence: bulk
I should have included the following reference in my previous message
in which I mentioned Feferman's PRAstrong logic FS0: "Finitary
inductively presented logics", S. Feferman, Logic Colloquium '88,
Ferro, Bonotto, Valenti and Zanardo (eds.), Elsevier, NorthHolland,
1989., pp. 191220.
From qedowner Sun Apr 18 15:32:04 1993
Received: by antares.mcs.anl.gov id AA02431
(5.65c/IDA1.4.4 for qedoutgoing); Sun, 18 Apr 1993 15:29:23 0500
Received: from swan.cl.cam.ac.uk by antares.mcs.anl.gov with SMTP id AA02423
(5.65c/IDA1.4.4 for ); Sun, 18 Apr 1993 15:29:00 0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP6.4) to cl; Sun, 18 Apr 1993 21:28:54 +0100
To: QED
Subject: Re: Answer to a question, and further speculation on a QED foundation
InReplyTo: Your message of Sun, 18 Apr 93 12:36:45 0500. <9304181736.AA13372@axiom.CLI.COM>
Date: Sun, 18 Apr 93 21:28:49 +0100
From: John Harrison
MessageId: <"swan.cl.ca.904:18.04.93.20.28.57"@cl.cam.ac.uk>
Sender: qedowner
Precedence: bulk
Bob Boyer writes:
> I feel a little bit queasy talking about `intension' in view of the
> fact that all the consistent, recursively axiomatizable theories I
> know about that include the primitive recursive functions admit
> multiple models.
Indeed, if you are talking about firstorder theories, then since any
arithmetic worth the name has an infinite model, it must, by the upward
LowenheimSkolem theorem, have models of arbitrarily large cardinality,
which obviously can't all be isomorphic.
In fact I believe not all models can even be elementarily equivalent for the
following reason: any model assigns a definite true/false value to any
closed term. But if all models are elementarily equivalent, then a sentence
must either be true in all models or false in all models. This would mean
the theory is deductively complete (because FOL is semantically complete).
If the theory includes much arithmetic, Godel's theorem rules this out,
given consistency and recursive axiomatizability.
Perhaps PRA or FSO are so weak that this does not apply? Apparently they
lack the usual quantifier rules. Maybe someone could post a brief
explanation of what PRA is like, for those of us who don't know.
John Harrison (jrh@cl.cam.ac.uk)
From qedowner Sun Apr 18 17:06:22 1993
Received: by antares.mcs.anl.gov id AA03153
(5.65c/IDA1.4.4 for qedoutgoing); Sun, 18 Apr 1993 16:43:27 0500
Received: from life.ai.mit.edu by antares.mcs.anl.gov with SMTP id AA03139
(5.65c/IDA1.4.4 for ); Sun, 18 Apr 1993 16:43:05 0500
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI4.10) id AA24298; Sun, 18 Apr 93 17:43:03 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI4.10) id AA00902; Sun, 18 Apr 93 17:42:58 EDT
Date: Sun, 18 Apr 93 17:42:58 EDT
MessageId: <9304182142.AA00902@spock>
To: guttman@linus.mitre.org
Cc: qed@mcs.anl.gov
InReplyTo: guttman@linus.mitre.org's message of Sun, 18 Apr 93 12:17:10 0400 <9304181617.AA02751@circe.mitre.org>
Subject: Verification systems
Sender: qedowner
Precedence: bulk
By "foundational" I mean a system that is intended to be used (or is
most commonly used) by extension with definitions lemmas and theorems.
This is to be contrasted with systems whose typical use involves new
(unjustified) axioms. Definitions guarantee that extensions are
conservative  no new facts can be proved about old symbols. In
most resolution systems there is no notion of conservative extension
via definitions.
Mathematics itself seems to have made a transition at some point from
axiomatic to foundational techniques. The modern informal approach
DEFINES a group to be a structure (or a tuple) satisfying certain
conditions. Only rarely are really new axioms considered (such as the
existence of measurable cardinals).
Does IMPS have a conservative extension property stating that the
introduction of a new little theory does not allow the proof of new
theorems about old theories? If so then I would call IMPS a
foundational system. It seems to me that the theorems provable in any
given theory will be influenced by your choice of foundation. I'm not
sure if you encorporate the axiom of choice. Can you prove that any
group can be extended by a predicate that well orders its domain?
Can you prove that infinite groups exist?
David
From qedowner Sun Apr 18 17:36:04 1993
Received: by antares.mcs.anl.gov id AA03650
(5.65c/IDA1.4.4 for qedoutgoing); Sun, 18 Apr 1993 17:34:23 0500
Received: from life.ai.mit.edu by antares.mcs.anl.gov with SMTP id AA03643
(5.65c/IDA1.4.4 for ); Sun, 18 Apr 1993 17:34:19 0500
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI4.10) id AA25023; Sun, 18 Apr 93 18:34:16 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI4.10) id AA00906; Sun, 18 Apr 93 18:34:15 EDT
Date: Sun, 18 Apr 93 18:34:15 EDT
MessageId: <9304182234.AA00906@spock>
To: boyer@cli.com
Cc: qed@mcs.anl.gov
InReplyTo: Robert S. Boyer's message of Sun, 18 Apr 93 12:36:45 CDT <9304181736.AA13372@axiom.CLI.COM>
Subject: Answer to a question, and further speculation on a QED foundation
Sender: qedowner
Precedence: bulk
Although I am sympathetic to the idea that we can all accept primitive
recursive arithmetic (PRA) I am little troubled by using it as the
foundation of QED. Consider the mean value theorem (MVT) of calculus.
I agree that this thoerem can be encoded as "P is a proof in ZFC of
ZFCMVT" where ZFCMVT is some formal statement of the mean value
theorem in the langauge of set theory. I am concerned about the
difficulty of using this entry in the QED library. It seems
"encrypted". I need to talk to its author and have them explain how
they represent formulas as numbers. Although I can imagine "plain
text" annotations and translation algorithms entered in the QED
library, it seems like a lot of extra work.
Perhaps there is a compromise position. We could agree on a language
without agreeing on an inference system. For example, we could agree
to use the language of set theory (perhaps annotated with some
standard syntactic sugar like tuples, structures and
lambdaexpressions). We could have a long list of axioms and
inference principles not all of which are accepted by all players.
Each "theorem" could be annotated with the axioms and principles
needed to prove it. This annotation could, of course, be derived
automatically from a given proof. This allows "skeptical players" but
avoids the use of metatheorems. I would think that PRA corresponds
to a very restricted set of set theoretic inference principles.
David