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.