Axiomatic set theory is a foundational system of mathematics and has important applications in many fields. In this work, we present a formal system of axiomatic set theory based on the Coq proof assistant. The axiomatic system used in the formal system refers to Morse-Kelley set theory which is a relatively complete and concise axiomatic set theory.
In this formal system, we complete the formalization of basic definitions of sets, functions, ordinal numbers and cardinal numbers and prove the most commonly used theorems in Coq. Moreover, the non-negative integers are defined and Peano's postulates are proved as theorems. According to the axiom of choice, we also present formal proofs of Hausdorff maximal principle and Schroeder-Bernstein theorem. The whole formalization of the system includes eight axioms, one axiom schema, 62 definitions and 148 corollaries or theorems.
The ``axiomatic set theory'' formal system is free from the more obvious paradoxes and a complete axiomatic system is constructed through it. It is designed to give quickly and naturally a foundation for mathematics. On the basis of the system, we can prove many famous theorems and quickly formalize the theories of topology, modern algebra and so on.
- Elementary_Logic.v Defines some basic knowledge of elementary logic.
- Classification_Axiom_Scheme.v Defines some primitive constants and presents the classification axiom scheme.
- Elementary_Algebra.v Provides some elementary algebra operations of classes and provides some basic definitions related to sets.
- Sets_Existence.v Provides some basic definitions of sets and proves some theorems concerned with the existence of sets.
- Ordered_Pairs.v Provides the properties of ordered pairs and relations.
- Functions.v Defines functions and proves some properties of functions.
- Well_Ordering.v Defines well ordering and proves some properties of well ordering.
- Ordinals.v Defines the ordinal numbers and establishes the fundamental properties.
- Itegers.v Defines the non-negative integers and proves the Peano's postulates.
- Choice_Axiom.v Presents the axiom of choice and proves the Hausdorff maximal principle.
- Cardinal_Numbers.v Defines the cardinal numbers and proves the most commonly used properties.
Tianyu Sun. stycyj@bupt.edu.cn