Logical analysis of special relativity theory

Hajnal Andréka, Judit X. Madarász, and István Németi^{∗}

Abstract

Here we outline an approach to a logical analysis of relativity theory conducted purely in first order logic (for methodological reasons). Here we concentrate on special relativity, but in a more extensive work referred to here as [2], some steps are made in the direction of generalizing the present approach towards general relativity. In [2] we build up variants of relativity theory as “competing” axiom systems formalized in first order logic. The reason for having several versions for the theory, i.e. several axiom systems, is that this way we can study the consequences of the various axioms, enabling us to find out which axiom is responsible for some interesting or “exotic” prediction of relativity theory. Among others, this enables us to refine the conceptual analysis in Friedman’s and Rindler’s books, or compare the Reichenbach-Grünbaum approach to relativity with the standard one. After having formalized relativity in first order logic, we use the well developed machinery of first order logic for studying properties of the theory (e.g. the number of non-elementarily equivalent models, or its relationships with Gödel’s incompleteness theorems, independence issues etc). In the present paper, first we recall one of our axiom systems “Specrel” for relativity from [2]. Then we present some of the typically logical investigations of Specrel, e.g. independence of the axioms, consistency properties of models. We also discuss the intuitive contents (and consequences) of some of the axioms. We also present a little bit of the conceptual analysis part of [2] using the example of Specrel and “FTL observers”. Finally, we study how much Gödel’s incompleteness theorems apply to Specrel: Specrel is undecidable, and it admits natural extensions some of which are decidable, while to others the full strength of both of Gödel’s incompleteness theorems applies. E.g. there is an extension Specrel^{+} in which its own consistency is formalizable (and is neither provable nor refutable). Specrel^{+} is hereditarily undecidable. We deliberately try to keep the number of axioms in Specrel small, and their intuitive contents simple, transparent, and tangible from the logical point of view.

Contents

1 Introduction 3

2 The frame language 4 3 Basic axioms of special relativity 7 4 Traveling with light, traveling faster than light 9 5 A principle of relativity 14 6 Axioms making Specrel categorical 15 7 Decidability and Gödel incompleteness 16 8 Appendix 19 We dedicate this paper to Johan on his 50’th birthday.

∗Supported by Hungarian National Foundation for Scientific Research grants T30314, T23234.

1 Introduction

In this paper we try to give a small sample illustrating the approach of Andréka et al. [2] to a logical analysis of relativity theory conducted purely in first order logic (for methodological reasons). Here we concentrate on special relativity, but in [2] steps are made in the direction of generalizing the approach towards general relativity. In [2] we build up variants of relativity theory as “competing” axiom systems formalized in first order logic. The reason for having several versions for the theory, i.e. several axiom systems, is that this way we can study the consequences of the various axioms, enabling us to find out which axiom is responsible for some interesting or “exotic” prediction of relativity theory. Among others, this enables us to refine the conceptual analysis in Friedman [6] and Rindler [10], or compare the Reichenbach-Grünbaum approach to relativity (cf. L. E. Szabó [12] or [6]) with the standard one.

As explained in [2], the present approach is (in some sense) more ambitious (as a relativity theory) than e.g. a formalization of, say, Minkowskian geometry in first order logic would be, in various respects: (i) One respect is that if we identified Minkowskian geometry with special relativity, then this would yield an uninterpreted (in the physical sense) version of relativity, while the first order theory which we develop in [2] contains “its own interpretation”, too. (ii) It is not clear to us how the conceptual analysis^{1} suggested e.g. in [6] (or the Reichenbach-Grünbaum issues) could be squeezed into Minkowskian geometry. (iii) Our formalized relativity theory is undecidable, while the first order version of Minkowskian geometry in [7] is decidable, pointing in the direction that perhaps in our theory one can talk about things which do not appear in the pure Minkowskian geometry. Someone may argue that Minkowskian geometry is the heart of special relativity theory, but it is only the heart; and we would like to formalize the full theory and not only its heart. (iv) The observational/theoretical duality outlined in [6] motivates us to keep our vocabulary and axioms on the observational side (while Minkowskian geometry remains more on the “theoretical” side).

After having formalized relativity in first order logic, one can use the well developed machinery of first order logic for studying properties of the theory (e.g. the number of non-elementarily equivalent models, or its relationships with Gödel’s incompleteness theorems, independence issues, etc). The ideas in Johan’s [5] (combined with the ones in the version of Sain [11] updated during the A’dam-Budapest cooperation) explain why we have to insist on keeping our axiomatic relativity theory within (possibly modal and many-sorted) first order logic. For a more comprehensive introduction and for more connections with Johan’s (or Tarski’s, Suppes’, Goldblatt’s etc) work we refer to [2].

1Which axiom is responsible for what, which axiom is intuitively more natural than the other, etc.

2 The frame language

We introduce the first order language, which we will use for formalizing (special) relativity.

We want to talk about \underline{motion of bodies}.^{2} What is motion? It is changing location in time. Therefore we will talk about \underline{bodies}, \underline{time}, \underline{space}, and about a \underline{location-function} which tells us which body is where at a given time. We want to talk about \underline{relativity} theories; therefore these location functions will depend on \underline{observers}; different observers may see the same motion differently. (The location function determined by an observer m will be called the world-view function w_{m} of observer m.) We will treat observers as special bodies whose motion will (of course) be represented exactly the same way as that of the rest of the bodies. These observers are often called, in the literature, \underline{reference frames}.^{3}

