FOM: Tarski's elementary geometry
Stephen G Simpson
simpson at math.psu.edu
Wed Feb 17 17:27:08 EST 1999
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
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.
More information about the FOM