A Combination of Geometry Theorem Proving and Nonstandard Analysis, with Application to Newton's Principia
University of Cambridge, Computer Laboratory, 1999 - Automatic theorem proving - 135 pages
Abstract: "Sir Isaac Newton's Philosophiæ Naturalis Principia Mathematica (the Principia) was first published in 1687 and set much of the foundations that led to profound changes in modern science. Despite the influence of the work, the elegance of the geometrical techniques used by Newton is little known since the demonstrations of most of the theorems set out in it are usually done using calculus. Newton's reasoning also goes beyond the traditional boundaries of Euclidean geometry with the presence of both motion and infinitesimals. This thesis describes the mechanization of Lemmas and Propositions from the Principia using formal tools developed in the generic theorem prover Isabelle. We discuss the formalization of a geometry theory based on existing methods from automated geometry theorem proving. The theory contains extra geometric notions, including definitions of the ellipse and its tangent, that enable us to deal with the motion of bodies and other physical aspects. We introduce the formalization of a theory of filters and ultrafilters, and the purely definitional construction of the hyperreal numbers of Nonstandard Analysis (NSA). The hyperreals form a proper field extension of the reals that contains new types of numbers including infinitesimals and infinite numbers. By combining notions from NSA and geometry theorem proving, we propose an 'infinitesimal' geometry in which quantities can be infinitely small. This approach then reveals new properties of the geometry that only hold because infinitesimal elements are allowed. We also mechanize some analytic geometry and use it to verify the geometry theories of Isabelle. We then report on the main application of this framework. We discuss the formalization of several results from the Principia and give a detailed case study of one of its most important propositions: the Propositio Kepleriana. An anomaly is revealed in Newton's reasoning through our rigorous mechanization. Finally, we present the formalization of a portion of mathematical analysis using the nonstandard approach. We mechanize both standard and nonstandard definitions of familiar concepts, prove their equivalence, and use nonstandard arguments to provide intuitive yet rigorous proofs of many of their properties."
27 pages matching construction in this book
Results 1-3 of 27
What people are saying - Write a review
We haven't found any reviews in the usual places.
Geometry Theorem Proving
Constructing the Hyperreals
Infinitesimal and Analytic Geometry
4 other sections not shown
automated axioms basic calculus Cauchy Cauchy sequence centripetal force circle Clifford Algebra concepts congruent construction convergence cross product deal defined denoted derive developed diagram ellipse embedded equal equivalence classes equivalence relation Euclidean geometry example Figure filter finite following theorem formalized in Isabelle free ultrafilter full-angles function geometry theorem proving Hilbert's hrinv hyperreal numbers hyperreals hypreal infinite numbers infinitely small infinitesimal inite introduced intuitive Isabelle's Isabelle/HOL len(C len(P len(Q len(S logic mathematical mechanization natural numbers Newton's reasoning non-Archimedean Nonstandard Analysis nonstandard definitions nonstandard extension notation notions NSDERIV(x number system pnat Principia properties Proposition 11 quantities ratio real analysis real numbers rigorous rinv rules s-delta Section set theory signed area simplifier SReal standard and nonstandard step subset sumhr sumr SuperFrechet tangent techniques Transfer Principle triangles Ultrafilter Theorem ultrapower upper bound various Zorn's Lemma