It will be convenient for us to be flexible about the dimension of space: we will not only treat 3-dimensional space, but 1 or 2, or higher-dimensional spaces also. We will treat time as a special dimension of \underline{space-time}. n will denote the dimension of our space-time. Thus, usually n = 4 (3 space-dimensions and 1 time-dimension), but we will consider also n = 2, 3 or n > 4. Our bodies will be idealized, pointlike.^{4}

The vocabulary of our language is the following: unary relations

B (bodies)

Obs (observers)

P h (photons)

Q (quantities used for giving location and “measuring time”);

an n + 2-ary relation, the \underline{location-} or \underline{world-view} relation

W (world-view relation, W (m, b, t, s_{1}, …, s_{n−1}) intends to mean that according to observer (or reference-frame) m, the body b is present at time t and location (s_{1}, …, s_{n−1}));

for dealing with quantities, we will have two binary functions, and a binary relation:

+, ·, ≤.

In our theories, we will always assume the following:

• observers and photons are bodies • W (m, b, t, s_{1}, …, s_{n−1}) implies that m is an observer, b is a body, and

2In this paper we concentrate only on kinematics; the same kind of investigations can be carried out concerning mass, forces, energy etc. But if a theorem can be proved without referring to these extra notions, we consider that a virtue.

3The difference is only a matter of terminology and we do not find it important from the point of view of the present work.

4From the point of view of the questions studied here this does not restrict generality.

If some reader would prefer “fat observers” to “thin observers”, we can always identify an observer m with the “reference frame” induced by m, and then this will yield a “fat notion of observer”.

t, s_{1}, …, s_{n−1} are quantities

• (Q, +, ·, ≤) is a Euclidean^{5} linearly ordered field.

We found that the simplest way of treating these assumptions is to use a 2-sorted first-order language, where

B, Q are sorts

Obs, P h are unary relations of sort B

W is an n + 2-ary relation of sort B × B × Q × Q × … × Q

+, · and ≤ are operations and relation of sort Q.

Let

M = ⟨BM, ObsM, P hM; QM, +M, ·M, ≤M; W M⟩

be a model of our two-sorted language. This means that BM and QM are sets, they are called the universes of sort B and Q respectively, ObsM, P hM ⊆ BM etc. We will omit the superscripts M. We call M a \underline{frame-model} if (Q, +, ·, ≤) is a Euclidean linearly ordered field and W ⊆ Obs × B × Q × … × Q. ⊧ denotes the usual semantical consequence relation induced by frame-models, i.e. T h ⊧ φ means that for every \underline{frame-model} M, if M ⊧ T h, then M ⊧ φ.

In [2] we use an expansion of this language to prepare the road for formalizing general relativity theory as well. There we introduce explicit tools for treating geometry: there is a new sort G for “geodesics”, and we also have a certain “metric” on space-time. Here we do not need these (as basic symbols) because they will be first-order definable in our formalized theory of special relativity.

Next we introduce some terminology in connection with arbitrary framemodels M = ⟨B, Obs, P h; Q, +, ·, ≤; W ⟩.

The essence, the “heart” of a frame-model is the world-view relation W. Since W ⊆ Obs × B × ^{n}Q, for every observer m ∈ Obs it induces a function w_{m} : ^{n}Q → {X : X ⊆ B} as follows: for every p ∈ ^{n}Q

w_{m}(p) := {b ∈ B : W (m, b, p)}.

Thus w_{m}(p) is the set of bodies present at space-time location p for m.

We call a set of bodies an \underline{event}, and w_{m} is called the \underline{world-view function} of m, which to each space-time location p tells us what event observer m observes or “sees happening” at location p. ^{6}

The \underline{trace} or \underline{life-line} of a body b according to an observer m is the set of space-time locations where m sees b, i.e.

tr_{m}(b) := {p ∈ ^{n}Q : W (m, b, p)}.

5An ordered field is called \underline{Euclidean} if every positive element has a square root in it, i.e.

if (∀x > 0)(∃y)x = y^{2} is valid in it.

6 ‘‘Seeing” has nothing to do with photons here, it really means “coordinatizing” only.

nQ  p W (m, −, −)  w_{m}  B w_{m}(p)

Figure 1: The world-view function w_{m}.

The world-view function w_{m} can be recovered from the family of traces of all bodies (from ⟨tr_{m}(b) : b ∈ B⟩), and the world-view-relation W can be recovered from all the world-view functions (from ⟨w_{m} : m ∈ Obs⟩). Thus we can “represent” the function w_{m} by the \underline{world-view} of m, which is just the indexed family ⟨tr_{m}(b) : b ∈ B⟩, and which, in turn, we represent by drawing the traces of bodies that we are interested in. See Figure 2.

tr_{m}(b_{3}) tr_{m}(b_{2}) tr_{m}(b_{1})

Figure 2: World-view of m.

We now give some terminology which we will use in our models for special relativity.

Since (Q, +, ·) is a field, we can define n-dimensional straight lines as follows (these will be the life-lines of “inertial bodies”). \overline{0} denotes the \underline{origin}, i.e. \overline{0} = (0, …, 0), where 0 is the zero-element of the field. Let ℓ ⊆ ^{n}Q. We say that ℓ is a \underline{straight line} iff there are p = (p_{0}, …, p_{n−1}), α = (α_{0}, …, α_{n−1}) ∈ ^{n}Q such that α ≠ \overline{0} and

ℓ = {p + r · α : r ∈ Q} = {(p_{0} + r · α_{0}, …, p_{n−1} + r · α_{n−1}) : r ∈ Q}

Lines denotes the set of all straight lines (of dimension n). \overline{t} denotes the \underline{time axis},

\overline{t} =^{def} \{(r, 0, …, 0) : r ∈ Q\}.

