most recent 30 from http://mathoverflow.net 2013-06-18T21:11:37Z http://mathoverflow.net/feeds/question/20709 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/20709/higher-order-axiomatisations-of-euclidean-geometry Marcos Cramer 2010-04-08T11:30:08Z 2011-02-12T02:49:14Z

<p>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). </p> <p>$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}.</p> <p>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).</p> <p>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.</p> <p>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?</p>

http://mathoverflow.net/questions/20709/higher-order-axiomatisations-of-euclidean-geometry/20725#20725 Jacques Carette 2010-04-08T13:46:38Z 2010-04-08T13:46:38Z

<p>Whether it fulfills your needs or not, you should definitely read <a href="http://journals.cambridge.org/repo_A674ohNM" rel="nofollow">A Formal System For Euclid's Elements</a> by Jeremy Avigad, Edward Dean, and John Mumma, in Review of Symbolic Logic, Vol. 2, No. 4, 2009 [there was <a href="http://lambda-the-ultimate.org/node/3899" rel="nofollow">a discussion of this paper</a> over at <a href="http://lambda-the-ultimate.org/" rel="nofollow">Lambda the Ultimate</a> recently].</p> <p>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.</p>

http://mathoverflow.net/questions/20709/higher-order-axiomatisations-of-euclidean-geometry/55177#55177 none 2011-02-12T02:49:14Z 2011-02-12T02:49:14Z

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