A Formal System For Euclid's Elements

A Formal System For Euclid's Elements, Jeremy Avigad, Edward Dean, and John Mumma. Review of Symbolic Logic, Vol. 2, No. 4, 2009.

Abstract. We present a formal system, E, which provides a faithful model of the proofs in Euclid’s Elements, including the use of diagrammatic reasoning.

Diagrammatic languages are a perennial favorite discussion topic here, and Euclid's proofs constitute one of the oldest diagrammatic languages around. And yet for hundreds of years (at least since Leibniz) people have argued about whether or not the diagrams are really part of a formal system of reasoning, or whether they are simply visual aids hanging on the side of the true proof. The latter position is the one that Hilbert and Tarski took as well when they gave formal axiomatic systems for geometry.

But was this necessary, or just a contingent fact of the logical machinery available to them? Avigad and his coauthors show the former point of view also works, and that you can do it with very basic proof theory (there's little here unfamiliar to anyone who has read Pierce's book). Yet it sheds a lot of light on how the diagrams in the Elements work, in part because of their very careful analysis of how to read the diagrams -- that is, what conclusion a diagram really licenses you to draw, and which ones are accidents of the specific figure on the page. How they consider these issues is a good model for anyone designing their own visual programming languages.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Is it a diagrammatic language?

I haven't fully read this paper, but despite calling the entities of interest "diagrams", the logic looks fully symbolic. I see the actual picture diagrams in this system as "hanging on the side of the true proof."

2.6. Our methodology. We have cast our project as an attempt to model Euclidean
diagrammatic proof, aiming to clarify its logical form, and, in particular, the nature of
diagrammatic inference. In casting our project in this way, we are adopting a certain
methodological stance. From a logical standpoint, what makes a Euclidean proof “dia-
grammatic” is not the fact that we find it helpful to consult a diagram in order to verify
the correctness of the proof, or that, in the absence of such a physical artifact, we tend to
roll our eyes toward the back of our heads and imagine such a diagram. Rather, the salient
feature of Euclidean proof is that certain sorts of inferences are admitted as basic, and are
made without further justification. When we say we are analyzing Euclidean diagrammatic
reasoning, we mean simply that we are trying to determine which inferences have this basic
character, in contrast to the geometrically valid inferences that are spelled out in greater
detail in the text of the Elements.

Rerepresenting diagrams

Well, in category we are familiar with repesenting sketches both as figures on paper, and as formal constructions. But the purpose of the theory of sketches is to validate the reasoning category theorists actually do with commutative diagrams.

It is key that an instance of a geometrically valid inference might be a construction drawn by hand on a piece of paper. That drawing has a form that might or might not be valid in this Euclidean system.

Put this another way: one might say one has constructed in Coq a proof of the fundamental theorem of arithmetic. Would you say that this way of speaking is incorrect, because one has only really constructed a digital artefact that is hanging on the side of the true proof?

Not the same

I wasn't arguing that there is no such thing as diagrammatic reasoning, but rather that in this case, diagrams aren't playing such a big role. I don't see this as akin to reading a map or commutative diagram, where certain properties can be read off from the diagram directly. Here, in geometry, we can have A < B < C < D shown on a line, with that relative ordering fixed by construction except the relative order of B and C. The geometrical relations of interest aren't captured by any particular diagram.

If you'll look at section 3.3, you'll see a list of symbolic inferences that are permitted. That they are justified by consideration of diagrams seems irrelevant to me - the rules of most formal systems are ultimately justified by informal reasoning about the thing the system is supposed to model. The formal system itself is, nonetheless, symbolic. I don't object to calling this diagrammatic reasoning because I don't think such a thing could exist. On the contrary, it's because I can think it can exist, and don't think this is it.

In the area of diagrammatic reasoning

my experiences with model-driven development have led me to believe Jon Barwise was the logician who has had the largest impact on this field, but also as a group the Visual Inference Laboratory at Indiana University that he led. Barwise, from what I can tell, has had a huge impact on systems theorists disguised as UML weenies.

Barwise and Etchemendy's seminal paper on the theory of visual inferences is probably the best starting point. See: Visual information and valid reasoning. Purchaseable via a book of collected works, like this one. If anybody knows of an online copy to share, please reply to this.


How exactly did Barwise influence UML? There are definitely some influences on UML from the 'visual reasoning' community, particularly the use of higraphs for state diagrams (and UML 1.x activity diagrams). However, UML was clearly never intended to be a platform for rigorous inference: even the most 'basic' "UML infrastructure" metamodel is an elephantine monstrosity.

Barwise's paper is not available online AFAICT, but searching for papers which reference it turns up several interesting articles.

Barwise's paper

Re: searching for papers which reference it turns up several interesting articles..

Note to self: This looks interesting: Computers, visualization, and the nature of reasoning by Barwise and Etchemendy.

How exactly did Barwise

How exactly did Barwise influence UML?

