FOM: 79:Axioms for geometry

[Harvey Friedman]

This is a much simplified version of my posting 2/1/99 4:52AM. This posting
is self contained and supersedes it.

**********

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?

AN AXIOMATIZATION OF EUCLIDEAN PLANE GEOMETRY BASED ON DISTANCE COMPARISON
by
Harvey M. Friedman
January 9, 2000

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 reduces to the first
order algebra of real numbers.

Under the geometric approach, we consider structures such as (R^2,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,E). This is done by
equivalence classes of pairs of elements of R^2.
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,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 sets definable in (R^2,E) with only the three
parameters (0,0),(0,1),(1,0)  are exactly the semialgebraic subsets of R^2
presented with rational coefficients, or the subsets of R^2 that are
0-definable in (R,0,1,+,x).

(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,E) and vice versa.

Here, interpretations are allowed to be via equivalence relations of
tuples, which is allowed in a well known general form of interpretability.

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.

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,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,E) involving only
R^2,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.

Fundamental to all aspects of this theory is the concept of **equality
condition**. An equality condition is a formula in the language of (R^2,E)
of the
following special form: a conjunction of one or more atomic formulas of the
form E(x,y,z,w), where x,y,z,w are variables.

We can think of an equality condition in variables x_1,...,x_k as a
Euclidean plane geometric diagram. There are k labled points x_1,...,x_k in
the diagram. There is an indication that for various pairs of points
x_1,...,x_k, we have equality of distance. Thus we could mark the line
segments joining various pairs in such a way that pairs that are to have
the same distance have their line segments marked with the same marking.

Of course, here one must be entirely noncommittal about degeneracies; e.g.,
about which of the x's are equal or
nonequal, which line segments cross or don't cross, which triples of points
are or are not colinear, etcetera.

THEOREM 3. Let x in R^2. The following are equivalent:
a) x is definable in (R^2,E) with parameters (0,0),(1,0),(0,1);
b) x is 0-definable in (R,0,1,+,x);
c) x is real algebraic (i.e., its components are real algebraic numbers);
d) x is a coordinate in some solution of some equality condition in
(R^2,E) with parameters (0,0),(1,0),(0,1) that has at most finitely many
solutions;
e) x is a coordinate in some solution of some equality condition in (R^2,E)
with parameters (0,0),(1,0),(0,1) all of whose solutions are permutations
of each other.

We can alter the notion of equality condition to incorporate various
committments. E.g., we can consider modified equality conditions which
consist of a conjunction of one or more atomic formulas without equality
and the conjunction asserting that all points used  are distinct. This
eliminates the most basic of degeneracies, although there are other
important degeneracies still allowed. Then Theorem 3 still holds.
Furthermore, various other modifications with regard to the elimination of
degeneracies can be made, with the same result.

We now come to the more delicate matter of the complete axiomatization of
geometry in terms of diagrammatic axioms.

For this purpose it is very convenient to use the 4-ary relation
LE(x,y,z,w) on R^2, meaning that the distance between x,y is less than or
equaled to the distance between z,w. This relation can be defined nicely
from E(x,y,z,w). We give such a definition below.

First of all, we want to nicely define the midpoint between two
points x,y. Note that there are 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.

Now we are in a position to define LE(x,y,z,w) as follows. Let p be the
midpoint between
z,w. Then LE(x,y,z,w) if and only if there exists u such that d(x,u) =
d(u,y) = d(z,p).

Since we are now admitting the ordering directly, it is appropriate to
consider ordered fields and real closed fields using <. We assume
familiarity with the usual ordered field axioms. In this context, the real
field axiom 2) is superfluous. Thus in this context, real closed fields are
given by

1) the usual ordered field axioms;
2) every all x >= 0 has a square root;
3) every polynomial of odd degree has a root.

It is very useful to separate out what we call basic Euclidean plane
geometry and quadratic
Euclidean plane geometry.

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

One can give reasonably elegant axiomatizations of basic Euclidean plane
geometry and quadratic Euclidean plane geometry staying within the language
of (R^2,LE). The latter corresponds closely to ruler and compass
constructions. This much is well known.

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

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

For this purpose, we define a comparison condition as the conjunction of
finitely many atomic formulas LE(x,y,z,w), where x,y,z,w are variables.

Let phi(x_1,...,x_n,y_1,...,y_m) be a comparison condition, where n,m >= 0.

I. Suppose phi(x_1,...,x_n,y_1,...,y_m). Then we can adjust y_1,...,y_m so
that phi(x_1,...,x_n,y_1,...,y_m) and the maximum distance from x_1 to the
points y_1,...,y_m is minimized.

Think of x_1 as the center of a closed disk in which the new points
y_1,...,y_m to be constructed are to lie. We want to minimize the radius of
that closed disk.

THEOREM 4. A sentence is true in (R^2,LE) if and only if it is provable
from the axioms of basic Euclidean geometry plus the axiom scheme I.

There are a number of variants of * where related quantities are minimized.
Here are some examples.

II. Suppose phi(x_1,...,x_n,y_1,...,y_m). Then we can adjust y_1,...,y_m so
that phi(x_1,...,x_n,y_1,...,y_m) and the maximum distance from x_1 to the
points x_1,...,x_n,y_1,...,y_m is minimized.

III. Suppose phi(x_1,...,x_n,y_1,...,y_m). Then we can adjust y_1,...,y_m
so that phi(x_1,...,x_n,y_1,...,y_m) and the diameter of y_1,...,y_m is
minimized.

