FOM: foundations of geometry: axiomatizing `shape'

[Stephen G Simpson]

One of my FOM mantras has been that f.o.m. is the systematic study of
the most basic mathematical concepts.  I have suggested the following
tentative list of basic mathematical concepts: number, shape, set,
function, algorithm, mathematical axiom, mathematical definition,
mathematical proof.

What about `shape'?  This was deliberately vague.  I intended `shape'
as a placeholder, to make sure that f.o.m. (foundations of
mathematics) includes f.o.g. (foundations of geometry), without
insisting in advance on any one particular approach to f.o.g.

We have had several interesting postings by Mic Detlefsen and others
contrasting the numerical and geometrical approaches to f.o.m. in a
historical context.  

Now I think it's time to get more specific in examining the logical
structure of `shape'.  Let's make a start on axiomatizing various
notions of `shape' such as points, lines, circles, curves, triangles,
polygons, regular closed bounded sets, etc., starting from scratch and
not assuming an arithmetical or set-theoretical context.  This will
bear on many foundational questions, including the question of whether
it is or isn't reasonable to base mathematics on one or more concepts
of `shape'.

The literature in this area is not very familiar to me.  Moshe
Machover suggested looking at Wanda Szmielew's books.  In a few days
I'll get them out of the library and report to FOM.

Recently Harvey Friedman 1 Feb 1999 04:52:48 posted some nice
axiomatizations of the complete theory of (R^2,0,1,i,E,=) where E is
the equidistance predicate.  Harvey referred to this theory as
Euclidean plane geometry, and indeed many of the `shapes' studied by
Euclid are available in straightforward definitional extensions of
this theory.  Among the available `shapes' are points, line segments,
circles, triangles, quadrilaterals, etc.  But it would seem that
arbitrary finite polygons are not available in definitional extensions
of Harvey's theory.

Many questions suggest themselves.  I envision an axiomatization or
axiomatizations of one or more notions of `shape' that may exhibit a
fairly high degree of logical strength, in the sense that they may
interpret some fairly strong subsystems of second order arithmetic.
But how strong?  Which subsystems?  My book `Subsystems of Second
Order Arithmetic' <http://www.math.psu.edu/simpson/sosoa/> mentions a
lot of different subsystems, only a handful of which turn out to be
relevant for reverse mathematics.  At this point I have only the
vaguest idea of which subsystems might be relevant for f.o.g. or
reverse geometry.

But this is jumping ahead of ourselves.  The first thing to do is to
come up with some natural axioms for various `shapes'.

Does anyone else think this is a good program?  How about some
follow-up?

-- Steve Simpson