[FOM] 726: Philosophical Geometry/11

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

So where have we been and where are we going?

This Philosophical Geometry series started off here with assuming a
sort for real numbers with only additive and order properties, looking
at the plane as pairs of real numbers, and then completely determining
what the distance between arbitrary points must be on the basis of
what you see in your mind's eye. After some somewhat false starts,
this converged to the posting
http://www.cs.nyu.edu/pipermail/fom/2016-October/020103.html

REGARDING THE EARLIER POSTINGS FOUNDATIONS OF GEOMETRY 1-5

But earlier than
http://www.cs.nyu.edu/pipermail/fom/2016-October/020103.html I had
some versions that relied on the following:

THEOREM A. The f:R^2 into R^2 that are line preserving are exactly the
one-one affine f:R^2 into R^2.

I will give a readily self contained proof of this here, as I didn't
see a readily accessible internet proof. Here line preserving means
the forward image of every line is a line. This definitely is known.

I also stated this:

THEOREM B(?). The f:R^2 into R^2 that preserve collinearity (iff) are
exactly the one-one affine f:R^2 into T^2.

There was some confusion over B. I think I omitted one-one, which led
some to think that I meant preserve collinearity in the weak sense
that if x,y,z lie on a line then fx,fy,fz lie on a line. Then B is
false even without "one-one". Dana Scott sent me f(x,y) = (x^3,0).
However, I mean x,y,z lie on a line if and only if fx,fy,fz lie on a
line. Then (0,0),(0,1),(2,2) do not lie on a line but
(0,0),(0,0),(8,0) do lie on a line.

We first prove Theorem A. Until the end of the proof of Theorem 9, let
f:R^2 into R^2 be line preserving.

LEMMA A1. f is one-one.

Proof: Let x not= y, fx = fy. Let z be off xy. The lines f[zx], f[zy]
must have common point fz, and also common point fx,fy. Hence fz = fx
= fy. This shows that f is constant off of xy. But then f is constant
on a line disjoint from xy, and so maps a line onto a point. QED

LEMMA A2. f is collinearity preserving (iff).

Proof: Let x,y,z lie on L. Then fx,fy,fz lie on f[L]. Let fx,fy,fz lie
on L. If x,y,z are not distinct then x,y,z lie on a line. Assume x,y,z
distinct. Since f maps xy onto fxfy, the value fz is attained on xy.
Since z is not in xy, this violates that f is one-one. QED

LEMMA A3. L,L' intersect if and only if f[L],f[L'] intersect.

