package coq-morse-kelley-axiomatic-set-theory

In this project, we present a formalization of axiomatic set theory based on the Coq proof assistant. The axiomatic system is derived from Morse-Kelley (MK) set theory which is a relatively complete and concise axiomatic set theory.

MK includes eight axioms, one axiom schema, and 181 definitions or theorems. Different from ZFC, MK admits classes (whose quantity is more extensive than that of sets) as fundamental objects. That is to say, every mathematical object (ordered pair, function, integer, etc.) is a class, and only those classes belonging to some other ones are defined as sets. The non-set classes are named “proper classes”. In fact, ZFC can be proven consistent in MK. We consider that MK is a proper extension of ZFC and is convenient to utilize in formalization processes.