[FOM] 718: Foundations of Geometry/6

Sat Oct 1 12:19:17 EDT 2016

In http://www.cs.nyu.edu/pipermail/fom/2016-September/020096.html, we
gave a characterization of Euclidean geometry taking the reals as
given, with points as ordered pairs of reals. We used lines, 90 degree
counterclockwise rotation, and distance.

We now want to accomplish the same thing, only this time without lines
or 90 degree counterclockwise rotation. Just reals, points as ordered
pairs, and distance.

A1. D is poinrtwise continuous. D(x,(x+y)/2) = D(x,y)/2.
D((a,b),(a,c)) = |b-c|. 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 (x+w)/2 = (y+z)/2 and D(x,y) = D(z,w) and
D(x,z) = D(y,w) and D(x,w) = D(y,z). Then the same holds for
x,(x+y)/2,z,(z+w)/2, and for x,2y-x,z,2w-z.

We write (x+w)/2 = (y+z)/2 instead of s+w = y+z only because we want
to emphasize the midpoint construction, which also occurs in the
consequent of A2.

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

The first statement of A1 asserts obvious symmetries of D, and that D
is nonnegative. The second statement asserts that midpoints halve
distances. The third asserts that distance between points is strictly
monotone in the   distances between coordinates.

For A2, the condition 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, the midpoint of xw is the same as the
midpoint of yz, and the two diagonals xw and yz are of the same
length,

then

the same properties hold if we replace y,w with midpoints
(x+y)/2,(z+w)/2, or with midpoints 2y-x,2w-z.

The above expresses the following intuition. If the property holds
then x,y,z,w form a rectangle. And if we make the indicated
replacements in x,y,z,w, it still forms a rectangle. Therefore after
these replacements in x,y,z,w, the property still holds.

NOTE: As simple as A1,A2 are, we are looking at a couple of
opportunities for further simplification under the same setup.
Similarly for the axiomatizations below.

We now want to move in two directions. One is Second Order
Axiomatizations, where we no longer take R for granted, but we have a
sort for R. The second eliminates the sort for R entirely, and is
purely geometric.

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

Here we can either use two sorts, R, P (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 halving.
A2. (x_1,x_2) = x. (a,b)_1 = a, (a,b)_2 = b.
A3. D is poinrtwise continuous. D(x,(x+y)/2) = D(x,y)/2.
D((a,b),(a,c)) = |b-c|. 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 (x+w)/2 = (y+z)/2 and D(x,y) = D(z,w) and
D(x,z) = D(y,w) and D(x,w) = D(y,z). Then the same holds for
x,(x+y)/2,z,(z+w)/2, and for x,2y-x,z,2w-z.

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. <,+,x 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.

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

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_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 halving.
A2. (x_1,x_2) = x. (a,b)_1 = a, (a,b)_2 = b.
A3. D is poinrtwise continuous. D(x,(x+y)/2) = D(x,y)/2.
D((a,b),(a,c)) = |b-c|. 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 (x+w)/2 = (y+z)/2 and D(x,y) = D(z,w) and
D(x,z) = D(y,w) and D(x,w) = D(y,z). Then the same holds for
x,(x+y)/2,z,(z+w)/2, and for x,2y-x,z,2w-z.

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,<,+,x with 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 718th 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

Harvey Friedman