\overline{t} is a straight line. If ℓ ∈ Lines, then ang(ℓ), defined below, represents the \underline{angle}^{7} between ℓ and \overline{t}:

ang(ℓ) := \frac{α_{1}^{2}+...+α_{n−1}^{2}}{α_{0}^{2}} if α_{0} ≠ 0, and
ang(ℓ) = ∞ if α_{0} = 0.

ang(ℓ) = 1 means intuitively that the angle between ℓ and \overline{t} is 45^{o}. (See Figure 3.)

Assume that tr_{m}(k) = ℓ is a straight line. Then ang(ℓ) represents the \underline{velocity}^{8} of k as seen by m:

v_{m}(k) := ang(tr_{m}(k)), if tr_{m}(k) ∈ Lines.

E.g. v_{m}(k) = 0 means that tr_{m}(k) is parallel with \overline{t}, i.e. k’s location does not change with time, i.e. k is \underline{at rest} w.r.t. m. The bigger v_{m}(k) is, the bigger distance k travels in a unit time (as seen by m).

v_{m}(h) < 1  t̄  h  b  tr_{m}(b), v_{m}(b) = 1 v_{m}(h′) > 1 h′

Figure 3: Velocities.

3 Basic axioms of special relativity

As already indicated, a plurality of “competing” axiom systems (or “relativity theories”) is an essential feature of a logical analysis of relativity as developed e.g. in [2]. For lack of space here we recall only one of these axiom systems and will call it Specrel. It consists of five axioms. In the following axioms, m, k stand for arbitrary observers, h for an arbitrary body, ℓ for an arbitrary straight line (i.e. element of Lines), and ph for an arbitrary photon. We use the standard custom that free variables should be understood as universally quantified, e.g. the axiom tr_{m}(m) = \overline{t} means (∀m ∈ Obs)tr_{m}(m) = \overline{t}.

Our first axiom says that the traces of observers and photons, as seen by any observer, are straight lines:

7Actually, ang(ℓ) is the square of the tangent of the angle between ℓ and \overline{t}.

8Instead of “velocity”, the precise expression would be “speed”, since v_{m}(k) is a scalar and not a vector.

Ax1 tr_{m}(h) ∈ Lines for h ∈ Obs ∪ P h.

Since translating our intuitive statements to first order formulas will be mechanical, we will not give these translations, we will only give the intuitive forms.

The second axiom says that any observer sees himself at rest in the origin:

Ax2 tr_{m}(m) = \overline{t}.

The third axiom says that we have the tools for thought-experiments: on any apropriate straight line we can assume there is an observer (or reference frame); and the same for photons:^{9}

Ax3 ang(ℓ) < 1 ⇒ (∃k)ℓ = tr_{m}(k), and ang(ℓ) = 1 ⇒ (∃ph ∈ P h)ℓ = tr_{m}(ph).

The fourth axiom says that each observer “sees” the same events (possibly at different space-time locations):^{10}

Ax4 Rng(w_{m}) = Rng(w_{k}).

The last axiom says that the velocity of a photon is 1, for each observer:

AxE v_{m}(ph) = 1 (and tr_{m}(ph) ∈ Lines).

Our choice for a “first possible” axiom system for special relativity is:

Specrel =^{def} {Ax1, Ax2, Ax3, Ax4, AxE}.

When we want to indicate explicitly the number of dimensions, we will write Specrel(n) in place of Specrel.

Let n > 2. In this paper we show that Specrel(n) is consistent, it is not independent, and it forbids faster than light observers but permits faster than light bodies.^{11} We show that Specrel generates an undecidable first-order theory but we can strengthen it so that it becomes decidable (moreover categorical); and also we can strengthen it so that it becomes hereditarily undecidable, further both of Gödel’s incompleteness properties hold for this strengthened version. We will see that both kinds of extension of Specrel are natural.

9This axiom can be “tamed” by using modal logic, such that space-time does not get crowded with k’s and ph’s, cf. [2].

10This will have to be considerably weakened, when preparing for a generalization of the axiom system towards general relativity, cf. [2].

11The point in proving things like Specrel ⊧ no FTL observer is in the small number of axioms and concepts needed. Actually in [2] we show that a much weaker version of Specrel is enough for proving this conclusion. A more refined version of the theorem says that FTL observers “lose most of their meter rods”, cf. [2].

4 Traveling with light, traveling faster than light

As a warm-up, we begin with a simple statement about our axiom system Specrel. When Einstein was a child, he once dreamed that he traveled together with a photon, and then he tried to imagine how the world could look like when one sees it while traveling with a photon. Our first proposition says that in models of Specrel, you can’t see the world while traveling with a photon.

Proposition 1 Specrel ⊧ tr_{m}(k) ≠ tr_{m}(ph) for any m, k ∈ Obs, ph ∈ P h.

Proof. Assume that tr_{m}(k) = tr_{m}(ph) for some m, k ∈ Obs, ph ∈ P h in a model of Specrel. Then tr_{k}(k) = \overline{t} and v_{k}(ph) = 1 by Ax2, AxE. Thus tr_{k}(k) ≠ tr_{k}(ph). Then k sees an event in which k is present but ph is not present (namely such is w_{k}(p) for any p ∈ tr_{k}(k) \ tr_{k}(ph)). However, m does not see such an event by tr_{m}(k) = tr_{m}(ph). This contradicts Ax4, proving the proposition. See Figure 4. QED

m  k k ph  ph tr_{m}(k) = tr_{m}(ph)  tr_{k}(k) ≠ tr_{k}(ph)

