Axiomatizing relativistic dynamics using formal thought experiments

Thought experiments are widely used in informal explanations of Relativity Theories; however, they are not present explicitly in formalized versions of Relativity Theory. In this paper, we present an axiom system of Special Relativity which is able to express thought experiments formally and explicitly. Moreover, using these thought experiments, we can provide an explicit definition of relativistic mass based merely on kinematical concepts and thought experiments on collisions. Using this definition, we can geometrically prove the Mass Increase Formula \(m_0 = m \mathrel {\cdot }\sqrt{1-v^2}\) in a natural way, without postulates of conservation of mass and momentum.

1. Another good example is that faster than light motion of particles per se is logically independent from both relativistic kinematics (Székely 2013) and relativistic dynamics (Madarász and Székely 2014). For an axiomatic approach defining coordinate systems moving faster than light, see Hoffman (2013).

2. The statement “no inertial observer can go faster than light” follows from the basic assumptions we use in this proof, so we can use it. For a precise proof, see Andréka et al. (2012).

3. This basic statement can be proved using the very same assumptions as we use in this proof.

4. Later we will introduce a modal version of this assumption, see AxMEv.

5. Note that the starting idea, that thought experiments should be understood as tests for logical consistency, is fulfilled. The truth of \(\Diamond \varphi \) involves also classical logical consistency with the classical axioms. If \(\Diamond \varphi \) is true, then there is a (transformed) classical model in which \(\varphi \) is true. Since the classical axioms must be true in each world of the modal model, they are also true in the transformed model. This means that \(\varphi \) is consistent.

6. The modal operator \(\Diamond \) is designed to handle a restricted quantification over possible worlds in the metalanguage. Even though all the notions, such as interpretations and models are already present in classical semantics, using modal logic is not superfluous because the purpose of modalities is not only to quantify over models, but to do this from the object language. This fact makes it possible to axiomatize thought experiments or model transformations, which is a central goal of this paper.

7. Maybe it would be more accurate at the introduction of modal axioms to include the precise metalinguistic characterization of the expressed model transformations, but we will set aside from this. Besides of its technical nature, it does not affect the success of axiomatization of special relativistic dynamics.

8. However, this assumption can be evaded by replacing \(\Box \varphi \) and \(\Diamond \varphi \) with \(\varphi \wedge \Box \varphi \) and \(\varphi \vee \Diamond \varphi \) in all our axioms.

9. For the standard line of thought, see (Blackburn et al. (2002), Definition 3.3, Example 3.6).

10. Corsi (2002) proved strong completeness for only one-sorted modal languages, but our language can be interpreted into it in the usual way, i.e., we introduce a \(D\) and a \(Q\) predicate to distinguish the sorts. To construct one-sorted models for our system, we only have to stipulate that the mathematical parts of the \(R\)-connected worlds are the same, i.e., they are invariant under \(R\).

    (Goldblatt (2011), 5.6) is also a recent source of a strong completeness theorem, which is too general for our present purpose (it is designed to incorporate even nonrigid designator terms); however, using that approach would probably be more elegant especially for readers preferring algebraic approaches.

11. For the axioms of ordered fields, see e.g., (Chang and Keisler (1990), p. 41).

12. That is, \((\forall x>0)(\exists y)x=y^2\).

13. Note that the expression on the right side of the equivalence comes from the metalanguage. We can, however, pull this definition back the object language in the following way: \( b\in {\mathrm {ev}}_{k}({\bar{x}}) \mathop {\iff }\limits ^{{ def. }}{\mathrm {W}}({k},{b},{\bar{x}})\).

14. This assumption is axiom AxEv (the axiom of events) in the classical approach, see e.g., (Andréka et al. (2012), p. 638). Here we will use its modal version, see \({\mathsf{AxMEv}}\).

15. The possible events are accessible in the metalanguage in a straightforward way: they are sets of possible bodies, i.e., sets of elements of \(U\), occurring at a coordinate point of some observer. In the classical approach of \(\mathsf{SpecRel}\), we use this definition, see (Andréka et al. (2012), p. 637). However, in the modal approach, we do not have access to \(U\), only to a \(D_w\) since we can quantify over only the elements of \(D_w\), i.e., over actual bodies.

