[FOM] 728: Philosophical Geometry/12

Mon Oct 24 15:35:24 EDT 2016

We continue in this TOC:

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)  HERE
9. DIRECTED CIRCLES, TRIANGLES (1 dimension)
10. COORDINATED PLANE
11. DIRECTED LINES IN THE PLANE

In http://www.cs.nyu.edu/pipermail/fom/2016-October/020109.html we
mentioned that we can characterize midpoint functions M by either of
the two criterion:

M1. M(M(x,y),M(z,w)) = M(M(x,z),M(y,w)).
M2. Suppose x < y < z < u < v < w, where y = M(x,z) and v = M(u,w).
Then M(x,w), M(y,v), M(z,u) are all equal or all distinct.

I can simplify M1 but I need to add another clause to M2. This is all
worked out in detail in

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

This 10/2216 version supersedes some earlier ones of a few dates
earlier. The new conditions on midpoint functions M are

P1. M(x,M(y,z)) = M(M(x,y),M(x,z)).
P2.  Suppose x < y < z < u < v < w, where y = M(x,z) and v = M(u,w).
Then M(x,w), M(y,v), M(z,u) are all equal or all distinct.
Suppose x < y < z < w, where M(x,z) = y and M(y,w) = z. Then M(x,w) = M(y,z).

Obviously P1 is mathematically simpler, but P2 can be more easily visualized.

8. DIRECTED LINE (1 dimension)

Here we use directed lines and a choice of other primitives for one
dimensional geometry. For completeness, we can use just directed lines
with the associated primitives. For categoricity, we use a betweenness
function. This will give us categoricity only with respect to the
directed line primitives. To recover full categoricity and full
completeness, we use P1,P2 above for midpoint functions, or
alternatively an equidistance relation.

I like the directed line approach much better than betweenness, and I
am planning section 12, directed lines in the plane. It is useful to
be explicit about the notation for the directed line approach.

Informally, a directed line L is a line with a direction. This means a
line with a reflexive linear ordering on its points. We write L(x,y)
for "x is at or before y in L". Thus x is on (in) L is equivalent to
L(x,x).

In this section, we are working only on one dimension, and so there
are exactly two directed lines L,L', where we have L(x,y) iff L'(y,x).
Things get much richer, of course, in section 12.

Betweenness is of course easily defined as y is between x and z if and
only if there is an L such that L(x,y) and L(y,z). We don't need any
cumbersome or unfamiliar axioms for betweenness to deal with, instead
relying on the extremely familiar reflexive linear ordering axioms of
reflexivity, antisymmetry, transitivity, and connectedness.
Completeness is readily stated by lub for L(x,y).

We now state the exact syntax of the basic language for one
dimensional directed lines.

There are two sorts, one for points, and one for directed lines.
Variables over points are x_n, n >= 0. Variables over directed lines
are L_n, n >= 0. We have equality between variables of the same sort.
We have the primitive ternary relation between lines, points, and
points, written L(x,y).

To this is in the usual many sorted framework with equality for both sorts.

The atomic formulas are x_n = x_m, L_n = L_m, L_n(x_m,x_r). Atomic
formulas and formulas are defined as usual.

1. L(_,_) defines a dense reflexive linear ordering with no endpoints
on the universe of points.
2. There are exactly two L's.
3. L not= L' implies (forall x,y)(L(x,y) iff L'(y,x)).

THEOREM 8.1. 1-3 is countably categorical and complete. 1-3 proves
first order lub.

Here first order lub is the scheme

4. Least upper bound principle on the ordering L(_,_) for first order
formulas in the above first order language L(_,_).

We don't get that any two models of 1,2 are isomorphic, because we
never get that for first order theories with infinite models because
of upward Skolem Lowenheim. So we use a second order axiom. Here we
don't want to use anything like full second order logic, but rather a
tiny fragment thereof. I.e., free variable second order logic. Here we
have second order variables - over sets of points - but no second
order quantifiers. Then we have the second order axiom

5. Any nonempty set of points with an upper bound in the ordering
L(_,_) has a least upper bound in the ordering L(_,_).

THEOREM 8.2. 1-3,5 is not categorical. I.e., there are models of 1-3,5
that are not categorical.

There are a number of directions to go to achieve categoricity with
expanded languages. There are two different relevant senses of
categoricity here. The weaker sense is categoricity with respect to
L(_,_). This means that any two models in the expanded language are
isomorphic with respect to the language L(_,_). The stronger sense
requires that any two models in the expanded language are isomorphic
in the full sense.

For the weaker notion of categoricity, we can of course use weaker
additional axioms. Axioms 6,7 involve the new primitive BE (between
function) which is a binary function from points to points. Axiom 8
involves the new primitive F which is a binary function from points to
points.

6. (L(x,y) and x not= y) implies L(x,BE(x,y),y).

7. Let L be given. BE is continuous at each x not= y with L(x,y), in
the sense that uses L(_,_).

THEOREM 8.3. 1-3,5,6,7 is categorical with respect to the language L(_,_).

Proof: By the theory of continuous between functions developed in [1],
section 4. QED

8. Let L be given. F is strictly increasing in each argument (first or
second argument), and is continuous at every pair of points. in the
sense that uses L(_,_).

THEOREM 8.4. 1-3,5,8 is categorical with respect to the language L(_,_).

Proof: By the development in section 5 of [1]. QED

We use stronger axioms to achieve full categoricity. We will use M for
midpoint function, which is a binary function from points to points.

9. M(x,x) = x, M(x,y) = M(y,x). For each point x, M(x,y) and M(y,x)
are strictly increasing bijections from points y to points.

10. M(x,M(y,z)) = M(M(x,y),M(x,z)).

11. Suppose x < y < z < u < v < w, where y = M(x,z) and v = M(u,w).
Then M(x,w), M(y,v), M(z,u) are all equal or all distinct.
Suppose x < y < z < w, where M(x,z) = y and M(y,w) = z. Then M(x,w) = M(y,z).

Axiom 9 is of course mathematically simpler, but 11 is easier to "see".

THEOREM 8.5. 1-3,5,9,10 is categorical. 1-3,5,9,11 is categorical.

Proof: This is more or less done in section 6 of [1]. In the current
version, it is done only if there are endpoints. But it is easily
adapted to the present case where there are no endpoints. QED

There is another approach to categoricity here which is in essence a
weak form of the well known fact that complete densely ordered Abelian
groups are isomorphic. This approach is based on equidistance. Given
any three points x,y,z, we can see the unique point w such that the
directed distance from x to y is the same as the directed distance
from z to w.

We will use a very special case of equidistance which is the reverse
of the between functions and midpoint functions above. This is what we
call an Extension function E(x,y). We clearly see that if x < y then
there is a unique point z such that the distance from x to y is the
same as the distance from y to z.

12. x < y implies x < y < E(x,y). For each x, E(x,y) is strictly
increasing from the points greater than x onto the points greater than
x.

THEOREM 8.6. 1-3,5,12 is categorical with respect to the language L(_,_).

Proof: Define B at the (x,y) with x < y as the unique x < z < y with
E(x,z) = y. Then B is a continuous between function in the sense of
axiom 7. QED

For full categoricity, we can proceed as we did with axioms 9, 10, 11.

Presumably there is a development akin to what we did for midpoint
functions M to achieve full categoricity. The law E(x,E(y,z)) =
E(E(x,y),E(x,z)) is of course valid for the intended E(x,y) = 2y-x on
the reals.

***********************************************
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 728th 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
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  10/17/16  4:04PM
727: Large Cardinals and Emulations/25  10/20/16  1:37PM

Harvey Friedman