[FOM] 736: Philosophical Geometry/14
Harvey Friedman
hmflogic at gmail.com
Tue Dec 20 12:43:50 EST 2016
We now continue from Philosophical Geometry/13,
http://www.cs.nyu.edu/pipermail/fom/2016-December/020190.html where we
reworked section 0.
The new section 0 from
http://www.cs.nyu.edu/pipermail/fom/2016-December/020190.html was
particularly successful and has created a new standard for
Philosophical Geometry in two dimensions. So what we have had in mind
with Coordinated Plane will be postponed as we move directly to
DIRECTED LINES IN THE PLANE.
However, in this posting we revisit EQUIDISTANCE in one dimension
before we tacked Directed Lines in the Plane later.
We have reorganized the outline, renumbering sections - BUT we still
maintain those LINKS so as to avoid reader confusion. At some point we
will revisit and reorganize all of the 1 dimensional material. But up
to now, we have only One Dimensional Philosophical Geometry and the
reworking of section 0 in
http://www.cs.nyu.edu/pipermail/fom/2016-December/020190.html which is
now relabeled as section 2.1.
In this posting we take up section 1.10 in the New Outline:
NEW 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)
here
2. TWO DIMENSIONAL PHILOSOPHICAL GEOMETRY
2.1. DISTANCE DERIVATION IN THE PLANE
http://www.cs.nyu.edu/pipermail/fom/2016-October/020103.html
2.2. DIRECTED LINES IN THE PLANE
1.10. EQUIDISTANCE REVISITED (1 dimension)
Here we treat the continuum as a primitive which is taken to be the
one in a mind's eye. This is the private continuum, one that is not
available for other minds to see. Therefore it comes with a
left/right. In a public continuum, there is no preferred left/right
since another mind can view the same continuum from the other side and
have the opposite left/right.
This private/public distinction is not normally discussed as such in
mathematics. For instance, in the present situation, this is reflected
in simply what form the structures take. For the private continuum,
here we use (D,<,EQ), where < is the left/right linear ordering and EQ
is the 4-ary equidistance relation. For the public continuum, we use
either (D,{<_1,<_2},EQ) or (D,B,EQ), where in the first case we use a
set of cardinality 2 whose elements are binary relations, opposite to
each other, and in the second case, B is the 3-ary betweenness
relation. Obviously, the second option is much simpler logically, but
the axioms for betweenness are not nearly so easily memorable as the
axioms for strict linear ordering. In the former case, we are using an
extension of the usual elementary model theory to incorporate sets of
relations rather than just relations. There are corresponding axioms
and rules which are complete (incorporating sets of relations), and I
don't recall having seen this worked out. In this posting we will only
be working with the private continuum, (D,<,EQ).
Mathematics has been operating just fine for centuries without paying
direct attention to the private/public distinction. The usual
foundations of mathematics is based on set theory, whose objects are
rigid and immutable, and does not reflect any private/public dichotomy
(in standard treatments). Currently, any private/public distinction
such as the one we are drawing here between using < or using B or
using {<,>}. is handled as a development under the rigid and immutable
umbrella, as we do here. However, the private/public distinction seems
to have a different character in physical science. There it seems to
us that for genuine foundations of physical science, we need to
incorporate the private/public distinction at the outset - where the
private side corresponds to the observer and the public side
corresponds to external reality subject to multiple observers. This
may be a key reason - probably not the only key reason - why
foundations of physical science is in an incomparably more primitive
state than is foundations of mathematics.
In the earlier section 1.4 (and some related material in later
sections), we used equidistance to enforce that the left/right is
separable and order complete, thus establishing a second order
categoricity for the < part only. Here we want second order
categoricity for < and EQ (4-ary equidistance). We previously did this
with midpoints instead of equidistance.
We start with three axiom groups. These are not categorical or first
order complete, but form a fundamental set of axioms which correspond
to abelian ordered groups. We then exploit that correspondence to
obtain the later categoricity and first order complete results.
C1. (D,<) is a strict linear ordering with at least two elements.
C2. Equal distance. EQ(x,x,y,y). If x < y then there are exactly two
w's such that EQ(x,y,z,w). One of them is < z and the other is > z.
C3. Rearrangement.
i. If EQ(x,y,z,w) and EQ(x,y,u,v) then EQ(z,w,u,v) and EQ(w,z,x,y).
ii. Let x < y < z < w. If EQ(x,y,z,w) then EQ(x,z,y,w). Not EQ(x,w,y,z).
Note how readily these axioms are seen to be true in the mind's eye.
We have put serious effort into simplifying these as much as we have
been able to. Perhaps there are (no) further simplifications?
LEMMA 1.10.1. There are no endpoints.
Proof: By C2 since z is arbitrary, and there is some x not= y by C1. QED
LEMMA 1.10.2. EQ(x,y,x,y). In EQ(x,y,z,w), we can perform any of these
operations and preserve the truth value. interchange x and y,
interchange z and w, interchange x,y and z,w. In C2, we can replace x
< y by x not= y.
Proof: By C3i, we have EQ(x,y,z,w) implies EQ(w,z,x,y) implies
EQ(y,x,w,z) implies EQ(z,w,y,x) implies EQ(x,y,z,w), and hence these
are all equivalent.
Let x < y. By C2, there exists z,w such that EQ(x,y,z,w), EQ(w,z,x,y).
By C3i, EQ(x,y,x,y), EQ(y,x,y,x). This establishes the first claim.
Assume EQ(x,y,z,w). Since EQ(x,y,x,y), we have EQ(z,w,x,y) by C3i. We
also have EQ(z,w,y,x), EQ(y,x,z,w),. Wee also have EQ(w,z,x,y),
EQ(x,y,w,z).
For the final claim, let x > y. Then y < x and so there are exactly
two w's such that EQ(y,x,z,w), and one of them is < z and the other is
> z. But EQ(y,x,z,w) is equivalent to EQ(x,y,z,w). QED
LEMMA 1.10.3. Let x < y < z < w. EQ(x,y,z,w) iff EQ(x,z,y,w).
Proof: Let x < y < z < w and EQ(x,z,y,w). By C2, EQ(x,y,z,w'), w' > z.
By C3ii, EQ(x,z,y,w'), y < w'. By C2, w = w'. QED
LEMMA 1.10.4. EQ(x,y,z,z) iff x = y.
Proof: Suppose EQ(x,y,z,z). By Lemma 1.10.2, if x not= y then
EQ(x,y,z,z) implies z < z or z > z, which is impossible. Hence x = y.
The converse is by C2. QED.
LEMMA 1.10.5. Suppose EQ(x,y,z,w) and x < y iff z < w. Then
EQ(x,z,y,w) and x < z iff y < w.
Proof: Assume hypotheses. We argue by cases.
1. x < y. Then z < w.
1.1. x < z.
1.1.1. y < z. Thus x < y < z < w and apply C3ii.
1.1.2. y = z. Then EQ(x,z,y,w).
1.1.3. x < z < y. Now w < y is impossible by C3ii. Also w = y
contradicts Lemma 10.2. Hence x < z < y < w. EQ(x,z,y,w) by Lemma
10.3.
1.2. z < x. Now EQ(z,w,x,y), and so we are in case 1.1.
1.3. x = z. Then EQ(x,y,x,w), EQ(x,y,x,y). Since x < y and x < w, by
C2, w = y. Hence EQ(x,z,y,w).
2. x > y. Now EQ(y,x,w,z), and so we are in case 1.
3. x = y. Then EQ(x,x,z,w), z = w, EQ(x,z,x,z).
QED
DEFINITION 1.10.1. Fix arbitrary 0 in D. For x not= 0, x+y is the
unique z such that EQ(0,x,y,z) and 0 < x iff y < z (using Lemma 10.2).
For x = 0, x+y = y.
LEMMA 1.10.6. x+0 = 0+x = x. x+y = y+x.
Proof: The first claim is immediate for x = 0. Assume x not= 0. Then
0+x is the unique y such that EQ(0,x,0,y) and x < 0 iff y < 0. We have
EQ(0,x,0,x) and x < 0 iff x < 0. Hence 0+x = x.
Let 0 < x,y. Then EQ(0,x,y,x+y), EQ(0,y,x,y+x), y < x+y, x < y+x. By
Lemma 1.10.5, x < x+y and y < y+x. By Lemma 1.10.5, EQ(0,y,x,x+y). By
Lemma 1.10.2, y+x = x+y.
Let x,y < 0. Then EQ(0,x,y,x+y), EQ(0,y,x,y+x), y > x+y, x > y+x. By
Lemma 1.10.5, x > x+y and y > y+x. By Lemma 1.10.5, EQ(0,y,x,x+y). By
Lemma 1.10.2 , y+x = x+y.
Let y < 0 < x. Then EQ(0,x,y,x+y), EQ(0,y,x,y+x), y < x+y, x > y+x. By
Lemma 1.10.5, x > x+y, and EQ(y,0,y+x,x), y < y+x. By Lemma 10.5,
EQ(0,x,y,y+x). By Lemma 1.10.2, y+x = x+y.
We have verified x+y = y+x in all cases except (x = 0 or y = 0) and
the case x < 0 < y. The former case is by the first claim. In the
latter case, by the above, we have y+x = x+y. QED
LEMMA 1.10.4. x < y iff x+z < y+z. x = y iff x+z = y+z. x,y > 0
implies x+y > x,y. x,y < 0 implies x+y < x,y.
Proof: The first claim is obvious if z = 0. Suppose z not= 0. By
defintion, EQ(0,x,z,x+z), EQ(0,y,z,y+z), EQ(0,z,x,x+z), EQ(0,z,y,y+z),
EQ(x,x+z,y,y+z), and x < x+z iff y < y+z iff 0 < z. By Lemma 10.5, x <
y iff x+z < y+z.
By the first claim, x < y iff x+z < y+z. So if x+z = y+z then x < y
and y < x must both be false. Hence x+z = y+z implies x = y.
Let x,y > 0. By the first claim, 0 < x implies y < x+y and 0 < y
implies x < x+y. Hence x,y < x+y.
Let x,y < 0. By the first claim, x < 0 implies x+y < y and y < 0
implies x+y < x. Hence x+y < x,y. QED
LEMMA 1.10.5. For all x there exists a unique y such that x+y = 0.
Proof: This is obvious for x = 0. Let x not= 0. By Lemma 1.10.2,
EQ(x,0,0,y), x < 0 iff 0 < y. By definition, EQ(0,x,y,x+y), 0 < x iff
y < x+y. Clearly EQ(0,x,y,0), 0 < x iff y < 0. By Lemma 1.10.2, 0 =
x+y. Uniqueness of y follows from Lemma 1.10.4. QED
DEFINITION 1.10.2. -x is the unique y such that x+y = 0.
LEMMA 1.10.6. (x+y)+z = x+(y+z).
Proof: If any of x,y,z are 0 then this equation holds by inspection.
Assume x,y,z not= 0. We have
1. EQ(0,x,y,x+y), 0 < x iff y < x+y.
2. EQ(0,y,z,y+z), 0 < y iff z < y+z.
3. EQ(0,z,x+y,(x+y)+z). 0 < z iff x+y < (x+y)+z.
4. EQ(0,x,y+z,x+(y+z)). 0 < x iff y+z < x+(y+z).
all by definition. We have
5. EQ(y,x+y,y+z,x+(y+z)), y < x+y iff y+z < x+(y+z), by 1,4.
6. EQ(0,z,y,y+z), 0 < z iff y < y+z, by 2 and Lemma 1.10.5.
7. EQ(y,y+z,x+y,x+(y+z)), y < y+z iff x+y < x+(y+z), by 5 and Lemma 1.10.5.
8. EQ(y,y+z,x+y,(x+y)+z), y < y+z iff x+y < (x+y)+z, by 3,6.
9. x+(y+z) = (x+y)+z by 7,8 and Lemma 1.10.2.
THEOREM 1.10.7. Let (D,<) satisfy C1-C3, 0 in D be arbitrary, and +,-
be as defined above. Then (D,<,0,+,-) is an abelian ordered group with
no greatest and no least element. In particular, C1-C4 is mutually
interpretable with the theory of ordered abelian groups with at least
two elements.
Proof: Here is one well known version of the usual axioms for an
ordered group (D,<,+,-). Note that all of these have been verified
above.
(x+y)+z = x+(y+z).
x+0 = 0+x = x.
x+-x = -x+x = 0.
< is a strict linear ordering on D.
x < y implies x+z < y+z and z+x < z+y.
We have also verified x+y = y+x. So this interprets ordered abelian
groups with at least two elements in C1-C4. To interpret C1-C4 in
ordered abelian groups with at least two elements, define EQ(x,y,z,w)
according to C2 and proceed as expected. QED
LEMMA 1.10.8. EQ(x,y,0,y+-x). EQ(0,x,0,y) if and only if x = y or x = -y.
Proof: If x = y then EQ(x,y,0,y+-x). Suppose x not= y.
EQ(0,y,-x,y+-x)., EQ(0,-x,y,y+-x), EQ(x,0,0,-x), EQ(x,0,y,y+-x),
EQ(x,y,0,y+-x).
If x = y then EQ(0,x,0,y). Now x+-x = 0, and so EQ(0,x,-x,0). Hence
EQ(0,x,0,-x),
Suppose EQ(0,x,0,y). First assume 0 < x. Since EQ(0,x,0,x), if y > 0
then y = x. If y < 0 then since EQ(0,x,0,-x), -x < 0, we have y = -x.
Hence x = y or x = -y. Secondly assume x < 0. Since EQ(0,x,0,x), if y
< 0 then y = x. If y > 0 then since,EQ(0,x,-x) and -x > 0, we have y =
-x. Hence x = y or x = -y.
LEMMA 1.10.9. EQ(x,y,z,w) if and only if x+-y = z+-w or x+-y = w+-z.
Proof: Asume EQ(x,y,z,w). By Lemma 10.8, EQ(x,y,0,y+-x),
EQ(z,w,0,z+-w), EQ(0,y+-x,0,z+-w). By Lemma 10.8, y+-x = z+-w or y+-x
= w+-z (ordered group manipulation here).
Assume x+y = z+-w. Then EQ(0,x+-y,0,z+-w), EQ(x,y,0,x+-y),
EQ(z,w,0,z+-w), EQ(x,y,0,z+-w), EQ(x,y,z,w).
Assume x+y = w+-z. Then EQ(0,x+-y,0,w+-z), EQ(x,y,0,x+-y),
EQ(w,z,0,w+--z), EQ(x,y,0,w+-z), EQ(x,y,w,z), EQ(x,y,z,w). QED
We now add density and order completeness:
C1. (D,<) is a strict linear ordering with at least two elements.
C2. Equal distance. EQ(x,x,y,y). If x < y then there are exactly two
w's such that EQ(x,y,z,w). One of them is < z and the other is > z.
C3. Rearrangement.
i. If EQ(x,y,z,w) and EQ(x,y,u,v) then EQ(z,w,u,v) and EQ(w,z,x,y).
ii. Let x < y < z < w. If EQ(x,y,z,w) then EQ(x,z,y,w). Not EQ(x,w,y,z).
DECO. (D,<) is dense and order complete. I.e., between any two
elements there is a third, and every upper bounded nonempty subset of
D has a least upper bound.
Here the DE refers to "dense" and the CO refers to "complete".
THEOREM 1.10.10. Let (D,<,EQ) satisfy C1-C3,DECO. Then (D,<,EQ) is
isomorphic to the standard (R,<,EQ), where R is the usual real numbers
with the usual <, and EQ is the usual equidistance relation.
Proof: Let (D,<,EQ) satisfy C1-C3,DECO. Let 0 in D be arbitrarily. By
Theorem 1.10.7, (D,<,0,+,-) is an ordered abelian group whose ordering
is dense and complete. By a well known theorem going back to Holder,
1901, (D,<,0,+,-) is isomorphic to the usual ordered group of real
numbers. Let h:D into R be an isomorphism. We have only to check that
h preserves equidistance.
I.e., we need to verify that EQ(x,y,z,w) holds in (D,<,EQ) if an only
if EQ(hx,hy,hz,hw) holds in (R,<,EQ). By Lemma 1.10.9, EQ(x,y,z,w)
holds in (D,<,EQ) if and only if x+-y = z+-w or x+-y = w+-z holds in
(D,<,0,+,-). Also EQ(hx,hy,hz,hw) holds in (R,<,EQ) if and only if
hx+-hy = hz+-hw or hx+hy = hw+-hz. Because h is an isomorphism from
(D,<,0,+,-) onto (R,<,0,+,-), all four assertions are equivalent, and
hence h is an isomorphism from (D,<,EQ) onto (R,<,EQ). QED
C1-C3 is not first order complete. I.e., every sentence in the
language <,EQ is provable or refutable from the first order axioms
C1-C3. There are two main ways to complete it.
DECO(<,EQ).. < is dense, and every nonempty upper bounded subset of G
first order definable in <,EQ has a least upper bound.
DIV. For each integer n >= 2 and points x < y, there exists x = y_1 <
... < y_n = y such that for all 1 <= i <= n-2,
EQ(y_i,y_i+1,y_i+1,y_i+2).
DIV = "divisible".
THEOREM 1.10.11. C1-C3,DECO(<,EQ), C1-C3,DIV are logically equivalent
and complete first order theories.
Proof: We first show C1-C3,DECO(<,EQ) proves DIV. Let (D,<,EQ) satisfy
C1-C3,DECO(<,EQ), and let (D,<,0,+,-) be the abelian ordered group
defined previously. We first show that for every x > 0 and integers n
>= 1, there exists y such that y+...+y = x, where there are n y's. Let
S = {z: z+...+z < x}. A standard abelian densely ordered group
argument shows that for the least upper bound y of S, y+...+y = x. Now
S is defined in <,+,- but not in <,EQ. However, we defined +,- in
<,EQ.
Now let x < y. Set y so that z+...+z = y+-x, The definition of EQ in
terms of the ordered group given in the previous posting shows that x
< x+z < x+2z < ... < x+nz = y is as required. Thus we have proved DIV
from C1-C3,DECO(<,EQ).
Now suppose we have C1-C3,DIV. From the correspondence between EQ and
the ordered abelian group, we see from C6 that the ordered abelian
group is divisible. It follows from well known quantifier elimination
that this ordered abelian group has first order completeness in <,+,-.
We therefore have first order completeness in <,EQ, and hence we have
DECO(<,EQ).
Finally, we claim that C1-C3,DECO(<,EQ) and the logically equivalent
C1-C3,DIV are complete. Let phi be a sentence in <,EQ. Convert phi to
an equivalent sentence in ordered groups. Then phi* is provable or
refutable in divisible ordered abelian groups. But this translates
back to a proof or refutation of the original phi. 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 736th 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
Harvey Friedman
More information about the FOM
mailing list