16. We do not assume that the mass-standard is inertial in general. However, in thought experiments which we use to derive our theorems, the mass-standard will always be inertial. This will follow from axiom \({\mathsf{AxDir}}\), see Axiom 9.

17. These relations can also be defined in the object language using the method of footnote 13 together with \({\mathrm {in}}_k(\bar{x})=\{b,c\} \iff a\in {\mathrm {in}}_k(\bar{x}) \leftrightarrow (a=b \vee a=c)\) and with a similar substitution for \({\mathrm {out}}_{k}(\bar{x})\).

18. Practically, the ratio of collision is a formal implementation of Weyl’s definition for ratios of masses, see (Jammer (2000), (1.4) on p. 10), implemented to special relativity. Suppose that we already have a mass function \(m\) having the usual properties. So \(m_k(b)\) denotes the relativistic mass of \(b\) according to \(k\). Let \(b\) and \(c\) be two colliding bodies, and \(k\) be the inertial observer according to which the center of mass of \(b\) and \(c\) is stationary. Then \(({b}\mathop {:}{c})_{k}\) is the ratio \({\mathrm {v}}_{k}(c)/{\mathrm {v}}_{k}(b)\). Therefore, the collision ratio \(({b}\mathop {:}{c})_{k}\) corresponds to the ratio \(m_k(b)/m_k(c)\) by the conservation of linear momentum. And since Poincaré transformations preserve the ratio of points on a line, the ratio of collision means the ratio of masses even if we choose a different observer than \(k\).

