[FOM] 735: Philosophical Geometry/13

[Harvey Friedman]

In https://mail.google.com/mail/u/0/#sent/158d2b7fa8bed6d2?compose=158d4fb4c047548f
we are working with

TABLE OF CONTENTS

0. DISTANCE DERIVATION IN THE PLANE
http://www.cs.nyu.edu/pipermail/fom/2016-October/020103.html
1. ONE DIMENSIONAL GEOMETRY
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
2. CONTINUUOUS BETWEEN FUNCTIONS
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
3. MIDPOINT FUNCTIONS
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
4. EQUIDISTANCE  http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
5. EXTENDED CATEGORICITY
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
6. EXTENDED FIRST ORDER COMPLETENESS
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
7. BETWEENESS http://www.cs.nyu.edu/pipermail/fom/2016-October/020121.html
http://www.cs.nyu.edu/pipermail/fom/2016-October/020112.html
8. DIRECTED LINE (1 dimension)
https://mail.google.com/mail/u/0/#sent/158d2b7fa8bed6d2?compose=158d4fb4c047548f
9. DIRECTED CIRCLES, TRIANGLES (1 dimension)
10. COORDINATED PLANE
here
11. DIRECTED LINES IN THE PLANE

We have made major progress in two dimensional Philosophical Geometry.

a. We have simplified (and corrected) section 0, where we work over
the actual ordered group of real numbers.
b. We have fully worked out section 10, Coordinated Plane, where we
don't work over the actual ordered group of real numbers, but work
over a primitive continuum, and where the points are taken to be the
ordered pairs of elements of the primitive continuum. We use a
primitive notion of equidistance for the primitive continuum, and a
primitive notion of equidistance for the points.
c. In the course of working out section 10, we have a polished version
of one dimensional Philosophical Geometry based on equidistance.

We have encapsulated ALL of the nontrivial Euclidean plane geometry
into ONE principle for both sections 0 and 10:

*IF POINTS X,Y ARE EACH EQUIDISTANT FROM BOTH POINTS Z.W, THEN THE
MIDPOINT OF X,Y IS EQUIDISTANT FROM BOTH POINTS Z,W.*

The midpoint is defined using coordinates in the obvious way. The
coordinates of the midpoint are the midpoints of the coordinates.

In this posting we restate section 0 and give proofs. In posting 736,
we present the one dimensional equidistance development with proofs.
In posting 737 we treat section 10 based on posting 736.

0. DISTANCE DERIVATION IN THE PLANE
replaces old section 0

We derive the Euclidean distance function D:(R^2)^2 into [0,infinity)
in the plane, in terms of conditions readily seen by the mind's eye,
with the usual ordered group of real numbers taken for granted.

A1. EQUATIONS. D(x,y) = D(y,x) = D((x_2,x_1),(y_2,y_1)),
D((0,0),(0,1)) = 1, D((0,0),2x) = 2D((0,0),x), D((0.0),3x) =
3D((0,0),x).
A2. MONOTONICITY. If |x_1-y_1| <= |z_1-w_1| and |x_2-y_2| <= |z_2-w_2|
then D(x,y) <= D(z,w).
A3. MIDPOINTS. If D(x,z) = D(y,z) and D(x,w) = D(y,w) then
D(x,(z+w)/2) = D(y,(z+w)/2).

Here x,y,z,w are points, which are elements of D^2.

Note that we are not assuming the triangle inequality and we are not
assuming any kind of linearity except doubling and tripling between
the origin and points, as presented in A1.

Fix D:(R^2)^2 into [0,infinity) satisfying conditions A1-A3.

LEMMA 0.1. A3 holds with <= replaced by =. D(x,y) = D((0,0),y-x).
D(2x,2y) = 2D(x,y). D(3x,3y) = 3D(x,y).

