STMM: A Set Theory for Mechanized Mathematics
William M. Farmer
2001
Abstract
Although set theory is the most popular foundation for mathematics,
not many mechanized mathematics systems are based on set theory.
Zermelo-Fraenkel (ZF) set theory and other traditional set theories
are not an adequate foundation for mechanized mathematics. STMM is a
version of von-Neumann-Bernays-Goedel (NBG) set theory that is
intended to be a Set Theory for Mechanized Mathematics. STMM allows
terms to denote proper classes and to be undefined, has a definite
description operator, provides a sort system for classifying terms by
value, and includes lambda-notation with term constructors for
function application and function abstraction. This paper describes
STMM and discusses why it is a good foundation for mechanized
mathematics.
Keywords: Set theory, NBG, higher-order logic, mechanized mathematics,
theorem proving systems, partial functions, undefinedness, sorts.