[FOM] 723: Philosophical Geometry/8

[Harvey Friedman]

Recall that this is PHILOSOPHICAL GEOMETRY, where we investigate what
is in the mind's geometric eye. There is a considerable overlap with
well known mathematical developments. Note that I changed the title
from "foundations of geometry" to "philosophical geometry".

In http://www.cs.nyu.edu/pipermail/fom/2016-October/020103.html we
gave unexpectedly simple characterizations, second order
axiomatizations, and first order axiomatizations, of Euclidean plane
geometry using a sort for real numbers.

We now want to eliminate a sort for the real numbers, and proceed
purely geometrically.

In fact, I now want to try to systematically develop Philosophical
Geometry starting with the basics. This means that I am going to be
looking at ONE dimensional Philosophical Geometry before I even get to
two dimensions and higher.

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

1. ONE DIMENSIONAL GEOMETRY

I am looking at a pad of paper. Before taking up what I see on the
entire top page of the pad, I just want to take up what I see along
the bottom edge.

In this posting, I will focus on the most common modern way of looking
at the bottom edge, namely as a set of points with some structure.
There is a very interesting Aristotelean conception, where there are
no points as we understand them today, but rather only intervals. And
these intervals have no endpoints. I have made some substantial claims
about this conception in
http://www.cs.nyu.edu/pipermail/fom/2016-June/019893.html under
"Version for PA" and "Version for Z_2". I will take this up in a near
future posting, but not here. Here I will stick with points.

So I am looking at the bottom edge E with my mind's geometric eye.
What do I see? You can substitute "clearly imagine" if you want for
"see".

The usual plan in Philosophical Geometry is to list the basic
relationships that we see, and list the basic facts that we see are
true about them, and then investigate if these basic facts determine
the basic relationships up to isomorphism.

What is the special significance of having only one system up to isomorphism?

Aside from any mathematical significance, there is the following. It
means that what everybody sees is the same - at least the same
structurally. I.e., what you see at the bottom edge of your pad is the
"same" as what I see at the bottom edge - and also even if we are
together looking at the exact same bottom edge.

Now I certainly do not want to take this philosophical discussion of
just what we are doing when we do Philosophical Geometry too far.
First it is premature. We are better off getting a substantial
development of Philosophical Geometry off the ground, with hopefully
striking findings, first, and then using that success and experience
in order to fine tune and expand on the philosophy - thereby creating
offshoot foundational investigations, with crude philosophy, followed
by success and experience, following by fine tuned and expanding
philosophy, etcetera, in a long series of synergistic interactions
between philosophy, foundations, and mathematics..In this particular
case of Philosophical Geometry, the deep and subtle relationship
between the subjective and the objective will figure prominently.

1. We see points. For convenience, we refer to the set of points as E.
2. We see the left/right relationship. I will write this as <. We see
the usual strict linear ordering principles.
3. We see the leftmost point and the rightmost point. For convenience,
we refer to these two points as 0 and 1, respectively.
4. We see that if x < y then there exists z such that x < z < y.
5. We see that if we take any nonempty set of points, then there is a
leftmost point with the property that it is not to the left of any
points in the set.

Of course it is well known that 1-4 is not categorical. Furthermore,
it is also well known that even 1-5 is not categorical - which we can
conveniently think of as a second order theory. However, in order to
prove this non categoricity, some significant set theoretic
infrastructure is needed - even for 1-4. This is because it is
countably categorical, and so uncountable sets are needed. Actually, I
am not sure that people have discussed just what the best way to talk
about this situation is metamathematically, but I don't want to go
there - at least not here.

It is also well known that 1-4 forms a complete first order theory -
even without using 5 in any way. In particular, the first order form
of 5 is provable from 1-4. There are very interesting lengths of
proofs and lengths of kinds of proofs and structures of proofs issues
that have at least been partially addressed.

We would like to strengthen 1-5 so that the systems of points with
left/right is uniquely determined up to isomorphism. There are many
very appropriate ways of doing this, including some novel ones. It is
quite interesting to see just how minimalistic we can be, and we take
this to a fair extent - but there remains quite a lot to do along
these lines of minimalism.

It is pretty clear that any appropriate way of uniquely determining
(E,<) up to isomorphism is going to involve using new primitives.
Using just < will of course require second order conditions, but we
already have the second order condition 5. Clearly we are looking for
separability (countable dense set), and if we use a good chunk of
second order logical constructions, we can force separability without
adding to the primitives. However, such an approach would require some
serious second order quantifiers, rather than the extremely restrained
kind of free second order variables used in 5. So here we have a
foundational investigation - build up detailed results concerning what
it takes to get categoricity of (E,<) without using new primitives, in
terms of the complexity of second order logic constructions, toward an
argument that it cannot be done "satisfactorily".

Instead, we accept that we are going to use a new primitive, and of
course we want it to be something that we can clearly "see".

We discuss three approaches here. Between functions, midpoint
functions, and equidistance. The idea is to write down what we see
clearly and add it to 1-4, thereby determining (E,<) to be ([0,1],<)
up to isomorphism. Mathematically, the tool is to somehow derive
separability. This will involve defining a countable set and invoking
5 to get a maximal open interval disjoint from the countable set, and
showing that this maximal open interval is empty.

