most recent 30 from http://mathoverflow.net 2013-05-22T11:48:48Z http://mathoverflow.net/feeds/question/108588 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/108588/axiomatization-of-the-incidence-geometry-of-the-euclidean-plane Ian Maxwell 2012-10-02T01:31:30Z 2012-10-02T01:31:30Z

<p>There are several well-known axiomatizations of Euclidean plane geometry, the language of which is usually considered to include at least the relations of</p> <ul> <li>incidence (point-line, point-segment, or possibly point-circle),</li> <li>betweenness (point-point-point), and</li> <li>congruence (segment-segment).</li> </ul> <p>(One could define incidence in terms of betweenness---Tarski does this, for example---but I'm interested in the case where these are distinct primitives.)</p> <p>These axiomatizations are complete, so <em>a fortiori</em> they generate a complete theory in the language of incidence geometry. But on the face of it, there may be theorems of Euclidean plane geometry whose statements are in the language of incidence geometry, but which cannot be proven without appeal to axioms involving betweenness or congruence.</p> <blockquote> <p>Are there in fact any such theorems?</p> </blockquote> <p>And if so,</p> <blockquote> <p>Is there a known 'nice' axiomatization of the incidence geometry of the Euclidean plane, in the language of incidence geometry alone?</p> </blockquote> <p>I'm not sure how to formalize what I mean by 'nice.' Essentially I want to exclude such answers as "the set of all theorems of Euclidean geometry in the language of incidence geometry," which is a recursively enumerable set but seems like a bit of a cop-out.</p>