Machine Proving System Of The Foundations Of General Topology Based On Coq

Formal methods are a special technology based on mathematical theory in the field of computer science,which are widely used to specify,develop,and verify hardware and software systems.Mechanical theorem proving is an important branch of formal methods,and is a profound embodiment of basic theory for artificial intelligence.In recent years,the theorem provers such as Coq,Isabelle,HOL Light,Mizar,and Lean had rapid development.It is a very important research field to realize the machine proof and automatic reasoning of the mathematical theorem,and further construct the formal mathematical library based on mathematics mechanization.Topology is generally considered to be one of the three main areas of modern pure mathematics,and it mainly studies the continuous properties of geometric figures.Topology is not only an important part of applied mathematics but it also has been a significant increase in the applications to fields as diverse as economics,engineering,chemistry and medicine.This dissertation aims to present a machine-proving system of the foundations of general topology from the eight axioms of the Morse-Kelley axiom system using the Coq theorem prover,and further study the mathematical application and engineering application of the formal system.The main research contents and contributions of this dissertation include the following four aspects.1.A formal verification platform for the basic theory of set theory and number systems is developed in Coq.The construction of this platform mainly includes the following four parts.The first part completes the formal description of the fundamental logical symbols,logical properties and primitive mathematical constants for our system.The second part presents the formal description of the Morse-Kelley axiom system based on the concepts of set and function.The third part is the formalization of set theory,which uses the axiomatic method to formally verify the basic concepts and properties of sets and operations,relations,functions,indexing set family,countable set and uncountable set,and cartesian products.And further formally proves the pigeonhole principle,Cantor-Bernstein therorem,the equivalence among the axiom of choice,and the Tukey lemma.The fourth part is the formalization of number systems,which formally verifies the definitions,operation properties and order relations for different number systems based on the Morse-Kelley axiomatic set theory.The induction principle on the natural number,the recursion theorem on the natural number,and the supremum theorem on the real number are formally proved.The above work has realized the connection of Morse-Kelley axiomatic set theory and real analysis theory.It is not only the further extention of Morse-Kelley axiomatic set theory,but also a profound embodiment of embedding number systems into set theory.2.Machine proving system of the foundations of general topology is proposed based on the Morse-Kelley axiom system.It mainly follows Xiong’s textbook to study the topological spaces and continuous mappings in general topology,which is based on the formal verification platform for the basic theory of set theory and number systems.The main content includes the following three parts.The first part presents the formalization of topological spaces and the basic notion of topology.Firstly,the concept of topological spaces is constructed by open sets.Furthermore,the basic concepts and properties for neighborhoods and neighborhood systems,derived sets,closed sets,closure,interior,boundary,bases and subbases,sequences are formally verified.The second part realizes the formalization of continuous mappings in topological spaces.By abstracting the definition of continuous mapping in Euclidean space,the formal description of continuous mapping in metric space and topological space is presented in turn.It also focuses on a special kind of continuous mapping in topological space,namely homeomorphism mapping.And further formally verifies the equivalence propositions of continuous mapping in topological spaces.The third part is the formalization of new topological spaces,which formally describe the definitions and basic properties for subspaces,product spaces and quotient spaces based on the existing topological spaces.There is a good corresponding relationship between the formal description of the above work and the symbol representations,definitions and theorems description in the reference textbook.It is helpful to understand the core content of general topology more deeply,and can be further extended to formal verification of mathematical disciplines such as algebraic topology and differential topology.3.The application of machine proving system of the foundations of general topology in mathematics is realized.We formally prove the equivalence of the definition of topological spaces and C.T.Yang’s theorem using the theorem prover Coq.Firstly,the equivalence of the definition of topological space which is defined by open sets is formally proved by the eight basic topological concepts of neighborhood systems,closure,closed sets,interior,exterior,boundary,bases and subbases.The theory of topological spaces can be fully constructed by the above basic topological concepts.Secondly,C.T.Yang’s theorem subtly presents the relationship between the whole and the local properties in topological space,which lays the foundation for the convergence theory in topological space.After analysis of the essence and development of this theorem,C.T.Yang’s theorem is formally proved in the Coq theorem prover.The above work not only enriches the theoretical basis of topological spaces but also helps to understand the essence of topological spaces.4.The application of the machine proving system of the foundations of general topology in the field of Geo-spatial information sciences is realized.In the theorem prover Coq,we realize the formal verification of a classical topological spatial relations model for geographic information systems which is proposed by Egenhofer and Franzosa.Firstly,the basic notions and properties of connected spaces are formalized,and some topological properties used in geographic information systems are supplemented.Secondly,the topological spatial relations between two sets are described by using the concept of the intersection value,and we formally prove the topological spatial relations between two sets which are restricted to the regularly closed and the planar spatial regions.This work provides a new way for the reliability verification of geographic information systems models and software,it can also contribute to storing,querying,and manipulating geographically referenced data.