# Higher-order axiomatisations of Euclidean Geometry?

I am currently thinking about the possibility to axiomatise Euclidean Geometry using higher-order axioms. The idea is that all objects are points, and that we only have two primitive notions: A three place predicate for betweenness, and a one-place third-order predicate indicating whether a function from a set of points to another set of points is a congruence mapping (so the existence of such a function between two given sets means that the sets are congruent in the intuitive way; the function maps points from the first set to corresponding points of the set congruent to it).

$ab \equiv cd$ can then be defined to mean that there is a congruence mapping from {a,b} to {c,d}. The line through a and b can be defined to be {p|p is between a and b or a is between p and b or b is between p and a} $\cup$ {a,b}.

Using these two primitive notions of betwenness and congruence mappings, it seems to me that quite a short and simple list of axioms can specify Euclidean Geometry: Three simple betweenness properties, one completeness axiom (similar to that for $\mathbb{R}$, but using the betweenness relation rather than the less-than relation), one axiom ensuring the existence of enough congurence mappings, one axiom ensuring that relations between points are preserved by congurence mappings, and two axioms specifying the dimension of the space (one for the lower bound on the dimension, another for the upper bound).

My interest in such an axiomatisation is mainly philosophical: The two primitive notions correspond to concepts from our natural intuition and expirience of space (congruence mappings correspond to moves of an object in space without the shape of the object changing). The axiomatisation seems simpler than first-order axiomatisations like those of Hilbert and Tarski. And the higher-order nature of the system makes it possible to define lines, circles, triangle, quadrilaterals and any other shapes, which is not possible in first-order systems.

I have an idea for a proof that my axiomatisation specifies a space isomorphic to $\mathbb{R}^n$ (for the $n$ used in the dimension axioms); but before I actually work out the proof, I want to know whether a comparable higher-order axiomatisation of Euclidean Geometry already exists. Unfortunately, I couldn't find any higher-order axiomatisations of Euclidean Geometry. Does anyone know about such axiomatisations or attempts at them?

-
How are functions specified? Will your logic include the lambda-calculus (e.g., is a Henken-like calculus)? Do you want to have, say, all linear transformations? –  Charles Stewart Apr 8 '10 at 12:08
The logical system that I would use for formalising my ideas is Church's Type Theory. But other systems for higher-order logic might also do the job. At any rate, I am interested in existing axiomatisations in any system of higher-order logic, not just in the Church's Type Theory. –  Marcos Cramer Apr 8 '10 at 13:29
Why do you need the third order congruence predicate? It would seem that if you merely had a first order 4-ary predicate for congruence of line segments, then you would in effect have access to the metric, and you could express any kind of congruence in terms of it. –  Joel David Hamkins Apr 8 '10 at 15:29
One reason for the third-order congruence predicate is that it makes it easy to express the following very powerful axiom: Given a set of points M, distinct points a,b in M, and distinct points c,d, there is a unique set N of points such that there is a congruence mapping f from M to N such that f(a)=c and a is between d and b. This intuitive axiom corresponds a lot to the cutting down of the number of axioms needed. Additionally, congruence between arbitrary set seems to me a very basic concept of our intuitions about space. Congruence between pairs of points is just a special case of this. –  Marcos Cramer Apr 8 '10 at 19:50
Marcos, I'm not sure you stated the axiom you intended. But suitably corrected, I like it. My point, however, was that it seems to be second-order expressible, rather than third order, as long as you have a (first-order) way to say that line segments are congruent. That is, you could introduce your congruence predicate as a defined property of a set of pairs, state your axiom using it, and end up with a second-order axiomatization overall instead of third order. –  Joel David Hamkins Apr 8 '10 at 22:27

My work on Avigad's formal system is actually what originally got me thinking about the topic. Avigad's axiomatization is, however, a first-order axiomatization with a large number of axioms, so very much unlike what I am currently thinking about. Thanks for the idea to check out the libraries of Coq etc. I have just done this: the only things I found were a formalisation of Tarski's first-order theory in Coq, and a type-theoretic formalisation of $\mathbb{R}^n$ (for arbitrary n) in HOL-light (whereas I am thinking about a theory which doesn't depend on having defined the real numbers). –  Marcos Cramer Apr 8 '10 at 19:37