From qed-owner Mon Apr 12 17:38:34 1993 Received: by antares.mcs.anl.gov id AA25256 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.4.4 for ); Mon, 12 Apr 1993 17:23:20 -0500 Message-Id: <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: qed-owner 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 qed-owner Tue Apr 13 10:32:49 1993 Received: by antares.mcs.anl.gov id AA11770 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 13 Apr 1993 10:12:41 -0500 Received: from saturn.wwc.edu by antares.mcs.anl.gov with SMTP id AA11758 (5.65c/IDA-1.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 In-Reply-To: ; from "Zdzislaw Meglicki" at Apr 13, 93 1:50 pm X-Mailer: ELM [version 2.3 PL11] Message-Id: <9304130819.aa10002@saturn.wwc.edu> Sender: qed-owner 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)-6-249-0747, tel: (Australia)-6-249-0158 -- Ted Ashton (ashted@wwc.edu) Campus Computer Center (509) 527-2307 Walla Walla College College Place, WA 99324 "The slide rule liveth still." From qed-owner Tue Apr 13 10:45:52 1993 Received: by antares.mcs.anl.gov id AA12105 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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 Message-Id: <9304131525.AA01463@lutra.mcs.anl.gov> To: qed@mcs.anl.gov Subject: response to Meglicki Sender: qed-owner 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 | e-mail: mccune@mcs.anl.gov | | MCS-221 | phone: (708) 252-3065 | | Argonne National Laboratory | FAX: (708) 252-5986 | | Argonne, IL 60439-4844 | | | U.S.A. | | --------------------------------------------------------------------- Replied: Wed, 14 Apr 1993 12:57:51 -0500 Replied: "Gene Rackow " From qed-owner Tue Apr 13 14:48:36 1993 Received: by antares.mcs.anl.gov id AA16001 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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 Message-Id: <9304131838.AA04604@skeeve.mcs.anl.gov> To: qed@mcs.anl.gov Subject: manifest Sender: qed-owner 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 qed-owner Tue Apr 13 15:06:00 1993 Received: by antares.mcs.anl.gov id AA16249 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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" Message-Id: <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: qed-owner 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 low-level proof, based on matching character strings. The low-level 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 low-level checker is only a few pages of code; it's required that it be totally understandable in detail by a single person. The low-level data files should be human readable, and include comments with the high-level proof. The working character set should be emailable. Rich Schroeppel rcs@cs.arizona.edu From qed-owner Tue Apr 13 15:24:34 1993 Received: by antares.mcs.anl.gov id AA16520 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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/AI-4.10) id AA08247; Tue, 13 Apr 93 15:14:55 EDT From: dam@ai.mit.edu (David McAllester) Received: by spock (4.1/AI-4.10) id AA00347; Tue, 13 Apr 93 15:14:54 EDT Date: Tue, 13 Apr 93 15:14:54 EDT Message-Id: <9304131914.AA00347@spock> To: mccune@mcs.anl.gov Cc: qed@mcs.anl.gov In-Reply-To: Bill McCune's message of Tue, 13 Apr 93 10:25:52 CDT <9304131525.AA01463@lutra.mcs.anl.gov> Subject: the base logic Sender: qed-owner 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 Boyer-Moore 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 Boyer-Moore, 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 qed-owner Tue Apr 13 15:44:26 1993 Received: by antares.mcs.anl.gov id AA16805 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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/AI-4.10) id AA08830; Tue, 13 Apr 93 15:35:55 EDT From: dam@ai.mit.edu (David McAllester) Received: by spock (4.1/AI-4.10) id AA00351; Tue, 13 Apr 93 15:35:55 EDT Date: Tue, 13 Apr 93 15:35:55 EDT Message-Id: <9304131935.AA00351@spock> To: qed@mcs.anl.gov Subject: a multilingual approach Sender: qed-owner 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 qed-owner Tue Apr 13 17:25:32 1993 Received: by antares.mcs.anl.gov id AA18968 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 13 Apr 1993 16:10:54 -0500 Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA18961 (5.65c/IDA-1.4.4 for ); Tue, 13 Apr 1993 16:10:51 -0500 Received: from circe.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA12832; Tue, 13 Apr 93 17:10:49 -0400 Posted-Date: Tue, 13 Apr 93 17:10:38 -0400 Received: by circe.mitre.org (5.61/RCF-4C) id AA10474; Tue, 13 Apr 93 17:10:40 -0400 Message-Id: <9304132110.AA10474@circe.mitre.org> To: dam@ai.mit.edu (David McAllester) Cc: qed@mcs.anl.gov Subject: Re: a multilingual approach In-Reply-To: Your message of "Tue, 13 Apr 93 15:35:55 EDT." <9304131935.AA00351@spock> X-Postal-Address: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730 X-Telephone-Number: 617 271 2654; Fax 617 271 3816 Date: Tue, 13 Apr 93 17:10:38 -0400 From: guttman@linus.mitre.org Sender: qed-owner 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 qed-owner Tue Apr 13 18:14:00 1993 Received: by antares.mcs.anl.gov id AA19649 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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 (PP-6.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 Message-Id: <"swan.cl.ca.893:13.04.93.21.40.32"@cl.cam.ac.uk> Sender: qed-owner Precedence: bulk The influence of Bourbaki on the accepted structure of mathematics surely goes beyond a few bits of arcane terminology like "quasi-compact", 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 qed-owner Tue Apr 13 20:40:50 1993 Received: by antares.mcs.anl.gov id AA21469 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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/IDA-1.4.4 for qed@mcs.anl.gov); Tue, 13 Apr 1993 17:06:22 -0700 Message-Id: <199304140006.AA02373@panther.cs.uidaho.edu> To: qed@mcs.anl.gov Cc: guttman@linus.mitre.org Subject: Re: a multilingual approach In-Reply-To: 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" X-Mts: smtp Sender: qed-owner 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 qed-owner Tue Apr 13 20:45:44 1993 Received: by antares.mcs.anl.gov id AA21541 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.4.4 for ); Tue, 13 Apr 1993 19:01:44 -0500 Received: by arp.anu.edu.au id AA14285 (5.65c/IDA-1.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) Message-Id: 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: qed-owner 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)-6-249-0747, tel: (Australia)-6-249-0158 From qed-owner Tue Apr 13 23:20:50 1993 Received: by antares.mcs.anl.gov id AA23617 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.4.4 for ); Tue, 13 Apr 1993 21:36:12 -0500 Received: by xenon.csl.sri.com id AA08110 (5.65b/IDA-1.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 Message-Id: <9304140236.AA08110@xenon.csl.sri.com> To: qed@mcs.anl.gov In-Reply-To: David McAllester's message of Tue, 13 Apr 93 15:14:54 EDT <9304131914.AA00347@spock> Subject: the base logic Sender: qed-owner 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 qed-owner Wed Apr 14 00:01:03 1993 Received: by antares.mcs.anl.gov id AA24106 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 13 Apr 1993 22:17:06 -0500 Received: from cli.com by antares.mcs.anl.gov with SMTP id AA24098 (5.65c/IDA-1.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 Message-Id: <9304140316.AA08792@axiom.CLI.COM> Received: by axiom.CLI.COM (4.1/CLI-1.2) id AA08792; Tue, 13 Apr 93 22:16:48 CDT To: qed@mcs.anl.gov Subject: references Reply-To: boyer@CLI.COM Sender: qed-owner 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 qed-owner Wed Apr 14 05:42:39 1993 Received: by antares.mcs.anl.gov id AA28787 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.4.4 for ); Wed, 14 Apr 1993 04:04:26 -0500 Received: from DECNET-MAIL 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 Message-Id: <3CC0F1D94020052D@ICE.GE.CNR.IT> X-Envelope-To: qed@mcs.anl.gov X-Vms-To: ICE622::IN%"qed@mcs.anl.gov" Sender: qed-owner 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.uni-freiburg.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 qed-owner Wed Apr 14 06:45:37 1993 Received: by antares.mcs.anl.gov id AA00644 (5.65c/IDA-1.4.4 for qed-outgoing); Wed, 14 Apr 1993 06:25:58 -0500 Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA00637 (5.65c/IDA-1.4.4 for ); Wed, 14 Apr 1993 06:25:55 -0500 Received: from circe.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA18447; Wed, 14 Apr 93 07:25:53 -0400 Posted-Date: Wed, 14 Apr 93 07:25:50 -0400 Received: by circe.mitre.org (5.61/RCF-4C) id AA10713; Wed, 14 Apr 93 07:25:51 -0400 Message-Id: <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 In-Reply-To: Your message of "Tue, 13 Apr 93 17:10:38 EDT." <9304132110.AA10474@circe.mitre.org> X-Postal-Address: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730 X-Telephone-Number: 617 271 2654; Fax 617 271 3816 Date: Wed, 14 Apr 93 07:25:50 -0400 From: guttman@linus.mitre.org Sender: qed-owner 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 re-use 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 re-use 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 such-and-such 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: (def-constant monotone "lambda(f:[uu,uu], forall(x,y:uu, x prec y implies f(x) prec f(y)))" (theory partial-order)) Then the fixed point theorem is stated and proved in the theory (extending partial-order) complete-partial-order: (def-theorem knaster-fixed-point-theorem "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 complete-partial-order) (usages transportable-macete) (proof ( ... ))) Many useful consequences follow from interpreting uu and prec to be, for instance, sets and inclusion (such as the Schroeder-Bernstein 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", CADE-11, 567-580, written with my colleagues Bill Farmer and Javier Thayer. Josh From qed-owner Wed Apr 14 06:46:06 1993 Received: by antares.mcs.anl.gov id AA00557 (5.65c/IDA-1.4.4 for qed-outgoing); Wed, 14 Apr 1993 06:17:34 -0500 Received: from tuminfo2.informatik.tu-muenchen.de by antares.mcs.anl.gov with SMTP id AA00539 (5.65c/IDA-1.4.4 for ); Wed, 14 Apr 1993 06:16:45 -0500 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57709>; Wed, 14 Apr 1993 13:16:27 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8067>; Wed, 14 Apr 1993 13:16:06 +0200 From: Tobias.Nipkow@informatik.tu-muenchen.de To: FORSTER@matgen.ge.cnr.it Cc: qed@mcs.anl.gov In-Reply-To: FORSTER@matgen.ge.cnr.it's message of Wed, 14 Apr 1993 12:02:00 +0200 <3CC0F1D94020052D@ICE.GE.CNR.IT> Subject: Bourbaki/Mathias Message-Id: <93Apr14.131606met_dst.8067@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 14 Apr 1993 13:16:04 +0200 Sender: qed-owner Precedence: bulk ardm@sun1.mfo.uni-freiburg.de = Adrian Mathias ? Tobias From qed-owner Thu Apr 15 18:48:28 1993 Received: by antares.mcs.anl.gov id AA09746 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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/AI-4.10) id AA17180; Thu, 15 Apr 93 19:27:49 EDT From: dam@ai.mit.edu (David McAllester) Received: by spock (4.1/AI-4.10) id AA00625; Thu, 15 Apr 93 19:27:49 EDT Date: Thu, 15 Apr 93 19:27:49 EDT Message-Id: <9304152327.AA00625@spock> To: qed@mcs.anl.gov Subject: Verification systems Sender: qed-owner 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 higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis. Kluwer, 1987. ****************** 2) The Boyer-Moore 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 Boyer-Moore 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 Boyer-Moore prover has been more widely used than HOL in the verification of software. Thousands of programs have been proven to meet specifications using the Boyer-Moore 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{boyer-moore-acl, author = {Boyer, Robert S. and Moore, J. Strother}, title = {A Computational Logic}, year = 1979, publisher = {Academic Press}, ISBN = {0-12-122952-1}, comment = {description of logic, heuristics, and many examples} } @book{boyer-moore-aclh, author = {Boyer, Robert S. and Moore, J. Strother}, title = {A Computational Logic Handbook}, year = 1988, publisher = {Academic Press}, ISBN = {0-12-122950-5}, order-info = {This book may be ordered by calling Academic Press at (800)321-5068 or (314)528-8110 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 Curry-Howard 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 semantics-preserving 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 Boyer-Moore 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 Boyer-Moore 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/ontic-manual.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 qed-owner Thu Apr 15 19:20:38 1993 Received: by antares.mcs.anl.gov id AA10740 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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 (PP-6.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 Message-Id: <"swan.cl.ca.855:16.04.93.00.18.08"@cl.cam.ac.uk> Sender: qed-owner 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. real-closed fields, aren't finitely axiomatizable in first-order 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 qed-owner Thu Apr 15 19:41:54 1993 Received: by antares.mcs.anl.gov id AA11201 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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/AI-4.10) id AA18633; Thu, 15 Apr 93 20:39:51 EDT From: dam@ai.mit.edu (David McAllester) Received: by spock (4.1/AI-4.10) id AA00645; Thu, 15 Apr 93 20:39:51 EDT Date: Thu, 15 Apr 93 20:39:51 EDT Message-Id: <9304160039.AA00645@spock> To: qed@mcs.anl.gov : bcc rlg, cwitty Subject: a list of systems. Sender: qed-owner 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) -rw-rw-r-- 1 1437 2060 Feb 1 15:13 clam -rw-rw-r-- 1 1437 3848 Aug 3 1992 coq -rw-rw-r-- 1 1437 5360 Aug 10 1992 ehdm -rw-rw-r-- 1 1437 5327 Feb 2 10:16 elf -rw-rw-r-- 1 1437 6401 Jan 4 15:15 hol -rw-rw-r-- 1 1437 3884 May 15 1992 isabelle -rw-rw-r-- 1 1437 6277 Apr 30 1992 larch -rw-rw-r-- 1 1437 8004 Aug 10 1992 never -rw-rw-r-- 1 1437 6734 May 15 1992 nqthm -rw-rw-r-- 1 1437 2786 May 15 1992 nuprl -rw-rw-r-- 1 1437 5677 Apr 14 1992 obj3 -rw-rw-r-- 1 1437 1936 Dec 5 15:22 otter -rw-rw-r-- 1 1437 3511 Feb 1 15:13 oyster -rw-rw-r-- 1 1437 4416 Apr 2 1992 pcnqthm -rw-rw-r-- 1 1437 5104 Dec 5 15:25 pvs -rw-rw-r-- 1 1437 2821 May 15 1992 rrl -rw-rw-r-- 1 1437 4373 Apr 4 1992 sdvs -rw-rw-r-- 1 1437 2713 Aug 10 1992 tableaux -rw-rw-r-- 1 1437 2205 May 15 1992 tps From qed-owner Thu Apr 15 21:29:42 1993 Received: by antares.mcs.anl.gov id AA13179 (5.65c/IDA-1.4.4 for qed-outgoing); Thu, 15 Apr 1993 21:27:38 -0500 Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA13171 (5.65c/IDA-1.4.4 for ); Thu, 15 Apr 1993 21:27:35 -0500 Received: from malabar.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA28968; Thu, 15 Apr 93 22:27:31 -0400 Posted-Date: Thu, 15 Apr 93 22:27:28 -0400 Received: by malabar.mitre.org (5.61/RCF-4C) id AA02239; Thu, 15 Apr 93 22:27:28 -0400 Date: Thu, 15 Apr 93 22:27:28 -0400 From: jt@linus.mitre.org Message-Id: <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: qed-owner 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 qed-owner Sun Apr 18 11:07:39 1993 Received: by antares.mcs.anl.gov id AA29605 (5.65c/IDA-1.4.4 for qed-outgoing); Sun, 18 Apr 1993 11:02:02 -0500 Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA29598 (5.65c/IDA-1.4.4 for ); Sun, 18 Apr 1993 11:01:56 -0500 Received: from circe.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA20861; Sun, 18 Apr 93 12:01:52 -0400 Posted-Date: Sun, 18 Apr 93 12:01:50 -0400 Received: by circe.mitre.org (5.61/RCF-4C) id AA02738; Sun, 18 Apr 93 12:01:51 -0400 Message-Id: <9304181601.AA02738@circe.mitre.org> To: John Harrison Cc: QED Subject: Re: "Little Theories" and the base logic In-Reply-To: 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> X-Postal-Address: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730 X-Telephone-Number: 617 271 2654; Fax 617 271 3816 Date: Sun, 18 Apr 93 12:01:50 -0400 From: guttman@linus.mitre.org Sender: qed-owner 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. real-closed fields, aren't finitely > axiomatizable in first-order 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 meta-logical properties as a more ordinary first order logic. Josh From qed-owner Sun Apr 18 11:20:11 1993 Received: by antares.mcs.anl.gov id AA29752 (5.65c/IDA-1.4.4 for qed-outgoing); Sun, 18 Apr 1993 11:17:15 -0500 Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA29745 (5.65c/IDA-1.4.4 for ); Sun, 18 Apr 1993 11:17:13 -0500 Received: from circe.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA21101; Sun, 18 Apr 93 12:17:12 -0400 Posted-Date: Sun, 18 Apr 93 12:17:10 -0400 Received: by circe.mitre.org (5.61/RCF-4C) id AA02751; Sun, 18 Apr 93 12:17:11 -0400 Message-Id: <9304181617.AA02751@circe.mitre.org> To: qed@mcs.anl.gov Subject: Re: Verification systems In-Reply-To: Your message of "Thu, 15 Apr 93 19:27:49 EDT." <9304152327.AA00625@spock> X-Postal-Address: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730 X-Telephone-Number: 617 271 2654; Fax 617 271 3816 Date: Sun, 18 Apr 93 12:17:10 -0400 From: guttman@linus.mitre.org Sender: qed-owner 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 Boyer-Moore 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 qed-owner Sun Apr 18 12:39:08 1993 Received: by antares.mcs.anl.gov id AA00702 (5.65c/IDA-1.4.4 for qed-outgoing); Sun, 18 Apr 1993 12:37:04 -0500 Received: from cli.com by antares.mcs.anl.gov with SMTP id AA00695 (5.65c/IDA-1.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 Message-Id: <9304181736.AA13372@axiom.CLI.COM> Received: by axiom.CLI.COM (4.1/CLI-1.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 Reply-To: boyer@CLI.COM Sender: qed-owner 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/FUNCTIONALLY-INSTANTIATE 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 theorem-prover map, on the other end of which one might find a resolution theorem-prover 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 PRA-powerful 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, 524-546) 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 (Yessenin-Volpin, The Ultra-Intuitionistic Criticism ..., Intuitionism and Proof Theory, North-Holland, 1970, pp. 3-45). 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 qed-owner Sun Apr 18 14:08:37 1993 Received: by antares.mcs.anl.gov id AA01640 (5.65c/IDA-1.4.4 for qed-outgoing); Sun, 18 Apr 1993 14:06:10 -0500 Received: from cli.com by antares.mcs.anl.gov with SMTP id AA01633 (5.65c/IDA-1.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 Message-Id: <9304181905.AA13435@axiom.CLI.COM> Received: by axiom.CLI.COM (4.1/CLI-1.2) id AA13435; Sun, 18 Apr 93 14:05:52 CDT To: qed@mcs.anl.gov Subject: Feferman FSO reference Reply-To: boyer@CLI.COM Sender: qed-owner Precedence: bulk I should have included the following reference in my previous message in which I mentioned Feferman's PRA-strong logic FS0: "Finitary inductively presented logics", S. Feferman, Logic Colloquium '88, Ferro, Bonotto, Valenti and Zanardo (eds.), Elsevier, North-Holland, 1989., pp. 191-220. From qed-owner Sun Apr 18 15:32:04 1993 Received: by antares.mcs.anl.gov id AA02431 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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 (PP-6.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 In-Reply-To: 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 Message-Id: <"swan.cl.ca.904:18.04.93.20.28.57"@cl.cam.ac.uk> Sender: qed-owner 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 first-order theories, then since any arithmetic worth the name has an infinite model, it must, by the upward Lowenheim-Skolem 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 qed-owner Sun Apr 18 17:06:22 1993 Received: by antares.mcs.anl.gov id AA03153 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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/AI-4.10) id AA24298; Sun, 18 Apr 93 17:43:03 EDT From: dam@ai.mit.edu (David McAllester) Received: by spock (4.1/AI-4.10) id AA00902; Sun, 18 Apr 93 17:42:58 EDT Date: Sun, 18 Apr 93 17:42:58 EDT Message-Id: <9304182142.AA00902@spock> To: guttman@linus.mitre.org Cc: qed@mcs.anl.gov In-Reply-To: guttman@linus.mitre.org's message of Sun, 18 Apr 93 12:17:10 -0400 <9304181617.AA02751@circe.mitre.org> Subject: Verification systems Sender: qed-owner 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 qed-owner Sun Apr 18 17:36:04 1993 Received: by antares.mcs.anl.gov id AA03650 (5.65c/IDA-1.4.4 for qed-outgoing); 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/IDA-1.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/AI-4.10) id AA25023; Sun, 18 Apr 93 18:34:16 EDT From: dam@ai.mit.edu (David McAllester) Received: by spock (4.1/AI-4.10) id AA00906; Sun, 18 Apr 93 18:34:15 EDT Date: Sun, 18 Apr 93 18:34:15 EDT Message-Id: <9304182234.AA00906@spock> To: boyer@cli.com Cc: qed@mcs.anl.gov In-Reply-To: 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: qed-owner 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 ZFC-MVT" where ZFC-MVT 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 lambda-expressions). 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