Proof: If L,L' intersect then let x in L,L'. Clearly fx in f[L],f[L'].
Now let xy and zw be disjoint. For visual clarity, we can assume that
xy and zw have the same orientation. Then x,y,z,w are distinct, and so
fx,fy,fz,fw are distinct. Also fxfy and fzfw are either parallel or
have exactly one point of intersection. Assume the latter. The line yw
is mapped onto the line fyfw, and so let fu be on the line fyfw where
fzfu is parallel to fxfy. Then zu and xy meet, and therefore fzfu and
fxfy meet. QED

LEMMA A4. f is a bijection.

Proof: Let u not be a value of f. Let L,L' be two disjoint lines. Then
f[L],f[L'} are disjoint lines omitting u. Let fx,fy in f[L], fz,fw in
f[L'], fx,fy,fz,fw distinct, fxfw and fyfz meet at exactly u. Then
x,y,z,w are distinct, xy and zw are disjoint. Also xw and yz cannot be
disjoint since fxfw and fyfz are not disjoint. And xw and yz cannot be
the same line. Hence xw and yz meet at exactly one point v. Therefore
fsfw and fyfz both include fv. Therefore u = fv. QED

LEMMA A5. f preserves betweenness (iff). Also f preserves midpoints.

Proof: f is an automorphism of the structure (R,lines,membership). It
is known that betweenness and midpoints can be defined without
parameters in this structure. QED

LEMMA A6. Assume f(0,0) = (0,0). f(rx) = rf(x).

Proof: We can assume that x = (a,b) not= (0,0). Then f maps the line
{r(a,b): r in R} onto the line {rf(a,b): r in R}. Let f(a,b) = (c,d)
not= (0,0). Using that f preserves midpoints, we get that each
f(+-2^n(a,b)) = 2^n(f(a,b). Then using more preservation of midpoints,
we get f(p(a,b)) = p(f(a,b)) for dyadic rationals p. Since f preserves
betweenness, this gives f(r(a,b)) = rf(a,b). QED

A parallelogram is taken here to mean a quadruple of distinct points
x,y,z,w such that x,y,z are not collinear, xy, zw are disjoint, and
xz, yw are disjoint. Note that if x is (0,0), then w = y+z.

LEMMA A7. f maps parallelograms onto parallelograms.

LEMMA A8. Assume f(0,0) = (0,0). For all x,y,z, x+y = z if and only if
fx + fy = fz.

Proof: Suppose (0,0),x,y,x+y is a parallelogram. It is sent to the
parallelogram (0,0),f(x),f(y),f(x+y). We must have f(x+y) = f(x)+f(y).

Now suppose (0,0),x,y,x+y is not a parallelogram. We still claim
f(x+y) = f(x)+f(y). This is clear if x or y is (0,0). It is also clear
if x = y by Lemma 6. Finally suppose (0,0),x,y are distinct and
collinear. Write y = rx. Again apply Lemma A6. QED

THEOREM A. f is one-one affine.

Proof: f - f(0,0) is line preserving and by Lemmas A6,A8, f - f(0,0)
is linear. Hence f is affine and one-one by Lemma A1. QED

This completes the proof of Theorem A. I have run into some problems
proving Theorem B. If we add the additional hypothesis that f:R^2 into
R^2 is onto, then this reduces to line preservation:

THEOREM B'. If f:R^2 into R^2 is collinear preserving (iff) and
surjective, then it is line preserving.

Proof: Clearly f[L] is a collinear set with at least two elements x
not= y (uncountably many), and so part of a unique line L'. Suppose
f[L] is not all of L', and let fz in L'\f[L]. Then x,y,fz are
collinear but x,y,z are not. QED

Apparently from http://www.pnas.org/content/77/7/3756.full.pdf it is
more common to investigate collinear preserving in only the forward
direction. And there it is stated that already for collinear
preserving (if then), and a weak form of surjectivity, we get that f
is one-one affine. The weak form of subjectivity is that the range
contain a quadrangle.

So perhaps the status of Theorem B without the surjectivity, or some
weak form of surjectivity, is unclear. Possibly also relevant is

a. Martin, G. E., Transformation Geometry (An Introduction to
Symmetry), Springer-Verlag, New York, 1982.

b. http://www.kurims.kyoto-u.ac.jp/EMIS/journals/AMI/2005/krisztin.pdf

2. RESUMING DEVELOPMENT OF PHILOSOPHICAL GEOMETRY

I then articulated a general ongoing program called Philosophical
Geometry, where we systematically go through major geometric objects
and write down what we "see", and also what everybody "sees" - all
observers - which in many cases is somewhat different, forming
characterizations and second order and first order axiomatizations
that are hopefully complete and/or (countably) categorical.

We are not really finished with one dimensional geometry. However, we
started to anticipate the two dimensional situation, and we think that
using directed lines is particularly good. I.e.,at this point, we
think that notationally and arguably conceptually, the best primitive
for a lot of philosophical geometry, particularly if it is to be
OBSERVER INDEPENDENT, is the directed line. This incorporates lines,
collinearity, and betweenness, all in one convenient compact notation.
The basic notion is L(x,y), which means that the directed line goes
from point x to point y, where L(x,x) is allowed and simply means that
x is on L. For each L, L(x,y) is a reflexive linear ordering on {x:
L(x,x)}.

We need to restate the betweenness stuff with directed lines in one
dimension. We do this in a new section 8 based on directed lines.

But this posting is already long enough and we will start with the
next in the series.

To keep track of where we are in this Philosophical Geometry, we keep
a running Table of Contents with indications of where the topics have
been treated.

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/020112.html
and Philosophical Geometry/9
8. DIRECTED LINES
9. DIRECTED CIRCLES
9. DIRECTED TRIANGLES
10. DIRECTED LINES IN THE PLANE

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

Harvey Friedman