FOM: Re: More Axiomatization of Geometry

[Harvey Friedman]

Response to Simpson 12:41PM 2/4/99.

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

This follows from two well known facts. That the theory of Euclidean plane
geometry is intertranslatable with the theory of real closed fields, and
that the latter is not finitely axiomatizable.

>Yes, we need to hear from experts on axiomatic geometry.

Yes.
>
> > 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.

I agree. But the other axiomatization is algebraic. I like them both, and
both are important for certain purposes. E.g., what if you don't want to
use <?
>
> > 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?
>
Every angle can be trisected. Reverse geometry seems like a very good idea.