[FOM] 208:On foundations of special relativistic kinematics 3

[Harvey Friedman]

$$My apologies to everybody in the world who did anything similar or
overlapping or the same. I hope readers find this to be unusually
transparent.$$

A MATHEMATICAL AXIOMATIZATION OF SPECIAL RELATIVISTIC KINEMATICS.

As I said in postings #206, #207, the plan is to have

i) observational foundations of special relativistic kinematics, with only
observationally meaningful notions. In particular, no general concept of
event. There will be only the emitting and receiving of light;

ii) theoretical foundations of special relativistic kinematics. This is what
is being discussed, solely, in this posting.

iii) detailed relationships between i) and ii).

We further subdivide ii) into

iia) mathematical axiomatization of special relativistic kinematics. This
posting.

iib) autonomous axiomatization of special relativistic kinematics. Next or
later posting.

In later postings, we will take up iib).

We call this mathematical axiomatization SRK(math). We call the autonomous
axiomatization SRK(aut).

We declare three sorts of objects. One sort is for observers. Another sort
is for events. The third sort is for real numbers. We have the usual
<,0,1,+,-,x on the real numbers.

We have equality between observers and equality between events and equality
between real numbers.

We have four binary function symbols, TC,XC,YC,ZC. For each of the four, the
first argument must be an observer, the second argument must be an event,
and the value must be a real number.

Finally, we have a constant symbol c for a real number that represents the
speed of light in a vacuum.

We read 

TC(O,E) for the time coordinate of the event E according to observer O.
XC(O,E) for the x-coordinate of the event E according to observer O.
YC(O,E) for the y-coordinate of the event E according to observer O.
ZC(O,E) for the z-coordinate of the event E according to observer O.

Before giving the axioms, some comments are in order.

a. Setting this up very cleanly and explicitly as a three sorted theory in
first order predicate calculus, can be viewed as a TRIVIAL modification of
the usual way people present special relativistic kinematics, with their
potentially loaded terms like reference frames, etc. But look how comforting
it is. Particularly so for people familiar with f.o.m.

And why is it so comforting? Because there is expectation that absolutely
all hidden assumptions will be made absolutely explicit - as opposed to
listening to physicists. Of course, if hidden assumptions creep into the
treatment, then there will be a violent backlash against this sort of
approach...

The expectation is that in much more sophisticated/complex physical science,
it will be even more comforting to see an imaginatively identified sort
setup. E.g., in theoretical foundations of general relativity. This is a
tool that should help put us on the road towards a unified foundation for
physical science. 

b. Each observer has his/her own personal ordinary Euclidean space/time
coordinates of every event. The axioms deal mostly with the relationships
between the space/time coordinates of different observers regarding the same
events. 

c. I borrow the term "event" as it is now very standard. I mean it here in
the sense of "a location in world history". Actual events occur at a unique
location in world history. A great insight of Einstein is that "a location
in world history" is a much more subtle notion than Newton thought,
involving a highly nonobvious weaving together of temporal and spatial
ideas.  

Here are the axioms of SRK(math). We state them informally. The formal
statements are obvious.

First some completely obvious simple friendly standard defined notions from
high school math. Let O be an observer and E and E' be events.

The position of E according to 0 is the list of real numbers

(TC(O,E),XC(O,E),YC(O,E),ZC(O,E)).

The vector from E to E' according to O is obtained by substracting the
position of E according to 0 from the position of E' according to O,
coordinatewise.

The time interval from E to E' according to O is the real number

