Abstract: In this paper we try to give a small sample illustrating the approach of Andreka et al. [1] (see also Parts I-VII here) to a logical analysis of relativity theory conducted purely in first order logic (for methodological reasons). Here we concentrate on special relativity, but e.g. in [1] and in [2] steps are made in the direction of generalizing the approach towards general relativity. In [1] 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 book on Foundations of Space-Time Theories and in Rindler's relativity book, or compare the Reichenbach-Grunbaum approach to relativity with the standard one.
It is explained in [1] that 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 contains ``its own interpretation'', too. (ii) It is not clear to us how the conceptual analysis (which axiom is responsible for what, which axiom is intuitively more natural than the other, etc.) (or the Reichenbach-Grunbaum issues) could be squeezed into Minkowskian geometry. (iii) Our formalized relativity theory is undecidable, while the first order version of Minkowskian geometry in Goldblatt's 1987 Springer book 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 Friedman's book 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, 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 Godel's incompleteness theorems, independence issues, etc).
The idea of gradually generalizing our logical foundation for special relativity towards general relativity is also discussed in the paper.