Figure 4: An observer cannot travel together with a photon.

Theorem 2 Let n > 2.

(i) Specrel(n) is not independent, namely

{A2, Ax3, Ax4, AxE} ⊧ Ax1.

(ii) Specrel(2) is independent, i.e. for any Ax ∈ Specrel(2) we have

Specrel(2) \ {Ax} |̸= Ax.

Proof. It is not difficult to check that Specrel \ {Ax} |̸= Ax for any Ax ∈ Specrel, if Ax ≠ Ax1. So we have to show that

Specrel(n) \ Ax1 ⊧ Ax1 and Specrel(2) \ Ax1 |̸= Ax1.

Assume that M is a model of Specrel(n) \ Ax1. Let m, k ∈ ObsM and define

f_{mk} := {(p, q) ∈ ^{n}Q ×^{n}Q : w_{m}(p) = w_{k}(q)}.

Thus f_{mk} is a binary relation on space-time; two points of space-time are related when m and k see the same “events” at those points. We now show that

(*) f_{mk} is a bijection in any model of {Ax3, Ax4}.

Let p, q ∈ ^{n}Q be distinct. Then there is a straight line ℓ with ang(ℓ) < 1 separating them, i.e. p ∈ ℓ and q ∉ ℓ. By Ax3, ℓ is the trace of some observer h. Then h ∈ w_{m}(p), h ∉ w_{m}(q), showing that w_{m} is injective for any observer m. By Ax4 we have that both the domain and the range of f_{mk} is ^{n}Q. These facts imply (*).

f_{mk} is called the \underline{world-view transformation} between m and k: its intuitive meaning is that m thinks that k is crazy to the extent that his seeing is distorted by this function f_{mk} (whatever event m sees at space-time location p, k sees it at location f_{mk}(p)).

Now, AxE, Ax3 require that f_{mk} preserve \underline{light-lines} (i.e. lines with angle 1). By a slight generalization of the celebrated Alexandrov-Zeeman theorem (that we will recall in a moment) then f_{mk} has to preserve all straight lines, i.e. it is a \underline{collineation}. Then tr_{k}(m) = f_{mk}(tr_{m}(m)) = f_{mk}(\overline{t}) is a straight line by Ax2. Thus Ax1 holds.

To show Specrel(2) \ Ax1 |̸= Ax1 we construct a bijection f : ^{2}R → ^{2}R, where R is the set of reals, which preserves light-lines, but which takes \overline{t} onto a curve which is not a straight line. Here is the idea of the construction (see Figure 5):

ab  p  p′ f(a) f(b) f āt  t′

Figure 5: f preserves all light-lines but not all straight lines. \overline{t} cannot be defined from light-lines in ^{2}R.

Let t′ be a “slightly bent” version of \overline{t}, and let f be any bijection between \overline{t} and t′. We extend f to any point p not on \overline{t} as follows: Let a and b be the two points where the two light-lines through p intersect \overline{t}, and let f(p) be the intersection point of the two corresponding light-lines going through f(a) and f(b). With some care this extension of f will be a bijection, and it preserves all light lines by its construction. Now it is not difficult to construct a model of Specrel(2) \ Ax1 where this f is one of the world-view transformations; and so in this model Ax1 does not hold.

We now briefly recall the \underline{Alexandrov-Zeeman theorem}. This theorem states that a permutation of ^{4}R which preserves light-lines is a collineation of a special form (namely a Lorentz-transformation up to a dilation, a translation, and a field-automorphism^{12}). An illuminating logical proof can be found in Appendix B of Goldblatt [7]. That proof can be generalized to any Euclidean field Q and n > 2 in place of R and 4. About the Alexandrov-Zeeman theorem see also Rakić [9]. We sketch the proof for n = 3. Let ℓ be any light-line. Let P be the set of those points through which no light-line intersecting ℓ goes through. Then it is not difficult to see that P is just the plane tangent to any light-cone^{13} containing ℓ, see Figure 6.

ℓ  Plane(ℓ, p) = P  ℓ  Plane(ℓ, p) ≠ P

Figure 6: Definition of tangent planes: P is the set of points p through which no light-line intersecting ℓ goes. All straight lines can be defined from light-lines in ^{3}R.

Now we can obtain all straight lines ℓ with ang(ℓ) < 1 by intersecting such tangent planes; then we can define all planes using these newly obtained lines, and then we can obtain all the straight lines by intersecting again these new planes. Hence, any light-line preserving permutation is a collineation. We omit the proof of the rest. QED

Let M be a frame-model, and k be an observer in it. We say that k is a \underline{faster than light} (FTL) observer, if v_{m}(k) > 1 for some observer m. Below, \underline{no FTL observer} abbreviates the sentence (∀m, k ∈ Obs)v_{m}(k) < 1, i.e. that there is no FTL observer in the model.^{14} Theorem 3 Let n > 2.

12This will matter when R will be replaced with Q

13A \underline{light-cone} is the union of all light-lines going through a given point.

14There are well known common sense arguments, going back to Einstein, against FTL (cf. e.g. [9], p.11). These involve “causality” among other undefined concepts. As e.g. Gödel

(i) Specrel(2) |̸= no FTL observer.

(ii) Specrel(n) ⊧ no FTL observer.

Proof. Since we want to stay visual, we give a proof for n = 3. We give a proof that is centered around the notion of Minkowski-orthogonality. Let ℓ, k be two lines. We say that ℓ is \underline{Minkowski-orthogonal} (or shortly, M-orthogonal) to k if ℓ is orthogonal in the usual Euclidean sense to the reflection k′ of k to the xy-plane, see Figure 7.

