**Mail folder:**QED**Next message:**Tobias.Nipkow@informatik.tu-muenchen.de: "Bourbaki/Mathias"**Previous message:**FORSTER@matgen.ge.cnr.it: "Bourbaki/Mathias"**In-reply-to:**guttman@linus.mitre.org: "Re: a multilingual approach "

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