TC(O,E') - TC(O,E).

Note that time intervals can be positive, negative, or zero.

The distance from E to E' according to O is the ordinary Euclidean distance
between the triples

(XC(O,E), YC(O,E), ZC(O,E)) and (XC(O,E'), YC(O,E'), ZC(O,E'))

as points in Euclidean three space. Thus the distance from E to E' according
to O must be a nonnegative real number.
 
1. Coordinate axiom. According to any observer, every list of four real
numbers are the time, x-, y-, z- coordinates of some unique event.

2. Identification axiom. If two observers agree on the coordinates of every
event, then the two observers are the same.

3. Vector axiom. Let four events be given. If some observer thinks that the
vector from the first event to the second event is the same as the vector
from the third event to the fourth event, then every observer thinks so.

4. Simultaneous distance axiom. Let two events be given. Any two observers
that agree that the two events are simultaneous, agree on their Euclidean
distance. 

5. Light path axiom. Let two events be given. If some observer thinks that
the time interval from the first event to the second event is c times the
Euclidean distance between the two events, then every observer thinks so.

6. Light speed axiom. c > 0.

7. Maximality axiom. No proper extension of this three sorted system,
preserving the real numbers, exists.

This completes the mathematical axiomatization for special relativistic
kinematics, SRK(math).

The "math" in SRK(math) indicates that the models of SRK(math) must have
third sort the set of all reals, with the usual <,0,1,+,-,x.

In fact, it will be useful to state the form of the models of SRK(math).
They are structures of the form

(OBS,EVE,RLS,TC,XC,YC,ZC,c,<,0,1,+,-,x)

where OBS,EVE are nonempty sets, RLS is the set of all real numbers,
TC,XC,YC,ZC are functions from OBS x EVE into RLS, c is some rela number, <
is the usual ordering on the reals, 0,1 are the usual real numbers, +,x are
usual binary addition and multiplication operations on the reals, and - is
the usual unary additive inverse on the reals.

THEOREM 1. Any two models of SRK(math), with the same c, are isomorphic. Any
such isomorphism is the identity on the mathematical part (i.e., the
identity on the third sort).

By Theorem 1, we can speak of *THE* model of SRK(math) with a given c, as it
is unique up to isomorphism with respect to the ordered real field. This is
an essential point, which is stronger than mere isomorphism.

Thus for any c > 0, we write SRK(MATH,c) for the unique model (up to
isomorphism) of SRK(math) with constant c. Note the capitalization of MATH
to avoid confusion with the set of axioms, SRK(math).

THEOREM 2. If SRK(MATH,c) and SRK(MATH,d) are isomorphic, then c = d.

We now discuss the structure of the SRK(MATH,c).

THEOREM 3. There is no preferred observer in SRK(MATH,c). I.e., SRK(MATH,c)
has an automorphism which sends any given observer to any other given
observer. 

THEOREM 4. There is no preferred event in SRK(MATH,c). I.e., SRK(MATH,c) has
an automorphism which sends any given event to any other given event.

THEOREM 5. In SRK(MATH,c), the events are rigid with respect to the
observers, and the observers are rigid with respect to the events. I.e.,
every automorphism that fixes the observers, fixes the events. And every
automorphism that fixes the events, fixes the observers.

The Lorentz transformations in R x R^3 = R^4 form a well known specific
group of linear transformations from R^4 onto R^4. At this point, let us not
worry just which these are. We just need to know that they form a group
under composition. 

The Poincare transformations (perhaps not standard terminology) in R x R^3 =
R^4 is the specific group of affine transformations from R^4 onto R^4 given
by

T(x) = S(x) + y

where S is a Lorentz transformation in R x R^3 and y is an element of R^4.

The Lorentz group in R x R^3 = R^4 is the group of all Lorentz
transformations in R x R^3 = R^4. The Poincare group in R x R^3 = R^4 is the
group of all Poincare transformations in R x R^3 = R^4.

Note that the Lorentz transformations in R x R^3 = R^4 are exactly the
Poincare transformation in R x R^3 = R^4 that map the origin of R^4 to the
origin of R^4.

THEOREM 6. The automorphism group of SRK(MATH,c) is isomorphic to the
Poincare group in R x R^3 = R^4.

There is a sharpening of the idea that the automorphism group of a many
sorted relational structure is isomorphic to particular group. This
sharpening is the existence of what is called a group action.

Also note that the automorphism group is independent of the choice of c.
Contrast this with Theorem 2.

Let G be a group and X be a nonempty set. An action of G on X is a function
dot:G x A into A such that

i) 1 dot x = x, where 1 is the identity of G;
ii) gh dot x = g dot (h dot x).

It then follows that for every g in G, the function of x,

g dot x

is a permutation of X. These are called the fibers of the action.

THEOREM 7. The Poincare group in R x R^3 acts on the domain of any model of
SRK(MATH,c), in such a way that the fibers are exactly the automorphisms of
the model. 

We can of course be more explicit about how the Poincare group enters the
picture. 

Let M be a model of SRK(MATH,c), and let O and O' be two observers, which
may or may not be distinct. If they are distinct, then they disagree on the
coordinates of some events.

We wish to compare the coordinates of O and O', in the model M. We let
M[O,O'] be the function that transforms O's coordinates to those of O'. So

M[O,O']:R^4 into R^4.

The function M[O,O'] is defined as follows.

Let t,x,y,z be real numbers, thought of as O's coordinates. In the hands of
O, these are the coordinates of a unique event E. Now this event E, in the
hands of O', has coordinates t',x',y',z'.

Thus we set 

M[O,O'](t,x,y,z) = (t',x',y',z').

THEOREM 8. In SRK(MATH,1), the functions M[O,O'] are exactly the Poincare
transformations in R x R^3 = R^4. Furthermore, M[O,O''] is the composition
of M[O,O'] and M[O',O''].

For the general case of c > 0, we get what we call the c-Poincare
transformations in R x R^3 = R^4. These are the transformations of the form

T(x,y,z,w) = 
(cT'(x/c,y,z,w)_1,T'(x/c,y,z,w)_2,T'(x/c,y,z,w)_3,T'(x/c,y,z,w)_4)

where T' is a Poincare transformation in R x R^3 = R^4.

Here the subscripts 1,2,3,4 indicate the 1st, 2nd, 3rd, 4th coordinates.

The c-Poincare transformations also form a group. In fact, the group of
Poincare transformations is isomorphic to the group of c-Poincare
transformations via the defining equation above, where T' is sent to T.

To be continued...

i. Careful definition of relative velocities of observers, and velocity
addition.
ii. Associating a space to the SRK[MATH,c], uniquely. (Minkowski).
iii. Autonomous axiomatization, theories SRK[aut], SRK[aut,c], models
SRK[AUT,c].
iv. Observational foundations.
v. Logical relationships between observational and theoretical foundations.
vi. General relativity.

*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 208th 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-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM
186:Grand Unification 1  7/2/03  10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03  4:43AM
189:Some Model theoretic Pi-0-1 statements  9/25/03  11:04AM
190:Diagrammatic BRT 10/6/03  8:36PM
191:Boolean Roots 10/7/03  11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement  11/2/03  4:42PM
194:PL Statement/clarification  11/2/03  8:10PM
195:The axiom of choice  11/3/03  1:11PM
196:Quantifier complexity in set theory  11/6/03  3:18AM
197:PL and primes 11/12/03  7:46AM
198:Strong Thematic Propositions 12/18/03 10:54AM
199:Radical Polynomial Behavior Theorems
200:Advances in Sentential Reflection 12/22/03 11:17PM
201:Algebraic Treatment of First Order Notions 1/11/04 11:26PM
202:Proof(?) of Church's Thesis 1/12/04 2:41PM
203:Proof(?) of Church's Thesis - Restatement 1/13/04 12:23AM
204:Finite Extrapolation 1/18/04 8:18AM
205:First Order Extremal Clauses 1/18/04 2:25PM
206:On foundations of special relativistic kinematics 1 1/21/04 5:50PM
207:On foundations of special relativistic kinematics 2