[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]
NEW BOOK ANNOUNCEMENT
AUTHOR: Luis Sanchis, Professor at Syracuse University.
TITLE: Set Theory: An Operational Approach.
PUBLISHER: Gordon and Breach Publishers.
MORE INFORMATION: http://www.cis.syr.edu/~sanchis
In most interpretations types are sets with special structures, and it
is fair and trivial to assert that set theory is relevant to type theory.
This is not usually mentioned because it is taken for granted that set
theory is identical with Zermelo Fraenkel axiomatics. In my book I propose
a theory that does not conflict with ZF but is is both more conservative
and friendlier to the user. For example, I introduce primitive rules of
induction and recursion that I am sure practitioners of type theory will
find very attractive. In another direction, I object to the usual
definition (axiom?) of the power-set, but I propose a new construction
where the power-set is derived via the axiom of choice. The description
in my home page (http://www.cis.syr.edu/~sanchis) provides a few more
details and also a moderate (I hope) dosis of propaganda.