Machine Proof System Of Analysis

Formal verification technology can develop rigorous and reliable theory,which is widely used in mathematical theorem proving and highly trusted system testing,and has made great progress in recent years.The machine proof of mathematical theorem is the profound embodiment of the basic theory of artificial intelligence.It is of great significance to realize formal theorem proof and intelligent automatic reasoning based on mathematical mechanization.Starting from the limit,analysis studies the relevant theories of calculus,which effectively promotes the development of mathematics,physics,astronomy and other disciplines,provides strong support for the engineering field.Therefore,the formal research of analysis theory has important academic significance and wide application value.Using the formal verification tool Coq,this thesis develops a machine proof system of analysis based on type theory and set theory,and further realizes the formalization of the equivalence between nine real number completeness theorems,the properties of continuous functions on closed intervals and calculus without limit.The main research contents and innovations of this thesis are summarized as follows:1.The machine proof system of foundations of analysis is developed strictly following Landau’s Foundations of Analysis through the formal verification tool Coq.Moreover,we expand the important contents of the real number theory,and add the related properties of finiteness and sequence,so as to enhance the universality of this system.The design of system is divided into four parts:the first part is the logical basis,which lists the necessary and reasonable logic axioms and inferences of the system.The second part is elementary set theory,which describes the basic concepts of set theory through predicate logic,including the operation and mapping of sets.The third part is the formalization of Foundations of Analysis.Combined with the Calculus of Inductive Construction,the concepts of natural number,fraction,rational number,division,real number,complex number,their order relationship and operation are defined ’in turn,and key theorems are proved:minimum principle,Archimedes theorem(for rational number),the existence of irrational number and Dedekind fundamental theorem(real number completeness theorem).The fourth part is the supplementary part of real number theory,which completes the finiteness definition and relevant properties based on natural number and elementary set theory,and expands the real number theory,including supplementary operation and real value sequence.Furthermore,starting from the formal system of Morse-Kelley axiomatic set theory,this thesis formally proves the recursion theorem of natural numbers through the transfinite recursion theorem in this theory,which opens up the interface between axiomatic set theory and analysis.At last,we formalize all the contents of natural numbers in Foundations of Analysis based on Morse Kelley axiomatic set theory,and presents the formalization of other number systems.2.We complete the formalization of the equivalence between nine real number completeness theorems and the properties of continuous functions on closed intervals.Real number completeness theorem plays an important role in mathematics and is is very critical in the transition from calculus to analysis.It fundamentally solves the core of real number theory,and developes limit theory injecting strictness into analysis.Common completeness theorems of real numbers:Dedekind fundamental theorem,supremum theorem,monotone convergence theorem,Cauchy Cantor nested interval theorem,Heine Borel Lebesgue finite cover theorem,Bolzano Weierstrass accumulation point theorem,Bolzano Weierstrass sequential compactness theorem and Bolzano Cauchy convergence criterion.Starting from Dedekind fundamental theorem,we prove these theorems in turn.Finally,the Dedekind fundamental theorem is proved by Bolzano Cauchy convergence criterion.In addition,the equivalence between Dedekind fundamental theorem and supremum theorem,supremum theorem and intermediate value theorem is proved separately.Further,starting from the supremum theorem,the properties of continuous functions on closed intervals are formally proved,including extreme value property,boundedness,intermediate value property and uniform continuity.All proofs had been verified by Coq without exception.3.Formalizing the calculus without limit theory proposed by academician Qun Lin and academician Jingzhong Zhang.Due to the concept of vague infinitesimal,the initiation period of calculus caused many contradictions.Through strictly establishing the limit on "ε-N",the second mathematical crisis was solved,but the complex concepts and derivation made it difficult for beginners to understand.Therefore,academician Qun Lin and academician Jingzhong Zhang advocated the third generation of calculus--calculus without limit.In this thesis,the formal definition of difference quotient control function is derived from simple physical facts,and the intuitive relationship between difference quotient control function and monotonicity,concavity,convexity can be obtained.Furthermore,the elementary definitions of uniform derivative function and strong derivative function are given.It is obtained that the difference quotient function has uniform continuity or Lipschitz condition,that is,it is uniform derivative function or strong derivative function.Then,the relationship between integral system,definite integral and difference quotient control function is formally proved,so that differential and integral are connected through difference quotient control function.Finally,the core theorems in calculus such as Newton Leibniz formula,upper limit-variable integral differentiability and Taylor formula are formally proved.All contents are formally described and verified by Coq,which shows that the theory is rigorous and reliable,moreover,any proof does not involve the real number completeness theorem.