However, in adding a new primitive, we obviously would like
categoricity of the extended system. This requires yet more axioms
that we must clearly "see", hopefully without adding any further
primitives. Indeed, there are things that we can clearly "see" under
all three approaches that do close the process and obtain categoricity
for the extended language.

There still remains the issue of first order completeness. With 1-4,
we have first order completeness even without 5. What happens when we
add these primitives? This is addressed in the last section.

2. CONTINUOUS BETWEEN FUNCTIONS

In this approach to determining (E,<) up to isomorphism, we leverage
off of the usual notion of pointwise continuity. In this context, this
has a natural formulation which can be "seen". However, in the
approach in the next section, with midpoint functions, continuity is
not needed. The continuity that is needed is derived from arguably
more vivid scenery. So we replace 4 with

4'. We see the between function B from {(x,y): 0 < x < y < 1} into B,
with x < y implies x < B(x,y) < y. We see B(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 a < B(x,y) < b then there exists
c < x < d and e < y < f such that B maps (c,d) x (e,f) into (a,b).

NOTE: We could have B defined on all x < y or even all x,y (with an
obvious change), but we don't need it. For balance, the midpoint
functions of section 3 are defined on all x,y.

THEOREM  2.1. If (E,<,B) satisfies 1,2,3,4',5 then (E,<) is isomorphic
to ([0,1],<), where [0,1] is the usual unit interval in the real
numbers.

This was proved in
http://www.cs.nyu.edu/pipermail/fom/2005-February/008773.html This is
also proved in the much more detailed and comprehensive

H. Friedman, Complete Dense Linear Orderings,
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/

It hasn't been completed but it will be soon, and placed there right away.

3. MIDPOINT FUNCTIONS

Now we use

4*. We see the binary midpoint function M from E^2 into E. We see that
for all x,y
i. M(x,x) = x, M(x,y) = M(y,x).
ii. x < M(x,y) < y.
iii. M(x,y) as a function of y is strictly increasing from E onto
[M(0,x),M(x,1)].

THEOREM 3.1. If M is a midpoint function then its restriction to
{(x,y): 0 < x < y < 1} is a between function.

THEOREM 3.2. If (E,<,B) satisfies 1,2,3,4*,5 then (E,<) is isomorphic
to ([0,1],<), where [0,1] is the usual unit interval in the real
numbers.

4. EQUIDISTANCE

Equidistance is a 4-ary relation that we clearly see.

4#. We see the 4-ary equidistance relation EQ. Specifically,
EQ(a,b,c,d) means that a < b and c < d and the distance from a to b is
the same as the distance from c to d. We see the logical facts typical
in a situation like this. Namely, EQ(a,b,a,b), EQ(a,b,c,d) iff
EQ(c,d,a,b), EQ(a,b,c,d) and EQ(c,d,e,f) implies EQ(a,b,e,f). We see
that EQ(a,b,c,d) implies (a < c iff b < d). Let a < b and c < d. We
see that there exists x such that
i. c < x <= d and EQ(a,b,d,x); or
ii. a < x <= b and EQ(a,x,c,d).

THEOREM 4.1. If (E,<,EQ) satisfies 1,2,3,4#,5 then (E,<) is isomorphic
to ([0,1],<), where [0,1] is the usual unit interval in the real
numbers.

5. EXTENDED CATEGORICITY

So in sections 2-4, we have expanded (E,<) with three different kinds
of new primitives. The question arises if we have categoricity in the
extended languages.

THEOREM 5.1. In the case of 1-3,4',5 with B and in the case of
1-3,4*,5 with M, we do not have categoricity. However, in the case of
1-3,4#,5 we do have categoricity. In the latter case, any (E,<,EQ)
satisfying 1-3,4#,5 is isomorphic to ([0,1],<,R) where R(a,b,c,d) iff
a < b and c < d and a-b = c-d.

But we can put some rather satisfactory conditions on M so that we do
get the extended categoricity that we get for EQ. One is
mathematically preferable but not readily "seen", whereas the other is
readily "seen". Here are two for midpoint functions:

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.

These are obviously satisfied by the usual (x+y)/2.

THEOREM 5.1. There is a midpoint function M on usual [0,1] for which
M1 fails. M can be taken to be continuous piecewise linear.

THEOREM 5.2. Let (E,<,M) satisfy 1-3,4*,5 with M1 or M2. Then (E,<,M)
is isomorphic to ([0,1],<,(x+y)/2).

6. EXTENDED FIRST ORDER CATEGORICITY

We can also show that 1-3,4#, and first order 5 (for the extended
language) is first order complete (for the extended language).

We can show that 1-3,4* with M1 or M2, and first order 5 (for the
extended language) is first order complete (for the extended
language).

The idea is to establish an appropriate equivalence with the theory of
ordered abelian groups with first order 5. This is well known to be
first order complete, and is equivalent to the theory of divisible
ordered abelian groups. .

***********************************************
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 723rd 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

Harvey Friedman