ℓ  k k′ xy-plane

Figure 7: ℓ is Minkowski-orthogonal to k.

We say that ℓ is Minkowski-orthogonal to the plane P if it is Minkowskiorthogonal to at least two distinct lines lying in P, see Figure 8.

ℓ  P  ℓ P  P ℓ

Figure 8: ℓ is Minkowski-orthogonal to P.

Minkowski-orthogonality is exhaustively investigated, e.g. fully axiomatized, in Goldblatt [7]. We will use here the following corollary of the generalized Alexandrov-Zeeman theorem:

pointed out, these arguments are not proofs in the logical sense. Our present Theorem 3 is of an essentially different character from this point of view (contrast e.g. (i) with (ii)).

(1) If a bijection of ^{n}Q preserves light-lines, then it preserves Minkowskiorthogonality.

We call a plane \underline{space-like} if it contains no light-lines, and we call a line \underline{time-like} if it is Minkowski-orthogonal to a space-like plane. It is not difficult to check (see Figure 9) that

(2) ℓ is time-like iff ang(ℓ) < 1.

Figure 9: Time-like lines and space-like planes.

Clearly \overline{t} is time-like, since it is M-orthogonal to the xy-plane which contains no light-line. Now we have seen in the proof of Theorem 2 that f := f_{km} is a bijective collineation that preserves light-lines. Thus f takes the xy-plane to a space-like plane to which f[\overline{t}] is M-orthogonal by (1), thus f[\overline{t}] is time-like. By (2) then ang(f[\overline{t}]) < 1. But f[\overline{t}] = f_{km}[tr_{k}(k)] = tr_{m}(k), thus v_{m}(k) < 1 in M.

To show Specrel(2) |̸= no FTL observer, we have to give a model of Specrel(2) in which there are FTL-observers. Such models are given in [2], in section 2.4. QED

On pushing the limits of Theorem 3: We note that the generalized Alexandrov-Zeeman theorem is true only in geometries where positive square roots exist in the field. As a contrast, in [2], “no FTL obs” is proved without assuming the existence of positive square roots; and moreover it is proved in axiomsystems where AxE too is substantially weakened; hence a proof different from the above was needed. Also, in the process of finding the “limits” of the “no FTL theorems”, we gave some intuitively appealing axiom systems (such is e.g. Relphax in section 3 of [2]) which do have models with faster-than-light observers.

Now we are going to introduce seven extra natural axioms that will make Specrel categorical over any field. The theory Specrel extended with these seven axioms (and with any decidable theory of fields) is decidable. We will see that if we leave out any one of six of these axioms, then the theory will become undecidable, and such that it can be extended to a hereditarily undecidable theory where both Gödel’s incompleteness theorems hold.

5 A principle of relativity

Our first axiom is a typically relativity theoretic assumption. It says that, up to congruence-transformations^{15} of space we have that the world-view transformations f_{mk} and f_{km} agree, for any two observers m, k. Intuitively this says that “As I see you, so will you see me. If I see that your clocks slow down, then you also will see that my clocks slow down, and they will slow down with the same rate”. AxR below is a possible formalization of Einstein’s Principle or Relativity, which says that the laws of nature are the same for every observer. See also Friedman [6], p.153.

To formalize AxR, first we single out special transformations, that we will call Galilean transformations. A mapping f : ^{n}Q → ^{n}Q is called a \underline{Galilean transformation} if it preserves Euclidean distance and f(1_{t})−f(\overline{0}) = 1_{t} where 1_{t} = ⟨1, 0, 0, …⟩ and 1 denotes the unit element of the field Q. In other words, a Galilean transformation is a congruence transformation which is the identity map on \overline{t}, composed with a translation. See Figure 10.

ȳ  x̄ t̄  g 1_{y}  1_{x} 1_{t}  g(1_{x})  g(1_{y}) g(1_{t})

Figure 10: A Galilean transformation takes the unit vectors into pairwise orthogonal vectors of length 1, and does not change the direction of the timeunit vector.

Our axiom expressing the principle of relativity is the following.

AxR f_{mk} = G ∘ f_{km} ∘ G for some Galilean transformation G.

In more detail, AxR says that (∀m, k)(∃ Galilean transformation G)f_{mk} = G ∘ f_{km} ∘ G.

We note that in models of Specrel, AxR is equivalent to the potential axiom requiring that, in space, in the direction orthogonal (in the Euclidean sense) to the direction of the movement there is no relativistic distortion, i.e. there is no length-contraction. Other equivalent formalizations of AxR can be found in section 3.7 of [2].

15A transformation is called \underline{congruence transformation} if it preserves Euclidean distance.

6 Axioms making Specrel categorical

Here we introduce six more axioms that will make Specrel categorical (over any given field). As in section 3, in the following m, k stand for observers, ℓ for a straight line, ph_{i} for photons; and free variables in the axioms should be understood as universally quantified.

The first two axioms deal with the direction of flow of time. We define for any two observers m, k

m ↑ k iff (f_{km}(1_{t}) − f_{km}(\overline{0}))_{t} > 0.

Intuitively this means that time flows in the same direction for m and k, see Figure 11.

m ↑ k  m ↓ k m  m k  k f_{km}¯0  f_{km}1_{t} f_{km}1_{t}  f_{km}¯0

Figure 11: m ↑ k means that time flows in the same direction for m and k.

Our first axiom is a stronger version of part of Ax3, it says that every appropriate line is the life-line of an observer whose time flows “forward”.

Ax5 ang(ℓ) < 1 ⇒ (∃k ∈ Obs)[ℓ = tr_{m}(k) and m ↑ k].

