[FOM] On foundations of special relativity

[Istvan Nemeti]

Harvey Friedman encouraged us to write a [FOM] posting on our work on,
and approach to, Foundations of relativity. One direction in our work is
the following.

AN AUTONOMOUS OBSERVATION ORIENTED AXIOMATIZATION OF SPECIAL
RELATIVISTIC KINEMATICS

Disclaimer: In our approach the above title is not the end of the story
but, instead, it is the beginning. Namely: axiomatizations of relativity
are not ends in themselves (goals), instead, they are only tools, in our
approach. Our goals are what Harvey Friedman summarized in his [FOM]
essays of Jan 20 01:17:00 and Jan 21 17:50:00. I.e. the goals are
obtaining simple, transparent, easy-to-communicate insights into the
nature of relativity, to get a deeper understanding of relativity, to
simplify it, to provide a foundation for it. A further aim is making
relativity accessible for many people (as fully as possible).

LANGUAGE

We declare two sorts of objects. One sort is for "quantities". This is
the same as Harvey's sort "real numbers", except that we will treat it
"autonomously", i.e. we will postulate that this sort with the
appropriate function and relation symbols form a linearly ordered field.
This sort will be denoted by F (for field).

The other sort, B, is for bodies (which do the "moving"). We have two
kinds of special bodies, observers and photons. Thus  Obs  and Ph  are
unary predicate symbols of sort B.

The "heart" of our models is the world-view relation W. The sentence
"observer o  observes body  b  at spacetime location  t,x,y,z" is
denoted as  W(o,b,t,x,y,z). Hence  W  is a relation of sort  B x B x F x
F x F x F. Here observing does not mean any special kind of act--- like
e.g. visual observing via photons---, instead, it simply means
coordinatizing.

Intuitively, each observer has his own personal ordinary Euclidean
space/time coordinates for every event. Following Einstein, we identify
an event with a set of bodies. An event is regarded as the set of those
bodies which were present in that event. Since "events" can be reduced
to "bodies", it is enough to have "observers" and "bodies" in our
language as primitives.

AXIOMS

Axiom 1.  Each observer observes himself on the "time-axis" of his
co-ordinate system. I.e., each observer  o  observes himself (as a body)
exactly at those spacetime locations (t,x,y,z) where (x,y,z)=(0,0,0).  

(As a first-order formula this is 
Obs(o) -> [W(o,o,t,x,y,z) <-> x=y=z=0], where  0  denotes the zero of
the field F. Later we will not spell out the exact formulas.)

Axiom 2.  Any observer  o  sees two points  p,q  connected by a photon
iff the slope of the line connecting  p  and  q  is 1. (By points we
understand 4-tuples  p=(t,x,y,z) of elements of  F.) In other words: in
each observer's co-ordinate system there is a photon observed both at  p
and  q  exactly if the "spatial distance" between  p  and  q  is the
same as the "time-distance" between  p  and  q.

Here the spatial distance between  p=(t,x,y,z) and q=(s,u,v,w) is the
positive square root of (x-u)^2 + (y-v)^2 + (z-w)^2, and the
time-distance between  p  and  q  is |t-s|, like in Harvey's FoSRK3
posting.

By an " event occurring at  p  for  o " we understand the set of bodies
o  observes at  p.

Axiom 3.  Let o1 and o2 be two observers. All events which exist for
o1,  exist for  o2, too. I.e., the event observed by  o1  at  p  is
observed by  o2  as well, perhaps at a different point q.

Axiom 4.  (F,<,+,x) is a linearly ordered field in which every positive
member has a square root.

Most of the interesting predictions of relativity can be proved (in the
rigorous manner of first-order logic) from the above 4 axioms. For the
rest we will use one more axiom.

Axiom 5.  Let two events be given. Any two observers that agree that the
two events are simultaneous, agree on their spatial distance.

Remark: Later we want to use the number  n  of dimensions of spacetime
as a variable, instead of the present  n=4 convention.  Axiom 5 above as
formulated does not work for the special case of  n=2. But it has an
equivalent version that works for all  n.  Cf.  AxSym  in our paper [1].

THEOREM 1. Our axiom system Axiom 1 - Axiom 5  is irredundant. I.e. no
axiom follows from the rest.

Proof can be found in [2].

Axioms 1-4 imply that "no faster than light observers exist", formalized
as follows.  NoFTL abbreviates the statement that for any observers o1,
o2, observer o1 will not "measure" the speed of  o2  as greater than
that of a photon.

Throughout |= is the usual consequence relation of first-order logic.

THEOREM 2.  Axioms 1-4 |= NoFTL.

This is Corollary 2.1 in [1].

THEOREM 3. Dropping any one of the axioms from Theorem 2 makes the
conclusion false.

Remark: For various reasons, "NoFTL" is an important issue in the
literature of relativity. E.g. the fact that for 2-dimensional
spacetimes FTL becomes possible (i.e. Theorem 3 does not extend to n=2)
plays a role in understanding the geometry of black holes. It is
important for other reasons as well. Because of this, we analyzed the
logical "causes" of Theorem 2 (NoFTL) in [3, section 3.4.2]. We found
that the cause is that being a photon  Ph  is a predicate independent
from observers. I.e. what is a photon for  o1  is also one for  o2. This
is an assumption of relativity theory which is built into the choice of
the language. It is not quite obvious that this assumption is completely
justified. (E.g. a photon for  o1  could be a tachion for  o2.)

