In a recent joint paper with Jeremy Avigad and John Mumma (forthcoming in the Review of Symbolic Logic, preprint available at the arXiv), we devise a formal system that is intended to faithfully capture the notion of Euclidean geometric proofs. Specifically, is meant to be a formal counterpart to Books I through IV of Euclid’s Elements, including a formal codification of Euclid’s diagrammatic reasoning; we want proofs in to mirror Euclid’s actual proofs. With this post I just want to briefly “set the scene” of the paper. In a later post, I will discuss some proof theory that comes up naturally in our analysis.

By modern logical lights, geometry did not receive a properly rigorous foundation until works such as Hilbert’s informal Grundlagen der Geometrie, and later formal work by the likes of Tarski. To be sure, Euclid certainly leaves certain necessary assumptions unstated (a minor problem which is easily remedied); but Euclid’s methods of proof have also been derided for relying on spatial intuition rather than precisely formulated logical rules. If one is not careful when proving with diagrams, one can easily misstep and use features of a particular diagram that are not general in order to make unwarranted deductions (as in classic “proofs” such as that all triangles are isosceles).

But of course, Euclid does not prove absurdities such as these! As Ken Manders has stressed, Euclidean geometry was a remarkably stable practice for thousands of years, and its practitioners exhibited a certain diagram discipline. One central idea is this:

What makes Euclid’s proofs (as opposed to those of Hilbert, say) diagrammatic has nothing to do with an improper reliance on spatial intuition; rather, it is merely that Euclid’s one-step inferences are of a very different nature than those of Hilbert.

While Euclid’s Elements might appear very far from rigorous when looking at it with systems like Hilbert’s or Tarski’s in mind, the point is that Euclid’s methods of proof can be given a solid formal foundation in and of themselves. (And in this light Euclid’s text is much closer to formalized mathematics than typical informal-yet-rigorous mathematical works, which goes well with the fact that Euclid was considered to be a paragon of mathematical rigor for many centuries.)

I don’t want to get into the nitty gritty details of spelling out the construction of , and I can get to the topic I want to discuss without doing so. As indicated above, we want single inference steps in to match the sort of “diagrammatic” inferences that Euclid makes. Consider:

Proposition I.12: Given a point off of line , construct line through perpendicular to .

Diagram for Proposition I.12

Proof. Let be a point on the other side of from . Let be the circle through with center . Let and be the intersection points of and . By Proposition I.10, let bisect the segment from to . Let be the line through and . By Proposition I.8, , hence and are perpendicular.

Inferences like the highlighted one above are the sort of step where we might worry that we could misuse a diagram to reach unwarranted conclusions (though this case is rather obviously benign). Our particular instantiation of our diagram has such intersection points, but we have given no reasoning to indicate why it must, i.e. why this isn’t merely an artifact of the particular way we drew it. A Hilbertian or Tarskian proof would provide a chain of logical reasoning in order to arrive at the existence of these intersection points. That is all well and good, but we end up with very different proofs than Euclid’s of course. In fact, in too we will have such chains of reasoning that look nothing like moves Euclid would explicitly carry out, but we have these only on a “background” or “internal” level. The proof given above (N.B. this has nothing to do with the picture) actually is the proof of Proposition I.12. (I led you to believe I was giving Euclid’s proof; one can check that ours has come out essentially identical to Euclid’s.)

In order for to properly license these kinds of diagrammatic inferences, but not go too far, there is a formalized notion of “direct diagrammatic consequence” in our paper. Next time, I will talk about some of the interesting proof-theoretic points surrounding its design.