The next axiom says that time flows in the same direction for any observers at rest in the origin.

Ax↑ tr_{m}(k) = \overline{t} ⇒ m ↑ k.

The next axiom says that every observer can “re-coordinatize” his worldview with a Galilean transformation.

Ax6 G(\overline{0}) ∈ \overline{t} ⇒ (∃k ∈ Obs)f_{mk} = G, for every Galilean transformation G.

The next two axioms say, intuitively, that of each kind of observers and photons we have only one copy (or in other words, according to Leibniz’s principle, if we cannot distinguish two observers or photons with some observable properties, then we treat them as equal). Id denotes the identity mapping.

Ax7 f_{mk} = Id ⇒ m = k.

Ax8 tr_{m}(ph_{1}) = tr_{m}(ph_{2}) ⇒ ph_{1} = ph_{2}.

The last axiom says that every body is an observer or photon.

Ax9 B = Obs ∪ P h.

Compl =^{def} {AxR, Ax5, Ax6, Ax7, Ax8, Ax9}.

We did not include Ax↑ into Compl because, as we will see, its effects are different from those of the the elements of Compl.^{16}

Theorem 4 Let^{17} n > 2 and let (Q, +, ·, ≤) be any Euclidean field.

(i) There are exactly two models of Specrel ∪ Compl with field-reduct (Q, +, ·, ≤), up to isomorphisms.

(ii) There is a unique model of Specrel ∪ Compl ∪ {Ax↑} with field-reduct (Q, +, ·, ≤), up to isomorphisms.

We omit the proof, but in the Appendix we illustrate that in any model of Specrel ∪ {AxR}, all the world-view transformations are so called Poincaretransformations, and this is the most important part of the proof of Theorem 4.

7 Decidability and Gödel incompleteness

We now turn to decidability questions. We start this by recalling the definition of real-closed fields and by recalling some facts from the literature.

An ordered field F is real-closed if it is Euclidean (i.e. every positive element has a square root), and if every polynomial of odd degree has zero as a value. This last requirement can be expressed with the infinite set {ϕ_{2n+1} : n ∈ ω} of first-order formulas, where for every n ∈ ω, ϕ_{n} denotes the following sentence

∀x_{0} … ∀x_{n}∃y[x_{n} ≠ 0 → (x_{0} + x_{1} · y + … + x_{n} · y^{n} = 0)].

By a \underline{theory} we will understand an arbitrary set of first-order formulas (i.e. we will not assume that it is closed under semantical consequence). We call a theory T h \underline{decidable} (or \underline{undecidable} respectively) if the set of all first-order semantical consequences of T h is decidable (or undecidable respectively). We call T h \underline{complete} if it implies either ϕ or ¬ϕ for each first order formula ϕ (of its language).

Fact 5 The theory of real-closed fields is decidable and complete.

16Intuitively, Ax↑ excludes only one model of two choices, while the rest exclude a larger number of possibilities.

17We exclude the case n = 2 for simplicity only.

Fact 6 The theories of ordered fields and Euclidean fields are undecidable. ^{18}

Conjecture 7 Any finitely axiomatizable consistent theory of ordered fields is undecidable.

Corollary 8 Specrel and Specrel ∪ Compl are undecidable.

Proof. This is a corollary of Fact 6, and the theorem that for any Euclidean field F there is a model of Specrel∪Compl with F as the field reduct (Theorem 4).: Let ϕ be any field-theoretic first order formula written by using variables of our quantity sort. Then ϕ is valid in a frame model M with field reduct F iff ϕ is valid in F. Thus ϕ is valid in the class of Euclidean fields iff ϕ is true in all models of Specrel ∪ Compl. Since the first-order theory of the Euclidean fields is undecidable by Fact 6, the first-order consequences of Specrel ∪Compl is undecidable, too. Since this is a finite theory, then any subset of it is undecidable, too. QED

The above suggests that if we want to obtain interesting decision-theoretic results, then we have to concentrate on real-closed fields; or at least include a decidable theory of field-axioms into our theories. Let Φ denote the theory of real-closed fields.

Theorem 9 Let n > 2.

(i) Specrel ∪ Compl ∪ Φ is decidable. (ii) Specrel ∪ Compl ∪ {Ax↑} ∪ Φ is decidable and complete. (iii) Specrel ∪ (Compl \ {Ax}) ∪ {Ax↑} ∪ Φ is undecidable, for any axiom

Ax ∈ Compl.

Proof. (i) and (ii) are corollaries of Theorem 4, we sketch the proof of (ii). Let M and M′ be models of Specrel ∪ Compl ∪ {Ax↑} ∪ Φ. We cannot apply Theorem 4 yet, because the field-reducts F and F′ of M and M′ respectively may not be the same. But they are elementarily equivalent, because Φ is complete, so by the Keisler-Shelah isomorphic ultrapowers theorem they have isomorphic ultrapowers, say F_{1} and F′_{1}. Let M_{1} and M′_{1} be the ultrapowers of M and M′ respectively, taken by the same ultrafilter. Then the field-reducts of these are F_{1} and F′_{1} respectively. Now we can apply Theorem 4 to M_{1} and M′_{1} because F_{1} and F′_{1} are isomorphic, getting that M_{1} and M′_{1} are isomorphic, so elementarily equivalent. But then M and M′ are elementarily equivalent, too, since the former two models are ultrapowers of these. This finishes the proof of (ii). (iii) is a corollary of the next theorem; we included it here because it nicely contrasts (i) and (ii). QED

We now turn to the analogon of Gödel’s first incompleteness theorem.

