Types, sorts and variable types

Solomon Feferman (sf@CSLI.Stanford.EDU)
Wed, 24 Aug 94 18:02:44 PDT

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.