[FOM] 716: Foundations of Geometry/4

[Harvey Friedman]

We now crystallize the logical structure of this approach. We now want
to be very careful about the primitives and the second order axioms.
We now realize that it is best to load up on the primitives, as long
as we have a clear picture of them in the mind's eye, geometrically.

There are three sorts. We use equality on all three. R, P, L. R =
reals, P = points, L = lines.

1. <, +, -, 0, 1, | |, and the operation x/2, all on sort R.
2. The two coordinate functions x_1, x_2 mapping points to reals. Also
the pairing function mapping two reals to a point. (The points are
like ordered pairs of reals).
3. Point lies on line. M for membership.
4. Function symbol for 90 degree counterclockwise rotation from a
point about a point. CR for counterclockwise rotation.
5. The reflection function symbol which sends a line and a point to
its reflection about the line. RF for reflection.
6. The distance function symbol, which maps pairs of points to reals.
D for distance.

Below are the first order axioms that we have been informally talking
about, which are evident truths in the mind's natural intuitive
geometric eye:

A1. In R, the usual axioms for an ordered abelian group with halving.
(See second order axiom below).
A2. Two points are equal if and only if their coordinates are equal.
The pair of the first and second coordinates of a point is the point
itself.
A3. Two lines are equal if and only if they have the same points.
Lines have at least two points on them. For any two distinct points,
there is a unique line through these points. Every line is disjoint
from some line. If (a,b) and (c,d) lie on L then so does
((a+c)/2,(b+d)/2). Let x,L be given. Suppose for all epsilon > 0 there
exists y on L such that x,y have their respective coordinates within
epsilon of each other. Then x lies on L.
A4. The 90 degree counterclockwise rotation about (a,b) is (a,b) at
(a,b); (a,b+1) at (a+1,b); (a-1,b) at (a,b+1). For each (a,b), 90
degree counterclockwise rotation about (a,b) is line preserving
(obvious definition for line preserving).
A5. Reflection about L
  a. is line preserving.
  b. has fixed points exactly the points on L.
  c. Is an involution.
  d. sends any point x not on L to a point y not= x not on L, where
the line through x,y and L meet at exactly point z, and the 90 degree
counterclockwise rotation about z sends x,y to points on L.
A6. The distance between (a,b) and (a,c) is |b-c|. Reflection about L
is distance preserving.

Second order axiom:

S1. Every nonempty upper bounded set of real numbers has a least upper bound.

Betweenness can be added to these axioms as an explicit definition in
terms of the coordinates of the three points, using < on R. This is
obviously optional - to have this explicit definition.

Note that 1-6 defines our second order language L2 where we use the
symbols in 1-6 together with the tiny fragment of second order logic
which has only free second order variables for subsets of R. Here the
2 in L2 means "second order". T2 is the system in L2 with axioms
A1-A6,S1.

THEOREM 1. T2 is categorical. I.e., any two models are isomorphic.

We now consider fragments. We have the fragment languages L2[R],
L2[R,P], L2[R,P,M], L2[R,P,M,CR], L2[R,P,R,P,M,CR,RF], L2 based on 1,
1-2, 1-3, 1-4, 1-5, 1-6 above, all of which have the aforementioned
tiny fragment of second order logic (and equality on each of the three
sorts). We have the respective second order theories T2[R], T2[R,P],
T2[R,P,M], T2[R,P,M,CR], T2[R,P,M,CR,RF], T2 based on A1, A1-A2,
A1-A3, A1-A4, A1-A5, A1-A6, all of which also have S1.

THEOREM 2. The fragments T2[R], T2[R,P], T2[R,P,M], T2[R,P,M,CR],
T2[R,P,M,CR,RF] of T2 are categorical.

We now take up the first order version of this approach. The crudest
way to proceed is to take each of the above fragments, and replace S1
by the axiom scheme using only formulas in their respective language
without the second order part. These fragments are referred to as
T1[R], T1[R,P], T1[R,P,M], T1[R,P,M,CR], T1[R,P,M,CR,RF], T1.

THEOREM 2. T1 is complete. So are the fragments T1[R], T1[R,P],
T1[R,P,M], T1[R,P,M,CR], T1[R,P,M,CR,RF]. All but T1[R] is mutually
interpretable with RCF = real closed fields.

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

Harvey Friedman