18Note that if a finitely (or more generally, recursively) axiomatizable theory is undecidable, then it is not complete.

Theorem 10 Let n > 0 and let Ax be any member of Compl. There is a formula ν (in our frame-language) such that

(i) ν is consistent with Specrel ∪ (Compl \ {Ax}) ∪ {Ax↑} ∪ Φ

and for any theory T h consistent with ν

(ii) T h is hereditarily undecidable in the sense that no consistent extension of T h is decidable.

(iii) The conclusion of Gödel’s first incompleteness theorem applies to the theory T h, i.e. no consistent recursively enumerable extension of T h is complete; moreover there is an algorythm that to each consistent, recursively enumerable extension T h′ of T h gives us a formula ϕ such that T h′ |̸= ϕ and T h′ |̸= ¬ϕ.

Proof. The idea of the proof is to show that absence of any member of Compl allows us to interpret Robinson’s Arithmetic into our theory. We sketch this for the case Ax = Ax9. We will see that in this case ν will be quite natural: it will state the existence of a periodically moving body.

Consider the following formulas (with free variables m, b and t):

I(t) = I(m, b, t) = W (m, b, t, \overline{0}), and

ν = I(0) ∧ (∀t, s)

[t < 1 ∧ t ≠ 0] → ¬I(t) ∧
t ≥ 0 → [I(t) ↔ I(t + 1)] ∧
[I(t) ∧ I(s)] → [I(t + s) ∧ I(t · s)]).

Add, for a moment, m and b as constants to our language. Then t remains the only free variable of I which then specifies a subset of the field-reduct in any frame-model: the set of time-points where the observer m sees the body b at the origin. Now the formula ν requires that this subset behaves like the set of integers: it is a discrete periodic subset containing 0, 1 and closed under +, ·. Since the field-reduct of a frame-model is a field, then Robinson’s arithmetic will be true in the field-reduct restricted to the subset defined by I. In other words, I is an \underline{interpretation of Robinson’s Arithmetic in T h ∪ \{ν\}}, whenever ν is consistent with T h. For definition of Robinson’s Arithmetic and (semantical) interpretation see e.g. Monk [8], Def. 14.17, Def. 11.43. Thus, Robinson’s Arithmetic can be interpreted in T h ∪ {ν}. Then T h ∪ {ν} is inseparable (which is a strong version of undecidability) by Thm. 16.1 and Prop. 15.6 in [8]; and thus (ii) and (iii) of our Theorem hold by Monk [8] Thm.s 15.9 and 15.8. Finally, if we omit the constants m, b, then semantical consequence does not change, so (i) and (ii) will hold for the original language (set of formulas not containing the constants m or b), too.

To show (i), we have to construct a model of Specrel ∪ (Compl \ {Ax9}) ∪ {Ax↑} ∪ Φ ∪ {ν}. This is not difficult as ν basically states the existence of a periodically moving body; see Figure 12.

m b

Figure 12: b is a periodically moving body in m’s world-view.

Take a “standard” model with minimum set of observers and photons; and add one periodically moving body. We omit the details of the definition of this model.

The proofs for the other cases are analogous; we only give different interpretations of Robinson’s arithmetic. This means that we give a different formula I, but ν will be the same (speaking about I), and then we only have to show that T h ∪ {ν} is consistent, where T h is the theory in (i). To give a flavor, we give this new interpration I for the case when Ax = Ax5.

I(m, t) =^{def} (∀ℓ)[ang(ℓ) = \frac{1}{t} ⇒ (∃k)(tr_{m}(k) = ℓ ∧ m ↑ k)] or t = 0, 1].

This finishes the proofidea of Theorem 10. QED

A theorem analogous to Theorem 10 but concerning Gödel’s second incompleteness theorem can also be stated and proved with analogous methods. For details see [1].

8 Appendix

Here we show that in any model of Specrel ∪ {AxR}, all the world-view transformations are so called Poincare transformations (we will introduce Poincare transformations while doing this).

First we explain the role of the Galilean transformation G in AxR, we explain why we did not just require f_{mk} = f_{km}. We illustrate this for n = 2. Assume that m, k are observers and m “sees” k as on Figure 13. Then f_{km} takes \overline{t} to tr_{m}(k), by Ax2, see Figure 14. We have seen in section 4 that in models of Specrel, f_{km} preserves Minkowski-orthogonality, thus f_{km} takes \overline{x} to the line M-orthogonal to tr_{m}(k). Thus f_{km} is either as on Figure 14, or as on Figure 15. We do not want to exclude the possibility on Figure 14, so let us assume that f_{km} is as on Figure 14. Then f_{mk} is also as on Figure 14, since f_{mk} = f_{km}^{−1}, and f_{mk} ≠ f_{km} because the two maps take the time axis \overline{t} to different places (see Figure 14). Let σ : ^{2}Q → ^{2}Q be the reflection w.r.t. the time axis \overline{t} (i.e. σ(t, s) = (t, −s) for any t, s ∈ Q). Then σ is a Galilean transformation. If we take G to be this reflection, then f =^{def} f_{mk} and g =^{def} σ ∘ f_{km} ∘ σ take the time axis to the same set, and similarly they take the other axis \overline{x} to the same set; this is illustrated on Figure 16.

world-view of m  world-view of k t̄ m  k  x̄  t̄  x̄ k m

Figure 13: The world-views of m and k.

f_{mk}  f_{km} = f_{mk}^{−1} t̄  x̄f_{mk}[x̄]  t̄  x̄

Figure 14: The world-view transformations between m and k can be this.

