FOM: Axiomatization of geometry

[Harvey Friedman]

I first want to correct three typos in posting 28':Restatement, 11:47AM
1/29/99. Eliminate "p" in Propositions 2.6, 4.5, and 4.6.

This abstract was motivated by three talks (by three different people) I
have heard over a period of years concerning geometrical reasoning by
diagrams. In these talks, the speakers wish to avoid following the modern
method of reducing plane geometry to algebra, and instead dwell on the
original Greek approach through diagrams. This abstract addresses the
relevant axiomatic issues in efficient mathematical terms - down to its
mathematical essence. Philosophers interested in this topic will probably
want to recast this development somewhat to interface better with various
views of diagrams and diagrammatic reasoning.

I am not an expert in the literature on axiomatic geometry, and
consequently I would appreciate comments on this approach. To what extent
has this topic been addressed in the literature?

AXIOMATIZATION OF EUCLIDEAN PLANE GEOMETRY BASED ON EQUIDISTANCE
by
Harvey M. Friedman
January 30, 1999

It will be convenient to consider Euclidean plane geometry normalized with
two distinguished points 0 and 1. We can think of 0 as the origin (0,0) and
1 as (0,1), and i as (1,0).

In the algebraic approach to geometry, one defines the plane and its
Euclidean metric in the usual first order way in the field of real numbers.
In this way, the first order Euclidean plane geometry (with distinguished 0
and 1) reduces to the first order algebra of real numbers.

Under the geometric approach, we consider structures such as (R^2,0,1,i,E),
where E(x,y,z,w) holds if and only if d(x,y) = d(z,w); i.e., the Euclidean
distance between x and y is the same as the Euclidean distance between z
and w.

We can define the field of real numbers in (R^2,0,1,i,E). In fact, much
more is true. This is almost surely known - but I don't know a reference.

THEOREM 1. The sets definable in (R^2,0,1,,i,E) are exactly the
semialgebraic subsets of R^2. By Tarski, these are also the subsets of R^2
definable in (R,0,1,+,x). The same is true for 0-definable.

(Here definable means definable with any number of parameters. And
0-definable means definable with no parameters).

We also consider interpretability.

THEOREM 2. (R,0,1,+,x) is interpretable in (R^2,0,1,i,E) and vice versa.

According to Tarski, the first order theory of (R,+,x) has a beautiful
axiomatization via the real closed field axioms. For these axioms, it is
customary to add the constants 0,1, and use the following:

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.

Tarski showed that these axioms are complete. Thus a sentence is true in
(R,0,1,+,x) if and only if it is derivable from these axioms.

Think of (R^2,0,1,i,E) as corresponding to the geometric approach to
Euclidean plane geometry, and (R,0,1,+,x) as corresponding to the algebraic
approach to Euclidean plane geometry.

The following question arises. Can we give a similarly elegant and basic
axiomatization of the first order theory of (R^2,0,1,i,E) involving only
R^2,0,1,i,E?

We also consider a related matter. According to Tarski, the real algebraic
numbers are the 0-definable elements of (R,0,1,+,x). But they have a very
algebraic definition (hence the name "real algebraic"): the solutions to
nontrivial polynomials in one variable with integer coefficients. In fact,
this is the usual definition of real algebraic numbers.

Similarly, the 0-definable elements of (R^2,0,1,i,E) are also the real
algebraic numbers. But do they have a very geometric definition? I.e., a
simple definition in (R^2,0,1,i,E)?

NOTE: Of course, the two coordinate functions on R^2 are NOT considered
part of the language of (R^2,0,1,i,E), but equality is taken for granted.
Of course, by Theorem 1, the coordinate functions on R^2 are definable in
(R^2,0,1,i,E).

We take the second matter up, which is considerably easier.

THEOREM 3. Let x in R^2. The following are equivalent:
a) x is 0-definable in (R^2,0,1,i,E);
b) x is 0-definable in (R,0,1,+,x);
c) x is real algebraic (i.e., its components are real algebraic numbers);
d) in (R^2,0,1,i,E), there is a finite set of atomic formulas without
equality which has a unique solution, and x is among the coordinates of
that unique solution.

We can think of any finite set of atomic formulas without equality as a
diagram, with possible degeneracies. If there are n variables, then the
diagram consists of n labeled points where some pairs of pairs of points
are indicated to be of the same distance; i.e., the line segments
connecting them are indicated to be of the same length. (Of course, the
distinguished points 0 and 1 are implicitly part of any diagram). The
degeneracies correspond to the possibility that the n points may not be
distinct.

One can take the point of view that a diagram must decide basic
relationships. E.g., the diagram must be required to be made up of distinct
points. And so we consider

d') in (R^2,0,1,i,E), there is a finite set of atomic formulas without
equality which has a unique solution with all points distinct, and x is
among the coordinates of that unique solution.

The same result applies to d'). Another requirment might be that all
colinearity relationships be identified, and/or that all right angles be
identified, and/or betweeness relationships, and/or left/rightness,
etcetera. None of this makes any difference in the sense that Theorem 3
still holds.

We now come to the first, more delicate matter. It is useful to separate
out what we call quadratic Euclidean plane geometry.

The quadratic real closed field axioms consist of just axioms 1) - 3)
above. Quadratic Euclidean plane geometry consists of the set of all
sentences of (R^2,0,1,i,E) that become provable from the quadratic real
closed field axioms under the obvious translation into (R,0,1,+,x).

One can give reasonably elegant axiomatizations of quadratic Euclidean
plane geometry staying in the language of (R^2,0,1,i,E), which amounts to
axioms corresponding to ruler and compass constructions.

We now come to the main issue of giving a geometric form of axiom scheme 4)
- that every polynomial of odd degree has a root - within the language of
(R^2,0,1,i,E).

We certainly don't want to simulate this axiom scheme 4) directly. E.g.,
odd degree appears to be geometrically meaningless. But we are looking for
a kind of geometric construction principle.

For clarity, we state the scheme somewhat informally. First of all, we want
to appropriately define the midpoint between two points x,y. Note that
there are unique points z,w (or w,z), such that x,y,z,w forms a square with
diagonal x,y (degenerate if and only if x = y). This is defined using
equidistance - the sides are all equal and the two diagonals are equal. The
unique point equidistant to the four corners is the desired midpoint.

Next we define d(x,y) >= d(z,w) as follows. Let p be the midpoint between
x,y. Then d(x,y) >= d(z,w) if and only if there exists u such that d(z,u) =
d(u,w) = d(x,p).

**********
Fix k,n,m >= 1, x,y,z_1,...,z_k in R^2, and a conjunction
A(x,y,z_1,...,z_k,u_1,...,u_n,v_1,...,v_m) of atomic formulas in the
language of (R^2,0,1,i,E) without equality, with at most the distinct
variables shown.

Assume that for all u_1,...,u_n in Dsk(x) there exists unique v_1,...,v_m
in Dsk(y) such that A(x,y,z_1,...,z_k,u_1,...,u_n,v_1,...,v_m). Let
F:Dsk(x)^n into Dsk(y)^m be defined by this unique correspondence. Then for
each i, the distances from 0 to values of F_i form a closed interval. NOTE:
This is formalized using the relation d(0,x) >= d(0,y), which we have
previously defined appropriately. And F_i is the i-th coordinate function
of F.
**********

Note that this is a kind of intermediate value condition for diagrams.

It appears that this is a complete axiomatization of Euclidean plane
geometry. I.e., every sentence true in (R^2,0,1,i,E) is provable from these
axioms and vice versa.