FOM: Tarski's elementary geometry

[Stephen G Simpson]

This is a followup to Harvey Friedman's posting of 1 Feb 1999 04:52:48
giving axiomatizations of the complete theory of (R^2,0,1,i,E,=) where
Exyuv is the equidistance predicate: the distance from x to y equals
the distance from u to v.  Harvey said:

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

A very relevant and interesting paper is Tarski's `What is Elementary
Geometry?', on pages 16-29 of

  The axiomatic method with special reference to geometry and physics, 
  Proceedings of an internation symposium, held at the University of
  California, Berkeley, December 26, 1957-January 4, 1958. / Edited by Leon
  Henkin, Patrick Suppes [and] Alfred Tarski. Amsterdam, North-Holland Pub.
  Co., 1959. xi,488p. illus. 23cm.
  Series: Studies in logic and the foundations of mathematics.

Tarski gives very explicit axioms A1-A13 for the complete theory of
(R^2,E,B,=) where E is as above and B is the betweenness predicate:
Bxyz means that y is on the line segment between x and z.  A13 is a
continuity scheme:

  if there exists u such that for all x and y [ F(x)&G(y) -> Buxy ],
  then there exists v such that for all x and y [ F(x)&G(y) -> Bxvy ].

Let's call this theory T.  Tarski notes that T is complete, decidable,
not finitely axiomatizable, and has an AE (universal-existential)
axiomatization.  He uses methods from Hilbert's Grundlagen der
Geometrie to show that the models of T are given by 2-dimensional
Cartesian space over an arbitrary real-closed field.  He points out
that T is rich enough to discuss basic geometrical properties of
special classes of geometrical figures describable by a fixed finite
number of points: line segments, circles, triangles, quadrangles, etc.
He points out the modifications that are needed for n-dimensional
space, n = 3,4,5,....

Tarski also considers a finitely axiomatizable subsystem T' of T
corresponding to elementary provability by ruler and compass
constructions.  Here A13 is replaced by the single axiom A13': If x
lies inside a circle C and y lies outside C, then the line segment
from x to y intersects C.  Tarski proves that the models of T' are
given by 2-dimensional Cartesian space over an arbitrary Euclidean
field.  He points out that T and T' have the same universal theorems.
He conjectures that T' is undecidable.

He gives the following g.i.i. statement of the situation:

  We know a general mechanical method for deciding whether a given
  elementary geometrical sentence is valid, but we do not, and
  probably shall never know, any such method for deciding whether a
  sentence of this sort is elementarily provable.

Tarski also considers strengthening T by allowing the formulas in A13
to contain quantifiers over arbitrary finite sets.  Call this T''.
(T'' is an example of what I think has sometimes been called a `weak
second-order' theory.)  The models of T'' are given by 2-dimensional
Cartesian space over Archimedean ordered fields.  T'' interprets PA
and is therefore undecidable.

Note that T'' isn't at all the same as my idea in 11 Feb 1999 13:22:27
of trying to give a first-order axiomatization of `shapes' determined
by finite sets of points.  Tarski doesn't really address this idea.
In a footnote, Tarski considers and rejects the familiar idea of
having `second-order' variables range over arbitrary geometrical
figures represented as sets of points.

-- Steve