Thursday, June 14, 2007

Here's looking at Euclid

A few weeks ago the Formal Epistemology Workshop (FEW) )was held at CMU. I attended a few sessions. The few sessions I attended were pretty good. In addition to a few good talks, I got to meet Kenny, who also commented on one of the talks I liked. Writing about the talks, even though kind of belated, is a great way to procrastinate on this paper I have hanging around, so I figure I'll do that.

I went to four talks. One on diagrams in proofs, one by Kevin Kelly on his stuff, one incomprehensible one by Isaac Levi, and one neat one on philosophical issues in AI and information theory. I'm going to talk about the first one. It was by John Mumma of CMU and it was on his thesis work. He was trying to offer a way of reconstructing Euclid's proofs in the Elements that gave the diagrams an important role. The traditional story, since Hilbert, is that diagrams don't have any actual role in the proof. Proofs are sequences of propositions or text, so diagrams, being neither propositional nor textual, play no role in proof. At best, they gesture towards how to the missing steps in a proof. Mumma's idea was to come up with a way of using the diagrams in proofs. He distinguished between two sorts of diagrammatic properties, whose names I cannot remember. The rough idea was that one was metric (how long) and the other topological (what is between/inside what). Based on this distinction, he noted that Euclid only invoked the latter when his diagrams played a role in the proofs. The proofs contain instructions for constructing the diagrams, and, when the constructions are done out of order the diagrams can lead us astray. He gave some examples and took the moral to be that the order of the constructions are important, that they create dependencies among the parts and properties of the diagrams. From my point of view, the neat thing was what he did next. In order to talk about proofs that actually use diagrams in a central way, he defined a proof system that included syntactic diagram objects. These diagrams were (roughly) n x n grids with lines between various points (I think they ended up being 4-tuples encoding this information). Akin to inference rules, diagrams get operations, or constructions, on them. (He might have ended up calling them inference rules in the end.) The proof system is a sequent calculus in which each sequent A, B-> A',B' consists of (sets of) diagrams A,A', and (sets of) formulas B,B'. This is all a bit rough since my memory of these details is hazy after the few weeks that have passed. Mumma had some nice result about this proof system being able to nicely reconstruct all of the proofs from the first four or so books of the Elements. Well done! It looks like a neat project.

I said the new proof system was the interesting thing from my point of view. I will explain. The traditional picture says that proofs are sequences of propositions or text related in a suitable way. Mumma's move was to expand the idea of proof theoretic language to include diagrammatic objects and operations on them. No reason to be overly strict with the notion of language for proofs. He did not go all the way to using full diagrams, it seems. The diagrammatic objects are encoded in 4-tuples (with some further abstracting into equivalence classes, I think). This means that some things are getting left out, but things must be left out to get the right level of generality needed for proofs I suppose. If Mumma's idea pans out (must read papers...), it seems like it could have an application to inferentialist semantics of the Brandomian sort. Certain sorts of concepts, e.g. geometrical ones, seem to have natural inferential roles bound up with diagrams or pictures. It would be nice to be able to take advantage of that. But, this is speculation. Something else I'm wondering is to what degree Mumma's work can hook up to Etchemendy and Barwise's project of investing hybrid forms of information, which are forms of information that depend on narrowly linguistic forms of information as well as traditionally non-propositional forms of information, such as maps and diagrams. Maybe some day I will get to come back to this.

2 comments:

Aidan said...

I actually wearing that shirt as I read this. Cosmic.

Shawn said...

Awesome. I found out the other day that the picture on yours is proposition 1 of the Elements. Unfortunately, I did not have the presence of mind to wear the version of the shirt I have while writing the post; it has a portrait of Euclid.