[FOM] 720: Foundations of Geometry/7

[Harvey Friedman]

Recall that this is PHILOSOPHICAL GEOMETRY, where we investigate what
is in the mind's geometric eye.

In http://www.cs.nyu.edu/pipermail/fom/2016-October/020100.html when
we intuitively explained A1, we mistakenly were explaining a previous
but discarded version of A1. Also sometimes I wrote x to indicate
multiplication, and x should instead be -.

In any case, we now substantially simplify
http://www.cs.nyu.edu/pipermail/fom/2016-October/020100.html, where we
remove some conditions and axioms.

1. CHARCTERIZATION

We characterize D:R^2 into R, intended as the intuitive distance
function between points in the intuitive plane.

A1. D:R^2 into R is pointwise continuous. D((0,0),(0,a)) = |a|. If
{|x_1 - y_1|, |x_2 - y_2|} = {|z_1 - w_1|,
|z_2 - w_2|} then D(x,y) = D(z,w).

A2.  Let x,y,z,w be such that D(x,y) = D(z,w), D(x,z) = D(y,w), D(x,w)
= D(y,z). Then the same holds for x,(x+y)/2,z,(z+w)/2.

THEOREM 1.1. D obeys A1,A2 if and only if D is Euclidean distance in R^2.

The first statement of A1 is stated in the usual epsilon/delta manner
with the coordinates. I.e.,

for all x,y in R^2 and reals epsilon > 0, there exists real delta > 0
such that for all z,w in R^2, if |x_1 - y_1|, |x_2 - y_2| < delta,
then D(x,y) < epsilon.

The third statement in A1 says that the distance between any two
points depends only on the at most two element set consisting of the
magnitude of the difference between their first coordinates, and the
magnitude of the difference between their second coordinates.

A2 asserts that for x,y,z,w, if

the two sides xy and zw are of the same length, the two sides xz and
yw are of the same length, and the diagonals xw and yz are of the same length

then

the same holds with y,w replaced by the midpoints (x+y)/2,(z+w)/2.

The above expresses the following intuition. If the property holds for
x,y,z,w then x,y,z,w forms a rectangle. And then if we cut it evenly
in half using the indicated midpoints, it remains a rectangle. Also
rectangles are characterized by the property for x,y,z,w.

2. SECOND ORDER AXIOMATIZATION
with a sort for real numbers
with and and without a sort for points

Here we can either use two sorts, R, P (R for reals, P for points), or
we can use
one sort R. Obviously using R,P has the advantage that we don't have
to refer to points in terms of their coordinates, but we need some
obvious axioms relating R and P. We begin with the version using R,P.

1. Sorts R,P.
2. <,+,-,| |, and halving on R.
3. x_1,x_2 for coordinates of points x. (a,b) for the point with
coordinates a,b.
4. D taking two points and returning a real.

A1. The usual ordered group axioms for R,<,+,- with | | and halving.
A2. (x_1,x_2) = x. (a,b)_1 = a, (a,b)_2 = b.
A3. D is poinrtwise continuous. D((0,0,(0,a)) = |a|. If {|x_1 - y_1|,
|x_2 - y_2|} = {|z_1 - w_1|,
|z_2 - w_2|} then D(x,y) = D(z,w).
A4. Let x,y,z,w be such that D(x,y) = D(z,w), D(x,z) = D(y,w), D(x,w)
= D(y,z). Then the same holds for x,(x+y)/2,z,(z+w)/2.

S1. Every nonempty set of reals with an upper bound has a least upper bound.

Here is the version with only one sort, R.

1. Sort R.
2. <,+,- and halving on R.
3. 4-ary distance function D(a,b,c,d), representing the distance
between (a,b) and (c,d).

A1. The usual ordered group axioms for R,<,+,x with halving.
A2. A3 above. State everything in terms of coordinates.
A3. A4 above. State everything in terms of coordinates.

S1. As above.

THEOREM 2.1. Both systems above are categorical. All models of the first
system are isomorphic to the model (R,R^2,<,+,-,| |,halving,first
coordinate function,second coordinate function,ordered pair,Euclidean
distance). All models of the second system are isomorphic to the model
(R,<,+,-,| |,halving,Euclidean distance).

3. FIRST ORDER AXIOMATIZATION
with a sort for real numbers
both with and without a sort for points

1. Sorts R,P.
2. <,+,-,| |, and halving on R.
3. x_],x_2 for coordinates of points x. (a,b) for the point with
coordinates a,b.
4. D taking two points and returning a real.

A1. The usual ordered group axioms for R,<,+,- with | | and halving.
A2. (x_1,x_2) = x. (a,b)_1 = a, (a,b)_2 = b.
A3. D is poinrtwise continuous. D((0,0,(0,a)) = |a|. If {|x_1 - y_1|,
|x_2 - y_2|} = {|z_1 - w_1|,
|z_2 - w_2|} then D(x,y) = D(z,w).
A4. Let x,y,z,w be such that D(x,y) = D(z,w), D(x,z) = D(y,w), D(x,w)
= D(y,z). Then the same holds for x,(x+y)/2,z,(z+w)/2.

S1. (Scheme). Every definable set of reals with an upper bound has a
least upper bound. Here definability is in the full language, and
allows parameters.

Here is the version with only one sort, R.

1. Sort R.
2. <,+,-,| |, and halving on R.
3. 4-ary distance function D(a,b,c,d), representing the distance
between (a,b) and (c,d).

A1. The usual ordered group axioms for R,<,+,- with | | and halving.
A2. A3 above. State everything in terms of coordinates.
A3. A4 above. State everything in terms of coordinates.

S1. (Scheme). Every definable set of reals with an upper bound has a
least upper bound. Here definability is in the full language, and
allows parameters.

THEOREM. Both first order systems above are complete in their
language. The systems are mutually interpretable with the theory of
real closed fields.

***********************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 720th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-699 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

700: Large Cardinals and Continuations/14  8/1/16  11:01AM
701: Extending Functions/1  8/10/16  10:02AM
702: Large Cardinals and Continuations/15  8/22/16  9:22PM
703: Large Cardinals and Continuations/16  8/26/16  12:03AM
704: Large Cardinals and Continuations/17  8/31/16  12:55AM
705: Large Cardinals and Continuations/18  8/31/16  11:47PM
706: Second Incompleteness/1  7/5/16  2:03AM
707: Second Incompleteness/2  9/8/16  3:37PM
708: Second Incompleteness/3  9/11/16  10:33PM
709: Large Cardinals and Continuations/19  9/13/16 4:17AM
710: Large Cardinals and Continuations/20  9/14/16  1:27AM
711: Large Cardinals and Continuations/21  9/18/16 10:42AM
712: PA Incompleteness/1  9/2316  1:20AM
713: Foundations of Geometry/1  9/24/16  2:09PM
714: Foundations of Geometry/2  9/25/16  10:26PM
715: Foundations of Geometry/3  9/27/16  1:08AM
716: Foundations of Geometry/4  9/27/16  10:25PM
717: Foundations of Geometry/5  9/30/16  12:16AM
718: Foundations of Geometry/6  10/1/16  12:19AM
719: Large Cardinals and Emulations/22  10/216  1:59AM

Harvey Friedman