STMM: A Set Theory for Mechanized Mathematics

摘要

Although set theory is the most popular foundation for mathematics, not many mech- anized 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--Godel (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.