From owner-qed Wed Aug 24 20:03:47 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id UAA02577 for qed-out; Wed, 24 Aug 1994 20:03:09 -0500 Received: from Csli.Stanford.EDU (Csli.Stanford.EDU [36.9.0.46]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id UAA02572 for ; Wed, 24 Aug 1994 20:03:03 -0500 Received: (from sf@localhost) by Csli.Stanford.EDU (8.6.9/8.6.9) id SAA02579; Wed, 24 Aug 1994 18:02:46 -0700 Date: Wed, 24 Aug 94 18:02:44 PDT From: Solomon Feferman To: qed@mcs.anl.gov Cc: sf@CSLI.Stanford.EDU Subject: Types, sorts and variable types Message-ID: Sender: owner-qed@mcs.anl.gov Precedence: bulk Re today's message from Farmer on a system of types and sorts, and Hoover's response, I have urged in various papers since 1975 on explicit mathematics, the use of formal systems with variable types (aka classifications, classes, and apparently sorts in Hoover's sense), for the formalization of classical, constructive and computational mathematics. This features, as in Farmer's IMPS partial functions and non-denoting expressions (best brought out by Beeson's logic of partial terms). Applications to typing systems with polymorphism and subtyping have been given in the papers: "Logics for termination and correctness of functional programs", in _Logic from Computer Science_, MSRI Pubs.vol.21, Springer 1992, 95-127, "Polymorphic typed lambda-calculi in a type-free axiomatic framework", in _Logic and Computation_, Contemporary Mathematics series vol.106, Amer. Math. Soc., 1990, 101-136. There is no question in my mind that if the qed project is to be viable, it has to concentrate on systems with these kinds of features. Relations to type-checking for computer programs (which in any case are of limited value), are a secondary matter. Moreover, it should be pretty open-ended about what basic principles are admitted, as in de Bruin's restaurant. What will be important is to have a rich formal language which reflects the everyday world of mathematics, where there is no concern with the "ultimate" building blocks of mathematical concepts (as many suppose sets and membership to be). Then one has to inquire what principles are commonly appealed to in a given body of mathematics when it comes to representing and checking proofs. The first part would be akin to what some people have tried to do in AI with the representation of common-sense knowledge.