Technical reports

A combination of geometry theorem proving and nonstandard analysis, with application to Newton’s Principia

Jacques Désiré Fleuriot

August 1999, 135 pages

This technical report is based on a dissertation submitted March 1999 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Clare College.

Abstract

Sir Isaac Newton’s Philosophiae 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 Euclidian 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 formalisation of a geometry theory based on existing methods from automated geometry theorem proving. The theory contains extra geometric notions, including the definition of the ellipse and its tangent, that enables 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 the the 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.

Full text

PDF (11.7 MB)

BibTeX record

@TechReport{UCAM-CL-TR-469,
  author =	 {Fleuriot, Jacques D{\'e}sir{\'e}},
  title = 	 {{A combination of geometry theorem proving and nonstandard
         	   analysis, with application to Newton's Principia}},
  year = 	 1999,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-469.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-469},
  number = 	 {UCAM-CL-TR-469}
}