19. The reader may wonder why is the formula of \({\mathsf{AxCollRel}}\) so complicated, while the informal description is so simple, what is more, why do we postulate that every collision thought experiment is relevant instead of only those that we really need? The reason is that the expressive power of first-order modal logic is not as strong as it seems. For example, it is hopeless to show a formula expressing exactly the following: “There is an alternative world \(w'\) in which every object from \(w\) having property \(P_w\), has a property \(Q_{w'}\) in \(w'\).” The main reason for this is that we cannot ‘quantify back’ into the previous world after we used a \(\Diamond \) operator. For a summary of expressivity problems of first-order modal logic, see Hazen (1976), Hodes (1984). Now the dynamical statement like “Only \(b\)’s worldline changes” is also such a statement. So this control is beyond the expressibility power of first-order modal logic. At the conference LR12 (Molnár 2012) and in Molnár (2013), we sketched a solution which used a trick to enforce this kind of thought experiments, but it cost a lot: it used two modal operators such that one of them was a transitive closure of the other. A strong completeness theorem for such a logic is impossible, see (Blackburn et al. (2002), Sect. 4.8 Finitary Methods I). So \({\mathsf{AxCollRel}}\) seems to be the appropriate axiom which makes relevant collision thought experiments possible, and is still expressible.

20. Note that the definitions (3), (4) and (5) express their intended meanings only if we assume AxCollRel as well.

21. It is a question for further research to find natural and more elementary axioms implying that the results of indirect measurements do not depend on the choices of transmitting body.

22. Proving that this key axiom does not follow even from our axiom system MSpecRelDyn (see Sect. 4.2) is out of the scope of this paper, since it involves an even more complicated model construction than what is outlined in Sect. 6.3 of Appendix. Nevertheless, the key idea is that if we have three worlds \(w\), \(w_1\) and \(w_2\) such that \(wRw_1\) and \(wRw_2\), then our only axioms that are capable of harmonizing the collisions in \(w_1\) and \(w_2\) are \({\mathsf{AxDir}}\), \({\mathsf{AxIndir}}\) and \({\mathsf{AxPDirComp}}\) (for the latter see the next section). However, if none of the colliding bodies are co-moving with an observer (to use \({\mathsf{AxIndir}}\) and \({\mathsf{AxPDirComp}}\)) or identical with the mass-standard (to use \({\mathsf{AxDir}}\)), then our axioms say nothing about the collisions in \(w_1\) and \(w_2\). This fact can be used to construct an appropriate model because \({\mathsf{AxCenter}}\) claims that if we have a collision in \(w\), then the measurements in \(w_1\) and \(w_2\) are determined by \(w\).

23. We take infinite number of observers only to simplify the construction. It is also possible to construct a model where there are only finitely many observers in every world.

24. Again, at the cost of simplicity, it is possible to construct a model where there are only finitely many photons in every world.

25. The key idea here is that we can adjust the worldlines in all worlds in a way that all collisions of the model became symmetric. This causes that all body became an mass-standard-equivalent in the model, even the results of the collision of mass-standard-equivalents, which is a violation of the law of the conservation of mass.

26. For the key idea, see footnote 22.

27. We suspect that the underlying directed graph drawn by the alternative relation of a model capable of showing the independence of \({\mathsf{AxEqSym}}\) must be very close to a tree.

We are grateful to Hajnal Andréka, István Németi and Lászlo E. Szabó for the inspiring discussions on the subject. This research is supported by the Hungarian Scientific Research Fund for basic research Grants Nos. T81188 and PD84093.

Authors and Affiliations

1. Institute of Philosophy, Eötvös Loránd University, Múzeum krt. 4/i, 1088, Budapest, Hungary

   Attila Molnár

2. Alfréd Rényi Institute of Mathematics, Hungarian Academy of Sciences, Reáltanoda utca 13-15, 1053, Budapest, Hungary

   Gergely Székely

Corresponding author

Correspondence to Attila Molnár.

Appendix

1.1 Poincaré Transformation Theorem

Here we are going to prove Theorem 1 sating that:

To prove that \({\mathrm {w}}_{{k}{h}}\) is a Poincaré transformation, it is enough to show that it takes lines of slope 1 to lines of slope 1, since there is an Alexandrov–Zeeman type theorem which works only with these premises, see Madarász and Székely (2013). To prove this lemma, let us introduce the following notation for the speed corresponding to coordinate points \(\bar{x}\) and \(\bar{y}\):

Lemma 1

(Light-line) Assume MSpecRel. Then every worldview transformation is a bijection taking lines of slope 1 to lines of slope 1.

Proof

Worldview transformations are bijections by Proposition 2.

Now we prove that worldview transformations take lines of slope 1 to lines of slope 1. By AxEField, \({\mathrm {v}}(\bar{x} ,\bar{y})={\mathrm {v}}(\bar{y} ,\bar{z})={\mathrm {v}}(\bar{z} ,\bar{x})=1\) implies that \(\bar{x}\), \(\bar{y}\) and \(\bar{z}\) are collinear. Therefore, to finish our proof, it is enough to derive the following formula:

Let \(k\) and \(h\) be arbitrary observers in a world \(w\), and let \(\bar{x}\) and \(\bar{y}\) be coordinate points such that \({\mathrm {v}}(\bar{x} ,\bar{y})=1\). By \({{\mathsf{AxPhExp}}}\), in every \(w\) world, there is an accessible world \(w'\) such that \(wRw'\) and in \(w'\) there is a light signal \(p\in {\mathrm {ev}}_{k}({\bar{x}})\cap {\mathrm {ev}}_{k}({\bar{y}})\) in \(w'\). By \({\mathsf{AxMFrame}}\), \(k\) still exists as an observer in \(w'\). So \(p\in {\mathrm {ev}}_{k}({{\mathrm {w}}_{{k}{h}}({\bar{x}})}) \cap {\mathrm {ev}}_{k}({{\mathrm {w}}_{{k}{h}}({\bar{y}})})\) by \({\mathsf{AxMEv}}\). Consequently, by \({\mathsf{AxPhObs}}\):

and this is what we wanted to prove.\(\square \)

1.2 Proof of Symmetric Collision Theorem

Here we are going to prove Theorem 2 stating that:

The symmetric collision theorem

Full size image

Proof

Let \(k\) and \(h\) be observers and let \(b\) and \(c\) be ordinary bodies in a world \(w\) such that \({\mathrm {v}}_{k}(b)=0\), \({\mathrm {v}}_{h}(c)=0\) and \({\mathrm {SymColl}}({b},{c})\) holds for them. Since \({\mathrm {SymColl}}({b},{c})\) holds, there is an observer \(m\) (the so-called median observer) in \(w\) such that \(\bar{{\mathrm {v}}}_{m}(b) + \bar{{\mathrm {v}}}_{m}(c)=\bar{0}\) and \(({b}\mathop {:}{c})_{m} = 1\). See Fig. 10.

The time dilation effect, i.e.,

is a consequence of Theorem 1, see (Andréka et al. (2007), Theorem 2.4, (2)):

We know from (15) that if the clocks of \(k\) and \(h\) show \(0\) at \(A\), and the clock of \(h\) shows \(-1\) at \(C\), then the clock of \(k\) shows \(-\sqrt{1-v^2}\) where \(v\) is \(\mathrm {v}_h(k)\).

We are interested in \(({c}\mathop {:}{b})_{h}\), which is now:

Since worldview transformation are affine transformations, this ratio is the same in the worldview of the median observer \(m\), i.e.,

Since the worldline of \(d\) is an angle bisector of the triangle \(A'B'C'\) in the worldview of \(m\), by the angle bisector theorem,

Since the clocks of \(k\) and \(h\) slow down with the same rate for the median observer \(m\), we know that

Since the collision was symmetric, \(({b}\mathop {:}{c})_{k} = ({c}\mathop {:}{b})_{h} \). Therefore, from (16), (17), (18) and (19) we have

and this is what we wanted to prove. \(\square \)

1.3 Consistency and independence

To prove the consistency of \({\mathsf{MSpecRelDyn}}\), it is enough to construct a model for it. It is easy to construct a model of \({\mathsf{MSpecRelDyn}}\)—if we choose \({\mathrm {IOb}}^\mathfrak M\) and \({\mathrm {W}}^\mathfrak M\) to be empty, then almost all axioms will be satisfied, since all of them has the form “\((\forall k \in {\mathrm {IOb}})\dots \)”. The only exception is \({\mathsf{AxMFrame}}\), since this requires the reflexivity of the alternative relation, the rigidity of mathematics, etc., but it is easy to satisfy these statements by choosing the set of possible worlds to be a singleton \(\{w\}\) such that \(wRw\).

However, we would not only like to prove that that \({\mathsf{MSpecRelDyn}}\) is consistent but also that it has some complex models, models where there are several observers moving relative to one another and measuring ordinary inertial bodies, e.g., where we see something similar to what we had in mind during the proofs of Sect. 4. This type of model construction is too complex to be included in detail in this paper. However, in this section, we give a sketch of such a construction.

The main difficulty in the construction of such a model is the following: If two ordinary bodies, say \(b\) and \(c\) collide, then every observer has to measure the two bodies and the resulting body \(b {\small \oplus } c\) directly, pseudo-directly or indirectly. There are plenty of other measurements we have to include because, for example, in the successor world, where the pseudo-direct measurement of \(b\) is done by \({\mathrm {e}}_{k}\), there will be an ordinary body \(b\oplus {\mathrm {e}}_{k}\), which again, has to be measured directly, pseudo-directly, indirectly, and so on and so forth. So building any model \(\mathfrak M\) in which \({\mathsf{MSpecRelDyn}}\) is true (i.e., true in every world of \(\mathfrak M\)), and in which \(\exists {\mathsf{2IOb}}\) and \((\exists b ) {\mathrm {OIB}}(b)\) is satisfied (i.e., true in some world of \(\mathfrak M\)) involves an infinite process of measuring.

Another difficulty is that by \(\exists {\mathsf{2IOb}}\) two observers sooner or later will compare their equivalents by \({\mathsf{AxPDirComp}}\), which postulates the existence of a median-observer as well. So the cardinality of observers cannot be 2 or any finite number.

From now on, to describe a complex model \(\mathfrak M\), we take the perspective of an observer \(M\). To guarantee the truth of \(\exists {\mathsf{2IOb}}\) and the existence of medians (needed for \({\mathsf{AxPDirComp}}\)), we include infinitely many^{Footnote 23} observers to meet with \(M\) in its origin in all worlds (where \(M\) exists) such that for every possible velocity in the interval \([-0.5,0.5]\), there will be an observer in the \(tx\)-plane having that velocity. There will be a set of possible worlds, \(S_0\), where these observers compare their mass-standard-equivalents and measure the other’s equivalent directly in the origin at time \(0\) according to \(M\). Every such comparison and direct measurement will result a body, which again has to be measured; these measurements will happen 1 second later according to \(M\), and these worlds will constitute the set \(S_1^{\oplus }\). Note that mass-standard-equivalents of \(S_1^{\oplus }\) have different worldlines than they had in \(S_0\) since their worldlines end at the time \(1\) instead of \(0\). So there will be a set \(S_1^{et}\) very similar to \(S_0\), where the observers compare their mass-standard-equivalents 1 second later. The construction continues in the same way with \(S_2^{\oplus }\), \(S_2^{et}\), \(S_3^{\oplus }\), \(S_3^{et}\) ...   into infinity. A part of that model, measurements concerning two equivalents \(a\) and \(b\) of observers \(A\), \(B\) having opposite velocity according \(M\), is illustrated on Fig. 11. This figure shows also how are the indirect measurements fulfilled in that model: \(a\oplus b\) is measured in the central world of the figure indirectly through worlds having the resulting body \(a\oplus a\oplus b\) and \(a\oplus e\) (the latter is from \(S_1^{et}\)).

A part of the model: measurements concerning two equivalents \(a\) and \(b\) of observers \(A\), \(B\) having opposite velocity according to \(M\)

Full size image

This construction will satisfy all the axioms of \({\mathsf{MSpecRelDyn}}\) except the light signal-sending axiom \({\mathsf{AxPhExp}}\). To make this axiom true in every world of our model, it is enough to extend this construction with only one world, say \(ph\), which is an alternative of every world of the model, and which realizes every possible photon needed by any world.^{Footnote 24} This means that \(ph\) will be a classical model of SpecRel. For such a construction, see (Andréka et al. (2007), Corollary 11.12, especially pp. 643–644).

This construction can be carried out even in a way such that the conservation of mass and linear moment fails in the resulting model. This construction shows that the Mass Increase Theorem can be proved without the usual conservation postulates, which is a result similar to that of Andréka et al. (2008).^{Footnote 25} However, \({\mathsf{MSpecRelDyn}}\) has models (different from the above construction) where even the key axiom of Andréka et al. (2008), \(\mathsf{AxCenter}\), the conservation of centerline of mass, is refutable.^{Footnote 26}

Independence This model \(\mathfrak M\) can easily be modified to show the independence of several axioms of \({\mathsf{MSpecRelDyn}}\). For example, if we remove a pair of worlds \(\langle w,w'\rangle \) from the alternative relation where \(w'\) is a world where the mass-standard exists, then we can falsify \({\mathsf{AxDir}}\) while the other axioms remain true, i.e., \({\mathsf{AxDir}}\) is independent from the rest axioms of \({\mathsf{MSpecRelDyn}}\). If we do the same with a \(w'\) where instead of the mass-standard, one of its equivalents exists, we have the independence of \({\mathsf{AxPDirComp}}\). To show that \({\mathsf{AxCollRel}}\) is independent, it is enough to copy an arbitrary world of \(\mathfrak M\) which sees the same alternatives, but which is seen by no one. If, in this copied world, we alter the speed of one body, we can violate \({\mathsf{AxCollRel}}\) while the other axioms remain true.

The independence of \({\mathsf{AxIndir}}\) from the rest of the axioms of \({\mathsf{MSpecRelDyn}}\) can be showed by a one-world model where there is only one observer and only one resting ordinary inertial body resting to that observer. However, in the light of our motivation of \(\mathfrak M\), it is worth to examine the independence of \({\mathsf{AxIndir}}\) in the axiom system \({\mathsf{MSpecRelDyn}}\cup \{\exists {\mathsf{2IOb}}\}\) as well. The existence of indirect measurements is a consequence of \({\mathsf{MSpecRelDyn}}\cup \{\exists {\mathsf{2IOb}}\}\), the idea is used in the proof of the Mass Increase Theorem (Thm. 3). However, the independence of the uniqueness of the results of indirect measurements is a question for further research. Our conjecture is that it is independent.

It is also a question for further research whether the last axiom of MSpecRelDyn, \({\mathsf{AxEqSym}}\) is independent from the rest of \({\mathsf{MSpecRelDyn}}\) or not; our conjecture is that it is. However, a model which would be capable of showing this must be entirely different from the above outlined \(\mathfrak M\).^{Footnote 27}

Reprints and permissions