[FOM] 725: Philosophical Geometry/10

[Harvey Friedman]

I just posted

[1] Complete Dense Linear Orderings, October 14, 2016, 22 pages, #90,
http://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/

It contains complete proofs, and works entirely in complete dense
linear orderings (D,<), covering continuous between functions and
midpoint functions. So readers of
http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html may want
to consult it.

We continue the development of Philosophical Geometry in one
dimension from http://www.cs.nyu.edu/pipermail/fom/2016-October/020112.html
where we proved the completeness and omega-categoricity of 1-4

1. ONE DIMENSIONAL GEOMETRY
2. CONTINUUOUS BETWEEN FUNCTIONS
3. MIDPOINT FUNCTIONS
4. EQUIDISTANCE
5. EXTENDED CATEGORICITY
6. EXTENDED FIRST ORDER COMPLETENESS
7. BETWEENESS

1-6. See http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html

7.  BETWEENESS
continued from http://www.cs.nyu.edu/pipermail/fom/2016-October/020112.htm

1. Everybody sees points. We use D for the set of points.
2. Everybody sees the 3-ary relation BE(x,y,z) for "y is strictly
between x and z".
3. Everybody sees endpoints. We use E for the unary predicate "being
an endpoint". Everybody sees that E holds of exactly two points. Of
course, we have no notion of left and right endpoints, as not
everybody will agree on that.
4. Everybody sees that if v,w comprise the endpoints of D, then the
relation R given by BE(v,x,y) or BE(x,y,w) or (x = v and y = w) is an
sdlowbe with left endpoint v and right endpoint w, where BE(x,y,z) if
and only if (R(x,y) and R(y,z)) or (R(z,y) and R(y,x)).    .
5. For every nonempty set S of points, there is a minimal interval
(between interval, given by endpoints, possibly open, closed, or half
open, possibly
with only zero or one element) which contains S.

and also characterize the betweenness relation on strict dense linear
orderings with both endpoints = sdlowbe.

We now adapt sections 2-6 to betweenness.

6. We see the between function B:D'^2 into D, with x not= y implies
BE(x,B(x,y),y). We see BE(x,y) as the midpoint
between x and y. We also see its pointwise continuity. I.e., that for
all x,y that are not endpoints, if BE(a,B(x,y),b) then there exists
BE(c,x,d) and B(e,y,f) such that BET maps (c,d) x (e,f) into (a,b).
These intervals are betweenness intervals.

THEOREM  7.5. If (D,BE,B) satisfies 1-6 then (E,BE) is isomorphic
to ([0,1],BE), where [0,1] is the usual unit interval in the real
numbers and BE is its usual betweenness relation.

Proof: Let R be the sdlowbe given by 4. Then BET is a continuous
between function on (D,R). By [1], (D,R) is separable. Hence (D,R) is
isomorphic to [0,1[. Therefore (D,BE) is isomorphic to [0,1] with the
usual betweenness relation. QED

We can similarly adapt sections 3-6 to betweenness.

***********************************************
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 725th 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

Harvey Friedman