STMM: A Set Theory for Mechanized Mathematics

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–Gödel (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.