[FOM] 212:On foundations of special relativistic kinematics 4
Harvey Friedman
friedman at math.ohio-state.edu
Sat Feb 7 18:28:19 EST 2004
I now have a better understanding of the rather extensive literature on
basic axioms for special relativity. When I wrote
On foundations of special relativistic kinematics 1-3
I was not familiar with the following two important items:
1. The rather extensive and detailed and voluminous ongoing work of Andreka
and Nemeti,
2. In particular, the Aleksandrov Zeeman theorem, extensively quoted and
used by Andreka and Nemeti.
Looking at the AZ theorem, it is virtually immediate that my axioms can be
seriously simplified by just eliminating the vector axiom entirely.
We will restate my axioms below from scratch, in an entirely self contained
way. But first some remarks.
In looking at some principal works by Andreka and Nemeti, it is clear that
the axiomatization of special relativity (kinematics) that they *emphasize*
differs somewhat from ours in several ways (minor and major).
A major difference is our use of the SIMULTANEOUS DISTANCE AXIOM. They
emphasize a symmetry axiom about relative velocities of observers. A key
factor in their emphasizing this is that in my approach via the SIMULTANEOUS
DISTANCE AXIOM, I need at least 2 space dimensions; otherwise things go
badly. Whereas in their emphasized approach, they are just fine with just 1
space dimension.
I had thought that my use of the SIMULTANEOUS DISTANCE AXIOM here was new.
HOWEVER, Andreka and Nemeti have informed me that they discuss the
SIMULTANEOUS DISTANCE AXIOM thoroughly in parts of their forthcoming 1000+
page book, after Chapter 1. In the early parts of their many long works, the
SIMULTANEOUS DISTANCE AXIOM is not used - other principles of a different
character are used. So I was surprised to see Nemeti's recent FOM posting On
foundations of special relativity, 2/5/04, 5:13PM.
There are still some differences. I use c as a constant, whereas
Andreka/Nemeti prefer to use only geometric coordinates. Other than c, my
primitives are more minimal - no photons, and observers do not sit in event
space. That, in my setup, is a derived notion. Also, I use a maximality
axiom, to get categoricity. Also in the first order version, not discussed
in installments 1-3, but discussed below, I use my first order maximality
axiom T(max) - which I used to give a first order formulation of Hilbert's
axioms for plane Euclidean geometry. See my posting 205:First Order Extremal
Clauses 1/18/04 2:25PM.
The whole matter of exact choices of axioms for this elementary corner of
physics may seem utterly trivial to both mathematicians and physicists.
However, consider this:
**What happens when we scale up from this elementary corner of physics to
physics of much grander scope and complexity?**
I believe in gaining a deep understanding of simple things first before
getting into complex things. In my experience, there is always much more to
say about simple things, of a deeply clarifying character, than is normally
realized.
As a stepping stone to more complex matters orthogonal to special
relativistic mechanics, I would like to see what can be done in a deeply
clarifying way with, for instance, classical
Newtonian/Lagrangian/Hamiltonian mechanics.
Also recall that I wanted to use this very basic situation in the beginnings
of special relativity as a particularly TRANSPARENT example of foundational
thinking, outside the very substantial and varied examples we all know about
from the foundations of mathematics.
In fact, I now believe that there are perhaps over 500 corners of physics,
many surrounding key experiments, which admit of intellectually related
foundational treatment in the general style of the foundations of
mathematics.
In the next installments, I want to take up
i) the "conceptual derivation" of the Minkowski space, which we have
deliberately avoided as the starting point of special relativity;
ii) what I call observational foundations of special relativistic
kinematics, where the general concept of event is not present.
The restatement below is self contained, and also corrects some earlier
errors.
$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$
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.
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 O 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 subtracting 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. LIGHT SPEED axiom. c > 0.
4. LIGHT PATH axiom. Let two events be given. If some observer thinks that
the Euclidean distance between the two events is c times the time interval
from the first event to the second event, then every observer thinks so.
5. SIMULTANEOUS DISTANCE axiom. Let two events be given. Any two observers
that agree that the two events are simultaneous, agree on their Euclidean
distance.
6. 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).
Note that the "real physics", whatever that means, is contained in axioms 4
and 5. Presumably, a physicist might not even notice the remaining axioms.
Note also that we do not use photons among our primitives, and we also do
not place observers in event space. These are all derived notions in this
approach.
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 real 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.
THEOREM 3. For c > 0, there is an automorphism of SRK(MATH,c) carrying any
observer to any other observer.
We now discuss the structure of the SRK(MATH,c).
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. There are many equivalent
commonly used definitions. One is that it is a linear transformation T:R^4
into R^4 which preserves the Minkowski inner product, and where T(1,0,0,0)
has positive first coordinate.
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 of the
form T(x) = S(x) + y, where T is a Lorentz transformation.
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 4. The automorphism group of SRK(MATH,c) is isomorphic to the
Poincare group in R x R^3 = R^4.
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 5. 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 translates of the c-Lorentz
transformations, where the c-Lorentz transformations are of the form
T(x,y,z,w) =
(T'(cx,y,z,w)_1/c,T'(cx,y,z,w)_2,T'(cx,y,z,w)_3,T'(cx,y,z,w)_4)
where T' is a Lorentz transformation in R x R^3 = R^4.
Here the subscripts 1,2,3,4 indicate the 1st, 2nd, 3rd, 4th coordinates.
Or we can define the c-Poincare transformations in R x R^3 = R^4 directly
using the above equation, where T' is a Poincare transformation.
The c-Lorentz transformations also form a group. In fact, the group of
Lorentz transformations is isomorphic to the group of c-Lorentz
transformations via the defining equation above, where T' is sent to T. The
same for the group of c-Poincare transformations and the Poincare
transformations.
The autonomous axiomatization - in first order logic - is given by
i) adding the axioms for a Pythagorean ordered field;
ii) stating the maximality axiom as follows:
6'. MAXIMALITY axiom (first order). No proper extension of this three sorted
system, definable in the system, exists.
Axiom 6' is exactly in accordance with my first order version of Hilbert's
axiomatization of Euclidean plane geometry, via what I call T(max). See my
posting 205:First Order Extremal Clauses, 1/18/04, 2:25PM.
These axioms imply that the underlying field is a real closed ordered field,
and so we get completeness.
*********************************************
I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 211th 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 1/26/04 12:18AM
208:On foundations of special relativistic kinematics 3 1/26/04 12:19AAM
209:Faithful Representation in Set Theory with Atoms 1/31/04 7:18AM
210:Coding in Reverse Mathematics 1 2/2/04 12:47AM
211:Coding in Reverse Mathematics 2 2/4/04 10:52AM
Harvey Friedman
More information about the FOM
mailing list