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?