IV. Suppose phi(x_1,...,x_n,y_1,...,y_m). Then we can adjust y_1,...,y_m so
that phi(x_1,...,x_n,y_1,...,y_m) and the diameter of
x_1,...,x_n,y_1,...,y_m is minimized.

Theorem 4 holds for any of I - IV.

**********

This is the 79th in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM
5:Constructions  11/15/97  5:24PM
6:Undefinability/Nonstandard Models   11/16/97  12:04AM
7.Undefinability/Nonstandard Models   11/17/97  12:31AM
8.Schemes 11/17/97    12:30AM
9:Nonstandard Arithmetic 11/18/97  11:53AM
10:Pathology   12/8/97   12:37AM
11:F.O.M. & Math Logic  12/14/97 5:47AM
12:Finite trees/large cardinals  3/11/98  11:36AM
13:Min recursion/Provably recursive functions  3/20/98  4:45AM
14:New characterizations of the provable ordinals  4/8/98  2:09AM
14':Errata  4/8/98  9:48AM
15:Structural Independence results and provable ordinals  4/16/98
10:53PM
16:Logical Equations, etc.  4/17/98  1:25PM
16':Errata  4/28/98  10:28AM
17:Very Strong Borel statements  4/26/98  8:06PM
18:Binary Functions and Large Cardinals  4/30/98  12:03PM
19:Long Sequences  7/31/98  9:42AM
20:Proof Theoretic Degrees  8/2/98  9:37PM
21:Long Sequences/Update  10/13/98  3:18AM
22:Finite Trees/Impredicativity  10/20/98  10:13AM
23:Q-Systems and Proof Theoretic Ordinals  11/6/98  3:01AM
24:Predicatively Unfeasible Integers  11/10/98  10:44PM
25:Long Walks  11/16/98  7:05AM
26:Optimized functions/Large Cardinals  1/13/99  12:53PM
27:Finite Trees/Impredicativity:Sketches  1/13/99  12:54PM
28:Optimized Functions/Large Cardinals:more  1/27/99  4:37AM
28':Restatement  1/28/99  5:49AM
29:Large Cardinals/where are we? I  2/22/99  6:11AM
30:Large Cardinals/where are we? II  2/23/99  6:15AM
31:First Free Sets/Large Cardinals  2/27/99  1:43AM
32:Greedy Constructions/Large Cardinals  3/2/99  11:21PM
33:A Variant  3/4/99  1:52PM
34:Walks in N^k  3/7/99  1:43PM
35:Special AE Sentences  3/18/99  4:56AM
35':Restatement  3/21/99  2:20PM
36:Adjacent Ramsey Theory  3/23/99  1:00AM
37:Adjacent Ramsey Theory/more  5:45AM  3/25/99
38:Existential Properties of Numerical Functions  3/26/99  2:21PM
39:Large Cardinals/synthesis  4/7/99  11:43AM
40:Enormous Integers in Algebraic Geometry  5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees  5/25/99  5:11PM
43:More Enormous Integers/AlgGeom  5/25/99  6:00PM
44:Indiscernible Primes  5/27/99  12:53 PM
45:Result #1/Program A  7/14/99  11:07AM
46:Tamism  7/14/99  11:25AM
47:Subalgebras/Reverse Math  7/14/99  11:36AM
48:Continuous Embeddings/Reverse Mathematics  7/15/99  12:24PM
49:Ulm Theory/Reverse Mathematics  7/17/99  3:21PM
50:Enormous Integers/Number Theory  7/17/99  11:39PN
51:Enormous Integers/Plane Geometry  7/18/99  3:16PM
52:Cardinals and Cones  7/18/99  3:33PM
53:Free Sets/Reverse Math  7/19/99  2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry  8/27/99  3:01PM
57:Fixpoints/Summation/Large Cardinals  9/10/99  3:47AM
57':Restatement  9/11/99  7:06AM
58:Program A/Conjectures  9/12/99  1:03AM
59:Restricted summation:Pi-0-1 sentences  9/17/99  10:41AM
60:Program A/Results  9/17/99  1:32PM
61:Finitist proofs of conservation  9/29/99  11:52AM
62:Approximate fixed points revisited  10/11/99  1:35AM
63:Disjoint Covers/Large Cardinals  10/11/99  1:36AM
64:Finite Posets/Large Cardinals  10/11/99  1:37AM
65:Simplicity of Axioms/Conjectures  10/19/99  9:54AM
66:PA/an approach  10/21/99  8:02PM
67:Nested Min Recursion/Large Cardinals  10/25/99  8:00AM
68:Bad to Worse/Conjectures  10/28/99  10:00PM
69:Baby Real Analysis  11/1/99  6:59AM
70:Efficient Formulas and Schemes  11/1/99  1:46PM
71:Ackerman/Algebraic Geometry/1  12/10/99  1:52PM
72:New finite forms/large cardinals  12/12/99  6:11AM
73:Hilbert's program wide open?  12/20/99  8:28PM
74:Reverse arithmetic beginnings  12/22/99  8:33AM
75:Finite Reverse Mathematics  12/28/99  1:21PM
76: Finite set theories  12/28/99  1:28PM
77:Missing axiom/atonement  1/4/00  3:51PM
78:Qadratic Axioms/Literature Conjectures  1/7/00  11:51AM