## Geometrical Logic.

I’m such a crazy fun-lovin’ guy that I’m thinking about how to formalise Euclidean geometry. By this I mean affine geometry. Without a measuring function. So all you have is an infinite 2D plane, a compass and a straight edge. How would one rewrite the Elements in a symbolic language? Perhaps taking a,b,c… to be points and having operators like being equidistant and stuff. I don’t know enough about algebraic geometry to know this isn’t what they’re doing, but it is different from the group theory stuff one can do with symmetry groups and such. There is something to geometry over and above what can be done with group theory. For example, one can prove that a pentagon is constructible with a compass and straight edge. But that is a non-constructive proof. So the construction procedure for a pentagon is outside the realm of groups.

Why would you want to do this? Firstly to explore the relationship between geometry and logic. When you are doing number theory or set theory or other branches of mathematics, there is a kind of presupposed foundation of logical consequence required to do anything useful. I wonder if the same is true of geometry. Since all we are doing is constructing geometrical objects from other geometrical objects, it isn’t obvious how logic gets involved. A formalised system might make the link clearer. Or maybe you’d want to go the other way and say such a system doesn’t presuppose any logic. Either way it should be an interesting exercise. The other reason for doing this is related. I’m interested in Category Theory and I wonder if the formalisation of geometry in this way might make it easier to deal with in Category Theoretic terms.

I don’t know enough about Euclid’s Elements, Logic or Category theory to know whether this is a worthwhile endeavour, but that’s not going to stop me trying it out!

What problems are there with this approach? I don’t want to import more logic or set theory than I need to into the system. In fact, I want to absolutely minimise my commitments in that area. Now obviously a point will have to be a primitive notion here. One way to proceed is to say a line is a defined term; it is a set of points. But what if there were a way to avoid using the idea of a set here? The only interesting lines are straight lines and circles. So perhaps we can treat them separately. But I also want to limit myself to finitary procedures. In other words, every construction must only consist of a finite number of steps. This means that say we have a line going through two points. Then there is no general way to construct a point a third of the way along the line. We still want to be able to say that point is on the line, otherwise the parallel postulate becomes a little awkward (since it rests on the fact that the point is not on the line…)

I’m sure there are many other difficulties. But I’m off to read the first part of the Elements and see if I cant come up with something fun.

I have posted a post regarding Euclid’s fifth postulate but in a somewhat developmental way. you may want to check it out.

http://math4allages.wordpress.com/2009/12/17/parallel-lines-and-transversal/

Guillermo BautistaDecember 17, 2009 at 5:32 am