Proof: Let |x_1-y_1| <= {z_1-w_1| and |x_2-y_2| <= |z_2-w_2|. By A3,
D(x,y) <= D(z,w). Also |z_1-w_1| <= |x_1-y_1| and |z_2-w_2| <=
|x_2-y_2|. By A2, D(z,w) <= D(x,y). Hence D(x,y) = D(z,w).

By the previous claim, D(2x,2y) = D((0,0),2y-2x) = 2D((0,0),y-x) =
2D(x,y). D(3x,3y) = D((0,0),3y-3x) = 3D((0,0),y-x) = 3D(x,y). QED

LEMMA 0.2. The set S of finite products of the numbers 2,3,1/2,1/3 is
dense in [0,infinity).

Proof: This is well known, but we give a proof. Suppose this set S is
not dense and assume that it is disjoint from the interval (a,b),
where 0 <= a < b. We can assume that this open interval is maximal.
Now 0 < a since S has arbitrarily small elements. Since S is closed
under division and a,b are limit points of S, b/a is also a limit
point of S. Since a is a limit point of S from below, b is also a
limit of S from below, by multiplying by b/a. This contradicts the
choice of the interval (a,b). QED

LEMMA 0.3. The following hold.
i. For all x,y in R^2 and r in S, D(rx,ry) = rD(x,y).
ii. D(x,y) = D((0,0),y-x) = D((0,0),x-y) = D(-x,-y).
iii. For all r >= 0, D((0,0),rx) = rD((0,0),x).
iv. For all r >= 0, D(rx,ry) = rD(x,y).
v. D(x,y) = 0 if and only if x = y.

Proof: By A1, for all x,y in R^2, D(x/2,y/2) = D(x,y)/2 and D(x/3,y/3)
= D(x,y)/3. Now if for all x,y in R^2, D(rx,ry) = rD(x,y) and D(sx,sy)
= sD(x,y), then for all x,y in R^2, D(rsx,rsy) = rsD(x,y). This
establishes i. ii follows from Lemma 0.1.

For iii, write x = (a,b).  We first assume a,b >= 0. Let r >= 0. By
A2, D((0,0),px) <= D((0,0),rx) <= D((0,0),qx) for all 0 <= p <= r <= q
chosen from S. Hence for all 0 <= p <= r <= q chosen from S,
pD((0,0),x) <= D((0,0),rx) <= qD((0,0),x). Therefore D((0,0),rx) =
rD((0,0),x).

For the general case, by Lemma 0.1 we have D((0,0),(ra,rb)) =
D((0,0),(r|a|,r|b|)) = rD((0,0),(|a|,|b|)) = rD((0,0),(a,b)).

For iv, D(rx,ry) = D((0,0),(ry-rx)) = D((0,0),r(y-x)) = rD((0,0),y-x) = rD(x,y).

For v, by Lemma 0.1, D((0,0),(0,0)) = 2D((0,0),(0,0)), and therefore
D((0,0),(0,0) = 0. By Lemma 0.1, D(x,x) = D((0,0),(0,0)) = 0. Now
suppose D(x,y) = 0. By Lemma 0.1, D((0,0),y-x) = 0.  If x not= y then
by iv, D((0,0),1) = (1/y-x)(0) = 0, which is a contradiction. QED

LEMMA 0.4. D is pointwise continuous as a function from R^4 into [0,infinity).

Proof: We first show that D is continuous at all quadruples (a,b,c,d),
a,b,c,d > 0. Let u < D(a,b,c,d) < v. Let r < 1 < s be sufficiently
close to 1. By Lemma 0.3, u < D(ra,rb,rc,rd) < D(a,b,c,d)  <
D(sa,sb,sc,sd). By A2, D is strictly between u,v on (ra,sa) dot
(rb,sb) dot (rc,sc) dot (rd,sd).

Next we show that D is continuous at all quadruples (a,b,c,d). Let t
be a real number so large that (a,b,c,d)+t has all coordinates
strictly positive. By Lemma 0.1, D((a,b,c,d)+t) = D(a,b,c,d). By the
above D is continuous at (a,b,c,d)+t. Let u < D(a,b,c,d) < v. Then u <
D((a,b,c,d)+t) < v, and so D is strictly between u and v on some
nonempty (e,f) dot (g,h) dot (p,q) dot (r,s) containing (a,b,c,d)+t.
By Lemma 0.1, D is strictly between u and v on some nonempty (e-t,f-t)
dot (g-t,h-t) dot (p-t,q-t) dot (r-t,s-t) containing (a,b,c,d). QED

LEMMA. 0.5. D((a,b),(a,c)) = |b-c|. D((a,c),(b,c)) = |a-b|.
D(x,(x+y)/2) = D((x+y)/2,y) = D(x,y)/2.

Proof: By Lemma 0.1, D((a,b),(a,c)) = D((0,0),(0,c-b)). By Lemma 0.3
and A1, D((0,0),(0,c-b)) = |c-b|D((0,0),(0,1)) = |b-c|. The second
equation follows by A1. For the third equation, using Lemma 0.1,
D(x,(x+y)/2) = D((0,0),((y-x)/2) = D((x+y)/2,y) = D((0,0),y-2)/2 =
D(x,y)/2. QED

LEMMA 0.6. xyzw is a usual square in R^2 with diagonals xw and yz if
and only if it is of one of the following two forms:
i. (0,0),(a,b),(b,-a),(a+b,b-a) shifted entirely by some unique (c,d),
where (a,b) not= (0,0).
ii. (0,0),(a,b),(-b,a),(a-b,a+b) shifted entirely by some unique
(c,d), where (a,b) not= (0,0).
x-y, y-w, x-z, z-w all have sets of coordinates of the form {+-a,+-b}.
D(x,y) = D(y,w) = D(x,z) = D(z,w).

Proof: Except for the four term equation at the end, this statement
does not involve D. Items in i,ii are squares by inspection. Any
square is a unique shift of some square starting with some
(0,0),(a,b), (a,b) not= (0,0). There must be exactly two such squares.
The two squares displayed in i,ii are such, and they are different. By
inspection, the set of coordinates of those differences before the
shift by (c,d) are as given. Hence these are also the sets of
coordinates of the differences. By A1 and Lemma 0.1, D(x,y) = D(y,w) =
D(x,z) = D(z,w). QED

LEMMA 0.7. Let xyzw be a usual square in R^2 with diagonals xw and yz.
{u: |x-u} = |w-u|} is the entire line yz. For all u in the closed line
segment yz, D(x,u) = D(w,u). Now let x,w,u be distinct. if |x-u| =
|w-u| and the angle xuw is obtuse, then D(x,u) = D(w,u). For all x
not= w, and all points u, if |x-u| = |w-u| then D(x,u) = D(w,u).

Proof: Let xyzw be as given. By Lemma 0.2, D(x,y) = D(w,y) and D(x,z)
= D(w,z). The second claim is well known.

We now prove by induction on integers n >= 0 that
y,y+(2^-n)(z-y),y+2(2^-n)(z-y),...,y+(2^n)(2^-n)(z-y) = z all have the
same D distance to x and w. The basis case n = 0 is immediate. For the
induction step, note that the new points are midpoints of adjacent
existing points, and so we can simply apply A3. This establishes
density in the closed line segment yz of {u: |x-u| = |w-u|}. Therefore
by Lemma 0.4, for all u in the closed line segment yz, |x-u| = |w-u|.

The next claim follows because given distinct x,w, there is exactly
one square xyzw (up to interchanging y,z), the characterization of the
entire line yz, and that the closed line segment consists of the u on
the entire line yz for which the angle xuw is obtuse.

Now let u lie on the entire line zw but outside the closed line
segment zw. Let v be such that u is the midpoint of x and v. Then
|u-v| = |w-u| and the angle vuw is obtuse. Therefore by the above,
D(v,u) = D(w,u). However, D(v,u) = D(x,u) by Lemma 0.5, and so D(x,u)
= D(w,u). QED.

LEMMA 0.8. D(x,y) = |x-y|.

Proof: Let x,y be given. We can assume that x not= y. Choose z so that
|z-x| = |y-x| and xz is horizontal. We can arrange y not= z by going
in the opposite direction horizontally if required. By Lemma 0.7,
D(z,x) = D(y,x). But by Lemma 0.5, D(x,z) = |x-z| = |y-x|. Hence
D(x,y) = |x-y|. QED

THEOREM 0.9. D obeys A1-A3 if and only if D is Euclidean distance in R^2.

Proof: A1-A3 obviously hold for the Euclidean distance. If D obeys
A1-A3 then D(x,y) = |x-y| by Lemma 0.8. QED

************************************************************************
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 735th 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
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  101/16  12:19PM
719: Large Cardinals and Emulations/22
720: Foundations of Geometry/7  10/2/16  1:59PM
721: Large Cardinals and Emulations//23  10/4/16  2:35AM
722: Large Cardinals and Emulations/24  10/616  1:59AM
723: Philosophical Geometry/8  10/816  1:47AM
724: Philosophical Geometry/9  10/10/16  9:36AM
725: Philosophical Geometry/10  10/14/16  10:16PM
726: Philosophical Geometry/11  Oct 17 16:04:26 EDT 2016
727: Large Cardinals and Emulations/25  10/20/16  1:37PM
728: Philosophical Geometry/12  10/24/16  3:35PM
729: Consistency of Mathematics/1  10/25/16  1:25PM
730: Consistency of Mathematics/2  11/17/16  9:50PM
731: Large Cardinals and Emulations/26  11/21/16  5:40PM
732: Large Cardinals and Emulations/27  11/28/16  1:31AM
733: Large Cardinals and Emulations/28  12/6/16  1AM
734: Large Cardinals and Emulations/29  12/8/16  2:53PM

Harvey Friedman