Not noticeably, as you say. His work has a bigger influence on formal diagrammatic systems like constraint diagrams: e.g. Stapleton's A Decidable Constraint Diagram Reasoning System. These diagrams are intended to take the place of OCL for specifying invariants etc. They've not taken off in that domain, of course, but are an interesting topic in their own right, and we can but hope. (I'm a student with the Visual Modelling Group at Brighton, which has had a big part in producing the theoretical framework for constraint diagrams, and also interesting work on generating and drawing diagrams based on Euler circles...if anyone's interested, our publications page gives a flavour, although it's out of date.)


I've noticed you've replied a couple of times to things I've said regarding visual languages, and you generally have bright things to say. Maybe you should be a contributing editor for LtU and post some of the more interesting diagrammatic reasoning papers you come across.

Thanks for mentioning where you do your work, too. I tried looking you up about a year ago but Jim Burton is an exceedingly common name.

oh, English language, you are so silly sometimes

I don't think Barwise has had much influence on the UML, but he has influenced people who are interested in modeling languages and tend to use UML just because (a) it is object-oriented [as opposed to modeling notations like IDEF which are mainly brain damaged government contraptions from the era when structured programming with COBOL vision where the supermarket grocery clerk would be your "coder"] (b) it is ubiquitous.

As for activity diagrams, I think those are pure and utter crap and feel bad for anyone who has ever had to look at one, especially an IBM-esque one with utter nonsense like "conditional threads". My opinion on activity diagrams is mainly methodological, since they are inherently non-OO (from a methodology standpoint, they encourage functional decompositions that lead to sequential coupling, and decrease re-use and composition of what otherwise could be autonomous entities). However, they also contain a ton of feature bloat that mainly exists to model 3GL code visually. Let me re-assert, as I have many times here before, that going down this reverse engineering route is a slippery slope and probably a guaranteed bad idea.

EDIT: I also don't think UML 2.x is that much worse than any other metalevel modeling tool, such as the Common Lisp Object System. UML is simply purely bigger than CLOS (which is itself enormous), and so as complexity tends to increase combinatorically with feature count, UML is correspondingly complex and bug-ridden. That's why you use Profiles to limit the scope of UML, thus reducing the feature count and likelihood of interacting with "bugs" in the specification. The major downside of UML is increasing generality in the execution model removes some elegance from using a simpler methodology directly. Subsetting then becomes a burden. To loosely quote belated comedian Mitch Hedburg, I don't like Pepperidge Farm, because that stuff is too fancy. It's wrapped twice. I don't need another step between me and toast.

I am not entirely sure I see

I am not entirely sure I see why this would be relevant for people working on visual programming languages, but this is very cool anyway, so thanks for posting it!

Formal diagrammatic reasoning

Is there such a thing? Well, the question is at least of interest when talking about the semantics of visual languages, so that's relevant around here.

For people who doubt that there is such a thing as diagrammatic reasoning, I recommend that the next time you find yourself lost, and are trying to figure out where you are on a map, to think about the inferences you are making. Are they purely symbolic? Sorry for any delay this exercise might cause you in finding your way.

Can diagrammatic reasoning be formal? Well, can symbolic reasoning be formal? The reason we think so is that some symbolic representations of inferences are schematic (consider, e.g., the Barbara syllogism: All As are B, and all Bs are C, so all As are C), and so are the skeleton for many other inferences, and so allow us to reduce talking about generative classes of inferences to a number of well-understood schemes.

This seems to be obviously the case here, as is it for Peirce's existential graphs. The graphs in this paper are obviously schematic - you can use the same figure for bisecting an angle, applying it to the case where there are a continuum of possible anglkes to be bisected, and the generality of the system of a whole depends on this schematicity. So yes, it is formal.

124 pages

Can't remember now if I liked Logic and Visual Information by Eric M. Hammer, but given how short it is, I heartily recommend it to anyone interested in the subject.

formal reasoning in VPLs

For instances of 'formal diagrammatic reasoning' in actual VPLs, you might be interested in the work I pointed out earlier by John Baez and others about string diagrams in monoidal categories. There were also useful pointers in the thread about 'function concatenation'(link).

Dan Piponi has pointed out that similar diagrams can apply to commutative monads [slides] [video]. (ISTM that extending them to the non-commutative case should be straightforward by adding a notation for 'barriers').

That Selinger paper is

That Selinger paper is really nice! I should look for a warm and friendly introduction to monoidal categories, so that I can post it as a prequel to the Selinger.

Anyway, a variant of sigfpe's observation is in Benton and Wadler's 1996 paper on monads and linear logic: any commutative monad gives rise to a model of intuitionistic logic (ie, a symmetric monoidal closed category). But if you see an easy way to extend that to the noncommutative case, I urge you to write it up -- it wasn't until just last year that Alex Simpson & co. figured out what linear-logic-ish term language corresponds to noncommutative monads.

I should look for a warm and friendly

I should look for a warm and friendly introduction to monoidal categories

The Baez paper seems warm and friendly enough (and it gives a notation for the cartesian closed case, which Selinger doesn't!) but I suppose you could find something even friendlier in Baez's other writings, including old issues of This Week's Finds

it wasn't until just last year that Alex Simpson & co. figured out what linear-logic-ish term language corresponds to noncommutative monads.

If a proper correspondence wasn't given until last year, that probably means I was thinking about a very special case. But since most practical uses of monads boil down to 'forcing function calls w/ side effects to be sequenced in the order you want', even ad-hoc special-case support could be very useful.