MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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

Whether it fulfills your needs or not, you should definitely read A Formal System For Euclid's Elements by Jeremy Avigad, Edward Dean, and John Mumma, in Review of Symbolic Logic, Vol. 2, No. 4, 2009 [there was a discussion of this paper over at Lambda the Ultimate recently].

I would also check out the libraries of Coq, Isabelle, HOL-light and maybe PVS -- they are all based on higher-order logic too, and someone may well have done such a formalization already.

share|cite|improve this answer
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

I thought Hilbert's postulates were a second-order axiomitization of Euclidean geometry, similar to what you are describing.

share|cite|improve this answer
Hilbert's axioms are indeed second-order, because else they couldn't express Archimedes' axiom and non-extendibility. But the core of the axioms is in first-order language, and most proofs of geometric facts only require those first-order axiom. The axiom system I envisaged, on the other hand, would be inherently higher-order, because of the higher order primitive of a congruence mapping that is formalised in it. – Marcos Cramer Feb 12 '11 at 15:07

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.