[FOM] 737: Philosophical Geometry/15
Harvey Friedman
hmflogic at gmail.com
Thu Dec 22 15:24:12 EST 2016
We have just realized that DISTANCE DERIVATION IN THE PLANE
http://www.cs.nyu.edu/pipermail/fom/2016-December/020190.html can be
further simplified by relying on the ordinary notion of line in R^2.
This is appropriate because in Distance Derivation the idea is to
determine D(x,y) on the actual R^2 by simple conditions.
The version in http://www.cs.nyu.edu/pipermail/fom/2016-December/020190.html
does NOT rely on lines.
With LINES is now SO SIMPLE that I would expect this or something
CLOSE to this to be KNOWN. We are looking into leveraging this new 2.1
and 1.10 to do something particularly simple for 2.2 in a further
posting.
OUTLINE
with links
PHILOSOPICAL GEOMETRY
1. ONE DIMENSIONAL PHILOSOPHICAL GEOMETRY
1.1. ONE DIMENSIONAL GEOMETRY
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
1.2. CONTINUOUS BETWEEN FUNCTIONS
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
1.3. MIDPOINT FUNCTIONS
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
1.4. EQUIDISTANCE
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
1.5. EXTENDED CATEGORICITY
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
1.6. EXTENDED FIRST ORDER COMPLETENESS
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html
1.7. BETWEENESS
http://www.cs.nyu.edu/pipermail/fom/2016-October/020121.html
http://www.cs.nyu.edu/pipermail/fom/2016-October/020112.html
1.8. DIRECTED LINE (1 dimension)
https://mail.google.com/mail/u/0/#sent/158d2b7fa8bed6d2?compose=158d4fb4c047548f
1.9 DIRECTED CIRCLES, TRIANGLES (1 dimension)
1.10. EQUIDISTANCE REVISITED (1 dimension)
http://www.cs.nyu.edu/pipermail/fom/2016-December/020191.html
2. TWO DIMENSIONAL PHILOSOPHICAL GEOMETRY
2.1. DISTANCE DERIVATION IN THE PLANE
here
2.2. DISTANCE COMPARISON IN THE PLANE
2.1. DISTANCE DERIVATION IN THE PLANE
augments http://www.cs.nyu.edu/pipermail/fom/2016-December/020190.html
We now 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, and
the usual notion of LINES in R^2.
A1. NORMALITY. D(x,y) = D((x_2,x_1),(y_2,y_1)), D((0,0),(r,0)) = |r|..
A2. COORDINATES. 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. EQUIDISTANCE. For x not= y, {z: D(z,x) = D(z,y)} is a line.
Here x,y,z,w are points, which are elements of D^2. In A3 we mean
lines in R^2 in the usual sense.
We can use collinearity between three points instead of directly
talking about lines. This is worth mentioning as collinearity can be
defined algebraically without directly mentioning lines. See Lemma
2.1.2, claim 2.
A3'. EQUIDISTANCE'. For x not= y, if D(u,x) = D(u,y), D(v,x) = D(v,y),
D(w,x) = D(w,y), then u,v,w are collinear.
A3,A3' look equivalent over A1,A2, but there is a subtlety. We need to
show in A1,A2 that there are at least two z such that D(z,x) = D(z,y).
See Lemma 2.1.2.
Note that we are not assuming the triangle inequality or any kind of linearity.
Fix D:(R^2)^2 into [0,infinity) satisfying conditions A1-A3. We use |
| for the usual Euclidean distance on R^2 (and absolute value on R).
LEMMA 2.1.1. D(x,y) = D(y,x) = D((0,0),y-x) = D(-x,-y). D((a,b),(a,c)) = |b-c|.
LEMMA 2.1.2. Let (a,b) not= (0,0) be given. The distinct points
((a+b)/2,(b-a)/2) and (a/2,b/2) both have the same distance and the
same D distance to (a,b) and (0,0). For any two points, there are at
least two points equidistant to both.The line of points Euclidean
equidistant to (a,b) and (0,0) is the same as the line of points D
equidistant to (a,b) and (0,0).
Proof: Subtract respective coordinates and see by inspection that we
can apply A2. If those two points are equal then we easily derive a =
b = 0.
Now let x not= y. By the first claim there exists at least two points
equidistant to (0,0) and y-x. Adding x to all four points maintains
this equidistance. QED
Note that for the first two claims of Lemma 2.1.2, we have only used A1,A2.
LEMMA 2.1.3. Let x = (a,b) not= 0, b not= 0, y = (a+D((0,0),(a,b)),b).
The line of points D equidistant from (0,0) and y includes x,
D((0,0),x) = |x|.
Proof: The first claim is by A2 and Lemma 2.1.1. By Lemma 2.1.2, x is
Euclidean equidistant from (0,0) and y. But the Euclidean distance
from x to y is the same as the D distance from x to y (Lemma 2.1.1),
and hence the Euclidean distance from x to (0,0) is the same as the D
distance from x to (0,0). QED
THEOREM 2.1.4. D:(r^2)^2 into [0,infinity) obeys A1-A3 if and only if
D is Euclidean distance in R^2.
Proof: A1-A3 obviously hold for the Euclidean distance. Suppose D
obeys A1-A3. By Lemma 2.1.3, if x_2 not= 0 then D((0,0),x) = |x| by
Lemma 2.1.3. If x_2 = 0 then D((0,0),x) = |x_1| by A1 and Lemma 2.1.1.
D(x,y) = D((0,0),y-x) = |y-x| using Lemma 2.1.1. QED
In http://www.cs.nyu.edu/pipermail/fom/2016-December/020190.html we
avoided D((0,0),(r,0)) = |r| in favor of D((0,0),2x) = 2D((0,0),x) and
D((0,0),3x) = 3D((0,0),3x). The cost that was paid was using
MONOTONICITY instead of the simpler COORDINATES here.
************************************************************************
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 737th 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
735: Philosophical Geometry/13 12/19/16 4:24PM
736: Philosophical Geometry/14 12/20/16 12:43PM
Harvey Friedman
More information about the FOM
mailing list