FOM: More Axiomatization of Geometry

[Stephen G Simpson]

Harvey, I like your results in 1 Feb 1999 04:52:48 concerning complete
axiomatizations of Euclidean plane geometry.  The idea of using
equidistance as a primitive seems nice.

An interesting corollary seems to be that complete Euclidean plane
geometry is not finitely axiomatizable.  Does this indeed follow from
your results?  Was this already known?  I am ignorant of the
background here.

 > To what extent has this topic been addressed in the literature?

Yes, we need to hear from experts on axiomatic geometry.  I seem to
remember that there is some well-known interesting stuff about
division rings corresponding to Desarguesian geometry ....

 > According to Tarski, the first order theory of (R,0,1,+,x) has a
 > beautiful axiomatization via the real closed field axioms:
 > 
 > 1) the usual field axioms;
 > 2) -1 is not the sum of squares;
 > 3) for all x, x or -x is a square;
 > 4) every polynomial of odd degree has a root.

I tend to prefer the following axiomatization of (R,+,-,x,0,1,<,=):

   a) the usual ordered field axioms;

   b) the intermediate value property for polynomials:
      if x<y and f(x)<0<f(y) then there exists z such that
      x<z<y and f(z)=0.

To me this is more elegant and intuitive.

 > One can give reasonably elegant axiomatizations of basic Euclidean
 > plane geometry and quadratic Euclidean plane geometry staying
 > within the language of (R^2,0,1,i,E). The latter corresponds
 > closely to ruler and compass constructions.

Are there any classical theorems of Euclidean plane geometry that
aren't provable from these axioms?  Is there any possibility of
"reverse geometry" here, i.e. showing that certain geometrical
theorems are equivalent (over basic or quadratic Euclidean plane
geometry) to the axioms needed to prove them?

-- Steve