[FOM] 717: Foundations of Geometry/5

[Harvey Friedman]

BY THE WAY: WHAT IS THIS WE ARE TRYING TO DO? It is what I call
Philosophical Geometry, focused on an analysis of intuitive geometric
notions. It is not aimed at developing geometry for various
mathematical purposes. And it is not at least directly concerned with
the structure of actual spacetime.

You will see below that there has been major simplifications. Most
notably, reflection about a line is no longer a primitive.

############################

I would like to explain two familiar formal notions in more detail.

DEFINITION. f:R^2 into R^2 is affine if and only if it is of the form
f(x) = g(x)+c, where g is linear and c is a constant from R^2.

DEFINITION. f:R^2 into R^2 is line preserving if and only if it maps
lines onto lines. f:R^2 into R^2 is collinearity preserving if and
only if for all points x,y,z lying on a line, fx,fy,fz lie on a line.

THEOREM. f:R^2 into R^2 is line preserving if and only if it is
one-one affine. f:R^2 into R^2 is collinearity preserving if and only
if f is affine. Bot is also true in any dimension >= 2.

I looked a bit on the internet for a nice short easy direct proof of
this, and didn't see one. I came up with one. Any favorite references?

REVIEW OF PHILOSOPHY. Under this approach, we start by taking for
granted the real number system. From this point of view, we regard
points as ordered pairs of reals, and put down conditions that are
clear in the mind's geometric eye that determine what the lines are
and what the distance functions (with values in the nonnegative
reals). In giving this characterization, we use just one auxiliary
conceps, also uniquely characterized. This is 90 degree
counterclockwise rotation. This aspect of what we are proposing does
not need any considerations of first or second order logic. It is a
straight unique characterization. Furthermore, we can look at the
fragments. I.e., whether the conditions involving only lines uniquely
characterize the lines, and so forth.

In the next posing we will take up second order axiomatizations. Here
we do not take the real number system for granted. There are two
developments here. One is to take a form of the real number system as
primitive, together with the usual complete axiom. The second is to
avoid any concept of real numbers, using only points and lines. This
of course raises the issue of how best and simplest to state the
necessary second order completeness.

Finally, we take up first order axiomatizations. There is a standard
way of passing from the kind of second order axiomatizations we are
considering to a corresponding first order axiomatization via schemes.
We show that this results in complete systems. I.e., where every
sentence in the language is provable or refutable in the system. This
is developed both with a sort for real numbers and without a sort for
real numbers.

CHARACTERIZATION

We take the reals as given. We simultaneously characterize the
following intuitive notions:

1. The lines as subsets of R^2. These are intended to be the intuitive
lines in R^2.
2. Binary function CCW(x,y). This is intended to be the intuitive
rotation of the point x 90 degrees counterclockwise about the point y.
2. Binary function D(x,y). This is intended to be the intuitive
distance between two points x,y, as a real number.

Here are the conditions:

A1. Two lines are equal if and only if they have the same points. For
any two distinct points, there is a unique line containing both. Every
line is nonempty and disjoint from some line.
A2. If x,y is in L then (x+y)/2 is in L. If (a,b) is not in L then
there exists c < a < d and e < b < f such that no (g,h) in L has c < g
< d and e < h < f. Informally, every line contains the midpoint
between any two of its points, and if a point does not lie on a line,
then its coordinates can be surrounded so that no point on the line
has its coordinates within those surroundings.
A3. CCW(y,y) = y. CCW(y+(1,0),y) = y+(0,1), CCW(y+(0,1),y) = y+(-1,0).
CCW(x,y), as a function of x, is line preserving.
A4. Let distinct points x,y,z,w,c be given, where CCW(x,c) = y,
CCW(y,c) = z, CCW(z,c) = w, CCW(w,c) = x. If x,z,u lie on a line then
D(u,y) = D(u,w).
A5. D(x,x+(0,a)) = |a|.

Since we are using the actual reals in this characterization, we are
free to use the simple numerical operations in A2,A3,A5.

THEOREM 1. The set of lines and functions CCW, D obeying conditions A1
- A5 are exactly the set of lines and functions CCW, D in the
Euclidean geometry of R^2.

TEHOREM 2. The set of lines obeying conditions A1-A2 are exactly the
set of lines in the Euclidean geometry of R^2.

THEOREM 3. The set of lines and function CCW obeying conditions A1-A3
are exactly the set of lines and function CCW in the Euclidean
geometry of R^2.

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

Harvey Friedman