[FOM] 738: Philosophical Geometry/16
Harvey Friedman
hmflogic at gmail.com
Tue Dec 27 18:54:07 EST 2016
We rework section 2.1 below.
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
http://www.cs.nyu.edu/pipermail/fom/2016-December/020190.html
http://www.cs.nyu.edu/pipermail/fom/2016-December/020195.html
and reworked and augmented here.
2.1.1. Multiplicative equidistance.
2.1.2. Additive equidistance.
2.1.3. Triangle inequality.
2.2. DISTANCE COMPARISON IN THE PLANE
##############################
2.1. DISTANCE DERIVATION IN THE PLANE
augments and replaces
http://www.cs.nyu.edu/pipermail/fom/2016-December/020190.html
http://www.cs.nyu.edu/pipermail/fom/2016-December/020195.html
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
looking at the static plane.
Here we are thinking of the plane as ordered pairs of real numbers,
where the real numbers are not analyzed, but rather taken as given
with its ordered group structure - and sometimes its ordered ring
structure.
In order to characterize the Euclidean D we need a single powerful
condition - the Equidistance Condition - along with what we
collectively call Infrastructure Conditions.
The Equidistance Condition naturally takes on several forms. Here we
use two forms. Each asserts that for any points x,y, the points y for
which D(y,x) = D(y,-x) obey a closure condition. The stronger
condition uses real multiplication (scalar multiplication), where the
weaker condition uses real addition. The former is used in section
2.1.1 and the latter is used in section 2.1.2.
The Triangle Inequality is not so vivid in the mind's eye when looking
at the static plane. However, if one considers motion in the plane in
its most basic form, then the Triangle Inequality is arguably vivid.
At this stage in Philosophical Geometry we are in no position to take
detailed positions on the merits and demerits of many basic
conditions. So we revisit distance derivation in the plane in the
context of the Triangle Inequality in section 2.1.3.
2.1.1. MULTIPLICATIVE EQUIDISTANCE.
Let D:(R^2)^2 into [0,infinity).
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 (dot). D(y,x) = D(y,-x) implies D(ry,x) = D(ry,-x), r in R.
Fix D:(R^2)^2 into [0,infinity) satisfying conditions A1-A3. We use |
| for the usual Euclidean norm on R^2. For x not= y in R^2, L(x,y) is
the entire line through x and y.
LEMMA 2.1.1.1. D(x,y) = D(y,x) = D((0,0),y-x). D((a,b),(a,c)) = |b-c|.
Proof: By subtracting coordinates and applying A1, A2. QED
LEMMA 2.1.1.2. |y-x| = |y+x| implies D(y,x) = D(y,-x).
Proof: We first claim that (b,-a) is D equidistant to (a,b) and
-(a,b). By subtracting coordinates, we get b-a, -a-b with (a,b), and
b+a, b-a with -(a,b), up to sign change. Apply A1,A2.
Now let |y-x| = |y+x|. Let x = (a,b). From standard Euclidean
geometry, the set of such y is the line through (0,0) and (b,-a).
Hence y is some r(b,-a). By the first claim, D((b,-a),x) =
D((b,-a),-x). By A3, D(r(b,-a),x) = D(r(b,-a),-x), and so D(y,x) =
D(y,-x). QED
LEMMA 2.1.1.3. |z-x| = |z-y| implies D(z,x) = D(z,y).
Proof: Let |z-x| = |z-y|. Then |w-(x-y)/2| = |w-(y-x)/2|, where w = z
- x + (x-y)/2. By Lemma 2.1.1.2, D(w,(x-y)/2) = D(w,(y-x)/2). By Lemma
2.1.1.1, D(z-x,(0,0)) = D(z-y,(0,0)), D(z,x) = D(z,y). QED
LEMMA 2.1.1.4. |x| = D(x,(0,0)). D(x,y) = |x-y|.
Proof: Let x = (a,b). Then x is equidistant to (a+|x|,b) and (0,0) by
standard Euclidean geometry. By Lemma 2.1.1.3, x is D equidistant to
(a+|x|,b) and (0,0). But D(x,(a+|x|,b)) = |x| by Lemma 2.1.1.1. Hence
|x| = D(x,(0,0)).
D(x,y) = D(x-y,(0,0)) = |x-y| by Lemmas 2.1.1.1, 2.1.1.2 and the first
claim. QED
THEOREM 2.1.1.5. D:(R^2)^2 into [0,infinity) satisfies conditions
A1-A3 if and only if D is the usual Euclidean distance in R^2.
Proof: By Lemma 2.1.1.4 and that the usual Euclidean distance D in R^2
obeys conditions A1-A3. QED
2.1.2. ADDITIVE EQUIDISTANCE
Here we will avoid any use of multiplication in favor of addition -
and even very limited uses of addition.
B1. NORMALITY. D(x,y) = D((x_2,x_1),(y_2,y_1)), D((0,0),(r,0)) = |r|.
B2. 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).
B3. CONTINUITY. If D(x,y) lies in nonempty open interval (a,b) then
all values of D on some Cartesian product of four open intervals
containing (x,y) in R^4 lie in (a,b).
B4. EQUIDISTANCE (2,1/3). If D(y,x) = D(y,-x) then D(2y,x) = D(2y,-x)
and D(y/3,x) = D(y/3,-x).
Let D:(R^2)^2 into [0,infinity) satisfy B1-B4.
Of course B4 has artificiality, but the main point is that it is
clearly vivid in the mind's eye. A3 involves a clearly more intensive
use of real numbers through scalar multiplication.
The proof of Lemma 0.2 in
http://www.cs.nyu.edu/pipermail/fom/2016-December/020190.html was not
entirely correct. We now prove a stronger result this time correctly.
LEMMA 2.1.2.1. Let S be the least subset of R containing 2, 1/3, and
closed under multiplication. 1 is not in S. 1 is a limit point of S. S
is dense in [0,infinity).
Proof: The elements of S are the numbers 2^n/3^m where n,m are
nonnegative integers which are not both 0. Note that 2^n = 3^m is
impossible for such n,m by divisibility considerations. Hence 1 is not
in S.
We now prove that 1 is a limit point of S. Suppose not, and let (a,b)
be disjoint from S where a < 1 < b. Since S contains arbitrarily small
and arbitrarily large positive reals, clearly 0 < a < 1 < b <
infinity. Let (c,d) be an inclusion maximal interval containing (a,b)
disjoint from S. Again, 0 < c < 1 < d < infinity. Now c < cd < d, and
so c,d are not both in S. Suppose d notin S. Then d is a limit point
of S from the right and we can choose q > d from S and p <= c, where q
is so close to d and p is so close to c, that c < cq < d, which is a
contradiction. Suppose c notin S. Then c is a limit point of S from
the left and we can choose p < c from S and q >= d from S, where p is
so close to c and q is so close to d that c < pd < d, which is also a
contradiction.
Now assume S is not dense in [0,infinity) and let (a,b) be disjoint
from S. Again we can extend (a,b) to a maximal (c,d) disjoint from S,
and we have 0 < c < d < infinity.
case 1. 1 is a limit point of S from the left. If d in S then by
multiplying by d we obtain an element of S in (c,d), which is a
contradiction. So d is a limit point of S from the right, and we can
again multiply to obtain an element of S in (c,d), a contradiction.
case 2. 1 is a limit point of S from the right. If c in S then by
multiplying by c we obtain an element of S in (c,d), which is a
contradiction. So c is a limit point of S from the left, and we can
again multiply to obtain an element of S in (c,d), a contradiction.
QED
Below we use the set S of Lemma 2.1.2.1.
LEMMA 2.1.2.2. D(x,y) = D(y,x) = D((0,0),y-x). D satisfies A3 =
Equidistance (dot).
Proof: The equations require only B1,B2, as can be seen from the proof
of Lemma 2.1.1.1. Now let x be given and suppose D(y,x) = D(y,-x). Let
T be the least subset of R^2 containing y and closed under
multiplication by 2, 1/3. By B4, for all y in T, D(y,x) = D(y,-x).
Note that T is the set of all ry, r in S U {1}. By Lemma 2.1.2.1, T is
dense in the closed ray {ry: r >= 0}. Hence by the continuity of D, we
see that D(y,x) = D(y,-x) holds for all y in this closed ray. Now
D(y,x) = D(y,-x) = D(-y,x) = D(-y,-x) holds just from B1,B2. Hence we
have D(ry,x) = D(ry,-x) for all r in R. QED
THEOREM 2.1.2.3. D:(R^2)^2 into [0,infinity) satisfies conditions
B1-B4 if and only if D is the usual Euclidean distance in R^2.
Proof: By Lemma 2.1.2.2, Theorem 2.1.1.5, and that the usual Euclidean
distance in R^2 satisfies B1-B4. QED
2.1.3. TRIANGLE INEQUALITY
C1. NORMALITY. D(x,y) = D((x_2,x_1),(y_2,y_1)), D((0,0),(r,0)) = |r|.
C2. 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).
C3. TRIANGLE INEQUALITY. D(x,y) <= D(x,z) + D(z,y).
C4. EQUIDISTANCE (2,1/3). If D(y,x) = D(y,-x) then D(2y,x) = D(2y,-x)
and D(y/3,x) = D(y/3,-x).
Let D:(R^2)^2 into [0,infinity) satisfy C1-C4.
LEMMA 2.1.3.1. D(x,y) = D(y,x) = D((0,0),y-x). D9(a,b),(a,c)) = |b-c|.
D satisfies B3 = Continuity.
Proof: The equations require only C1,C2, as in the proof of Lemma
2.1.1.1. Note that D((a,b),(c,d)) <= D((a,b),(a,d)) + D((a,d),(c,d)) =
|b-d| + |a-c|. Continuity of D is now immediate. QED
THEOREM 2.1.3.2. D:(R^2)^2 into [0,infinity) satisfies conditions
C1-C4 if and only if D is the usual Euclidean distance in R^2.
Proof: From Lemma 2.1.3.1, Theorem 2.1.2.3, and that Euclidean
distance evidently satisfies C1-C4. 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 738th 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
737: Philosophical Geometry/15 12/22/16 3:24PM
Harvey Friedman
More information about the FOM
mailing list