Author: Jacques D. Fleuriot

Publisher:

Published: 1999

Total Pages: 158

ISBN-13:

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."