Author
Mike Gordon
Abstract
Set theory is the standard foundation for mathematics, but the
majority of general purpose mechanized proof assistants support
versions of type theory (higher order logic). Examples include Alf,
Automath, Coq, Ehdm, HOL, IMPS, Lambda, LEGO, Nuprl, PVS and
Veritas. For many applications type theory works well and provides,
for specification, the benefits of type-checking that are well-known
in programming. However, there are areas where types get in the way or
seem unmotivated. Furthermore, most people with a scientific or
engineering background already know set theory, whereas type theory
may appear inaccessable and so be an obstacle to the uptake of proof
assistants based on it. This paper describes some experiments (using
HOL) in combining set theory and type theory; the aim is to get the
best of both worlds in a single system. Three approaches have been
tried, all based on an axiomatically specified type V of ZF-like
sets: (i) HOL is used without any additions besides V; (ii) an
embedding of the HOL logic into V is provided; (iii) HOL
axiomatic theories are automatically translated into set-theoretic
definitional theories. These approaches are illustrated with two
examples: the construction of lists and a simple lemma in group
theory.