We note that if f_{km} is as on Figure 15, then we do not need σ, already f_{km} and f_{mk} take \overline{t}, \overline{x} to the same sets respectively (i.e. f[\overline{t}] = g[\overline{t}] and f[\overline{x}] = g[\overline{x}]).^{19} Intuitively, this case corresponds to m and k “looking toward each other”, while the other case corresponds to the more commonly assumed situation that m and k “look in the same direction”.

But in addition to this, we need that f and g (as above) agree on \overline{t} and \overline{x}, not just that they take these lines to the same sets. We will see that to achieve this, f_{km} has to take 1_{t}(= ⟨1, 0, 0, …⟩) to a unique point on tr_{m}(k), see Figures 17, 18. So, let us look at f_{km} and let us see where e =^{def} f_{km}(1_{t}) is on tr_{m}(k). Let a, b and a′ be as on Figure 18; i.e. they are the points on tr_{m}(k) and on \overline{t} such that the straight line connecting 1_{t} and a is parallel with \overline{x}, and the straight lines connecting 1_{t} and b and connecting a and a′ are parallel with f_{km}[\overline{x}]. See Figure 18. If e = a, then m sees that k’s clock shows 1 just when his clock shows 1, because 1_{t} and a are simultaneous for m. But k will see that

19Here f[\overline{t}] = \{f(p) : p ∈ \overline{t}\}.

f_{mk}[x̄]  t̄ f_{mk}  x̄  t̄ f_{km} = f_{mk}^{−1}  x̄

Figure 15: The other possibility for world-view transformations between m and k.

t̄= σt̄ f_{km}t̄ σf_{km}t̄  x̄ σx̄ f_{km}σx̄  σf_{km}σx̄

Figure 16: f_{mk} and σ ∘ f_{km} ∘ σ, where σ is reflection w.r.t. t̄, take \overline{t} and \overline{x} to the same sets. m’s clock shows a′ < 1 when his clock shows 1, because for k, e = a and a′ are simultaneous. So k will think that m’s clocks are slow, but m will think that k’s clocks are right. See Figure 17. Analogously, m thinks that k’s clocks are right (slow or fast, respectively) iff e = b (> b or < b respectively). And, k thinks that m’s clocks are right (slow or fast, respectively) iff e = a (< a or > a respectively). Thus both think that the other’s clocks are slow iff b < e < a. The rate of “slowness” is the same for them at a unique point in between a and b, because the change of rate is a continuous and strictly monotonic function (of the “number” |e − \overline{0}|). Now, \underline{Minkowski-distance} is defined so that the Minkowski-distance is 1 between \overline{0} and this unique point (where the rates of slowing down are the same for m and k). Figure 19 shows the points whose Minkowski-distance from \overline{0} is 1, i.e. it shows Minkowski-circle with radius 1 and center \overline{0}.

m  k 1_{t}  e  direction of simultaneities for k direction of simultaneities for m this point is simultaneous for k with e this point is simultaneous for m with e

Figure 17: m thinks that k’s clocks are right, and k thinks that m clocks are slow. (e = f_{km}1_{t})

Summing up: In models of Specrel + AxR, the world-view transformations take the unit vectors into pairwise Minkowski-orthogonal vectors of Minkowskilength 1. These are called in the literature \underline{Poincare-transformations}; these are \underline{Lorentz-transformations} composed with translations. Or, equivalently, the world-view transformations are Minkowski-distance-preserving and light-line preserving.

References

[1] Andréka, H. Madarász, J. X. and Németi, I. Decidability, undecidability, and Gödel incompleteness in relativity theories. Manuscript, Budapest, 1999.

m  k 1_{t} a′  a b  e = f_{km}(1_{t}) direction of simultaneities for k direction of simultaneities for m

Figure 18: Both m and k think that the other’s clocks slow down iff f_{mk}(1_{t}) is in between a and b. The rates of slowing down will be equal at a unique point.

Figure 19: Minkowski-distance 1.

[2] Andréka, H. Madarász, J. Németi, I. Sain, I. and Sági, G. Analyzing the logical structure of relativity theory via model theoretic logic. Lecture Notes for A’dam course (spring 1998). http://www.mathinst.hu/pub/algebraic-logic.

[3] van Benthem, J. The logic of time. Reidel, Dordrecht, 1983.

[4] van Benthem, J. Semantics of time. In: Time, Mind, and Behaviour (eds: Michon, J.A. and Jackson, J.L.), Springer-Verlag Berlin 1985. pp.266-278.

[5] van Benthem, J. Content versus wrapping: an essay in semantic complexity. In: Arrow Logic and Multimodal Logic (eds: Marx, M. Pólos, L. and Masuch, M.) CSLI Publications, Stanford, 1996. pp.203-219.

[6] Friedman, M. Foundations of space-time theories. Relativistic physics and philosophy of science. Princeton University Press, 1983.

[7] Goldblatt, R. Orthogonality and space-time geometry. (With 126 illustrations.) Springer-Verlag, 1987.

[8] Monk, J. D. Mathematical Logic. Springer-Verlag, Berlin, 1976.

[9] Rakić, N. Common sense time and special relativity. Dissertation, University of Amsterdam, 1997. ILLC Dissertation series 97-02.

[10] Rindler, W. Essential relativity. Special, general and cosmological. Springer-Verlag, Berlin, 1969, 1977.

[11] Sain, I. There are general rules for specifying semantics: observations on abstract model theory. CL&CL13 (1990), 195-250.

[12] Szabó, L. E. The problem of open future, determinism in the light of relativity and quantum theory. Manuscript, Dept. of Theoretical Physics, Eötvös Loránd University, Budapest 1999.