2
$\begingroup$

There are several well-known axiomatizations of Euclidean plane geometry, the language of which is usually considered to include at least the relations of

  • incidence (point-line, point-segment, or possibly point-circle),
  • betweenness (point-point-point), and
  • congruence (segment-segment).

(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.)

These axiomatizations are complete, so a fortiori 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.

Are there in fact any such theorems?

And if so,

Is there a known 'nice' axiomatization of the incidence geometry of the Euclidean plane, in the language of incidence geometry alone?

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.

Improve this question
$\endgroup$
5
  • $\begingroup$ Theorem (Playfair): Given any line, and any point not on the line, there exists at most one line through that point that does not intersect the given line. This is in the language of incidence geometry, but in Euclid's original axiomatization, it cannot be proved without the parallel postulate, which implicitly talks about congruence (because it refers to right angles). $\endgroup$
    – user21349
    Commented Oct 2, 2012 at 2:53
  • $\begingroup$ @Ben: Good point! I suppose I could edit the original question to refer specifically to systems taking Playfair as an axiom, if anyone thinks the current version is unclear on that. $\endgroup$
    – user1448
    Commented Oct 2, 2012 at 3:10
  • $\begingroup$ @Ian Maxwell: To clarify for us what you're trying to accomplish, I think it might help if you would give us your current best shot at accomplishing such a "nice" axiomatization. It isn't going to be one that works (else you wouldn't have asked the question), but you can discuss why it doesn't work and why you're stuck trying to fix it. $\endgroup$
    – user21349
    Commented Oct 2, 2012 at 3:27
  • $\begingroup$ Do you have in mind only first-order logic? $\endgroup$
    – user21349
    Commented Oct 2, 2012 at 3:33
  • $\begingroup$ I just saw that a very similar question was asked recently by David Feldman. In light of this I wouldn't mind if my question were closed. $\endgroup$
    – user1448
    Commented Oct 3, 2012 at 17:18

0

Reset to default

You must log in to answer this question.