Abstract

This talk presents work carried out jointly with Ed Dean and John Mumma.

For more than two thousand years, Euclid’s Elements was viewed as the paradigm of rigorous argumentation. But this changed in the nineteenth century, with concerns over the use of diagrammatic inferences and their ability to secure general validity. Axiomatizations by Pasch, Hilbert, and later Tarski are now taken to rectify these shortcomings, but proofs in these axiomatic systems look very different from Euclid’s.

In this talk, I will argue that proofs in the Elements, taken at face value, can be understood in formal terms. I will describe a formal system with both diagram- and text-based inferences that provides a much more faithful representation of Euclidean reasoning. For the class of theorems that can be expressed in the language, the system is sound and complete with respect to Euclidean fields, that is, the semantics corresponding to ruler and compass constructions.

The system’s one-step inferences are smoothly verified by current automated reasoning technology. This makes it possible to formally verify Euclidean diagrammatic proofs, and provides useful insight into the nature of mathematical proof more generally.