The most frequently quoted predictions of special relativity are the
following three paradigmatic effects.
(i) moving clocks slow down
(ii) moving meter-rods shrink
(iii) moving pairs of clocks get out of synchronism.
These three effects are easily formulated in the first-order logic
language introduced so far. (These formulations can be found in our
papers.)

Axioms 1-4 already prove paradigmatic effects (i)-(iii) in qualitative
form, e.g.

THEOREM 5. Axioms 1-4 |= "Let o1,o2 be observers in relative motion.
Then one of them will observe that the clocks of the other run slow."

THEOREM 6. Axioms 1-5 |= "Let o1,o2 be observers in relative motion.
Then  o1  will observe that the clocks of  o2  run slow. Moreover, the
rate of slowing is the same function of their relative speed that can be
found in the relativity books."

In this context we would like to refer to Harvey's posting of Jan 24
05:14:58 (Knowledge - quantity/quality).

Similar statements are true for the other paradigmatic effects:

Axioms 1-4 |= qualitative forms of all three paradigmatic effects,
Axioms 1-5 |= quantitative forms of all three paradigmatic effects.

In the present first-order logic framework, one can also formulate a
version of the Twin Paradox. Now,

THEOREM 7.  Axioms 1-4 "not |=" Twin Paradox, but  
            Axioms 1-5      |=  Twin Paradox.

Details can be found in e.g. [1] or [3].

PROPOSITION 8. Axioms 1-4 |= "The world-view transformations  M[o1,o2]
are of the form (Poincare transformation composed with a dilation
composed with a field-automorphism-induced function)."

Here the world-view transformation  M[o1,o2] : F^4 -> F^4  is the
natural coordinate-transformation between the world-view of  o1  and
o2, as in Harvey's FoSRK3 posting.

PROPOSITION 9. Axioms 1-5 |= "M[o1,o2] is a Poincare transformation, for
every o1, o2."

Remark: We could have proved Theorems 5-7 by first deriving Poincare
transformations as in Propositions 8,9 and then deriving the
paradigmatic effects (i)-(iii) from the Poincare property. However, we
think this would be less helpful than the present approach. Namely, we
think that deriving the predictions of relativity directly from the
axioms is more helpful for various reasons.: (1) This way we can do
something like reverse mathematics for relativity, namely we can analyze
the question "which axiom is responsible for what prediction". (2) For
the student, Minkowski geometry and Poincare transformations are
non-observation oriented theoretical constructions which are
authoritative articles of faith not explaining why we are doing what we
are doing. Compare the paragraph on "prematurely introducing the
Minkowski inner product or the Lorentz group" in Harvey's posting of Jan
21 17:50:00 FoSRK1.

CATEGORICITY

We do not put too much emphasis on making our theories categorical,
because we found that this property is not particularly helpful in
connection with the logical analysis of relativity. All the same, by
adding a few book-keeping axioms to Axioms 1-5, one obtains an
observational autonomous theory which is *categorical* over the field
sort (F,<,+,x). This is shown in [4, section 6] as well as in [3,
section 3.8.3].

***

The approach outlined so far is an *observationally oriented autonomous*
one.

The reason why we emphasize such approaches is that both property
(observation-oriented, autonomous) forces the author to make tacit
assumptions EXPLICIT in the spirit of Harvey's postings.

One can also study by logical methods the connections between the
present (observational, autonoumous) axiom system and Harvey's
mathematical, theoretical one in his posting FoSRK3, as follows.

One obtains an autonomous theoretical version of Harvey's axiom system
SRK(math) by replacing the condition that the third sort is the standard
real line with the one that it is a Euclidean ordered field, and by
reformulating his axiom 7 accordingly (as done e.g. in [2, section 6]).

Now, we can use DEFINABILITY THEORY of many-sorted first-order logic to
study the connection between the so obtained version of Harvey's system
and ours. Actually, one can prove that the two first-order theories are
definitionally equivalent (modulo adding some book-keeping axioms to
ours). Such an investigation is carried through in [3, chapter 6]. 

We note that for the investigation one has to extend the definability
theory of many-sorted logic to defining new universes, i.e. new sorts.
The beginning of such an extension is in Chapter 12 of Hodges' book [5],
while the whole story is in [3, chapter 6.3]; but cf. also Makkai [6].

References

[1] Andreka-Madarasz-Nemeti: Logical axiomatizations of space-time.
Samples from the literature.
[2] Andreka-Madarasz-Nemeti: Logical analysis of special relativity
theory.
[3] Andreka-Madarasz-Nemeti: On the logical structure of relativity
theories.
[4] Andreka-Madarasz-Nemeti: Logical analysis of relativity theories.
[5] Hodges, W.: Model Theory, Cambridge University Press, 1993.
[6] Makkai, M.: Duality and Definability in First Order Logic. Memoirs
of the AMS, No 503 (Vol. 105), 1993.

[1]-[4] above can be found at
http://www.math-inst.hu/pub/algebraic-logic/Contents.html