A Comparative Review of ZFC, NBG, and MK Axiom Systems: Theoretical Foundations and Formalization in Coq

This paper presents a systematic comparative study of three major axiomatic set theory systems: Zermelo-Fraenkel system with “the Axiom of Choice” (ZFC), von Neumann-Bernays-Gödel system (NBG), and Morse-Kelley system (MK). The research begins by tracing the historical development and motivations behind these three axiomatic frameworks, followed by a detailed analysis of their axiom structures and fundamental concepts. The systems are then compared across several dimensions: expressive power, metamathematical properties, and practical applications. The innovative aspect of this study lies in introducing the Coq proof assistant as a formal verification tool to implement and compare MK, NBG, and ZFC, systematically investigating their differences within a formalized environment. Research findings indicate that the three axiomatic systems present distinct advantages and challenges during formalization, providing new perspectives for understanding the essential characteristics of axiomatic set theory and its position in mathematical foundations. This comparative analysis helps clarify the relationships between these three axiomatic systems and provides a theoretical reference for future formal verification work in set theory.