This article provides a synthetic (and second-order) axiom system, which I call \(\mathsf{Gal}(1,3)\), which describes Galilean spacetime and does so categorically.¹ Galilean spacetime is a system \(\mathbb{P}\) of points on which three physical geometrical primitives are defined, satisfying certain conditions.² Galilean spacetime can be thought of as the background geometry of the system of spacetime events for Newtonian classical mechanics:

I shall call the carrier set of Galilean spacetime \(\mathbb{P}\): this is the domain of “spacetime points” or “events.” Going ahead of ourselves a bit, there are three distinguished physical relations on \(\mathbb{P}\). A three-place betweenness relation \(B\), which gives the whole system an affine “straight-line” structure;³ a binary simultaneity relation \(\sim\), which induces a partition of \(\mathbb{P}\) into a system of non-intersecting simultaneity hypersurfaces, \(\Sigma_{0},\Sigma_{1},\dots\), arranged as a “foliation”; and a special four-place congruence relation: this is the four-place sim-congruence relation, \(\equiv^{\sim}\), which induces three-dimensional Euclidean geometry on each hypersurface.⁴

An especially important subset of straight lines are “time axes”: a time axis is a straight line in the affine geometry that does not lie within a simultaneity hypersurface. Physically, a time axis is the trajectory of a material point acted on by no forces—this is Newton’s First Law or the Law of Inertia.⁵

We can bundle the carrier set of Galilean spacetime and the aforementioned three distinguished physical relations on Galilean spacetime together: \((\mathbb{P},B,\sim,\equiv^{\sim})\). Our aim in this paper is to give a synthetic axiomatization of this structure \((\mathbb{P},B,\sim,\equiv^{\sim})\).⁶ This means that, in contrast with analytic geometry, the axioms do not quantify over the reals, introduce a metric function (like a Riemannian metric \(g_{ab}\)), or talk about coordinate systems. Instead, the axioms use a number of basic physical predicates on spacetime. And then the existence of special mappings \(\Phi:\mathbb{P}\to\mathbb{R}^{4}\)—that is, coordinate systems—becomes a theorem, not an assumption.

Hartry Field (1980) has carefully studied this approach in order to try and vindicate nominalism: this is the claim that there are no mathematical objects at all, and insofar as numbers, functions, sets, vector spaces, Lie groups, and so on are used in physics and science more generally, they can be dispensed with. It is the claim that physical theories can, in principle, be replaced with theories that are “nominalistic” and that the normal use of mathematics is “useful but false.” It is to Field’s enormous credit to have pinned down the two essential uses. These are:

As regards the second, in mathematical logic, this is called “speed-up,” and it was discovered by Kurt Gödel (1935) as a spin-off from his incompleteness results. Perhaps the most remarkable example of this phenomenon was given in Boolos (1987), a first-order valid inference with a short mathematical proof (it uses second-order comprehension), but whose shortest purely logical derivation, using the rules for the connectives and quantifiers, has vastly more symbols than the number of baryons in the observable universe.⁷

The best survey, and overall evaluation, of a large variety of nominalist approaches for both mathematics and science is Burgess and Rosen (1997).⁸ I’m not recommending this as an approach to studying the geometrical assumptions of physical theories, as my own view here is the usual mathematical realist view (“useful because true”). Indeed, Riemannian geometry is here to stay! Riemannian geometry provides incredible flexibility by assuming the existence of a metric tensor \(g_{ab}\) on spacetime.⁹ However, for the two special cases of Galilean spacetime and Minkowski spacetime, the synthetic approach helps provide a nice example of how the physics (i.e., the basic physical relations: betweenness, congruence, and so on) and mathematics (i.e., real numbers, coordinate systems, vector spaces, and so on) get “entangled.”

The basic machinery for the introduction of coordinates is the Representation Theorem. Given a synthetic structure satisfying a series of conditions, one proves the existence of an isomorphism to a standard coordinate structure:¹⁰ \[\Phi:\text{synthetic structure}\to\text{coordinate structure}. \qquad{(1)}\] That is, the isomorphism \(\Phi\) takes each point \(p\) in the synthetic structure to its coordinates \(\Phi^i(p)\) (usually in \(\mathbb{R}^{n}\)) in such a way that a distinguished synthetic relation \(R\) holds for \(p,q,\dots\) iff a separately defined coordinate relation \(R'\) holds for \(\Phi(p),\Phi(q),\dots\) (see, for example, (5) below). Because the synthetic and coordinate structures are isomorphic, the latter is a kind of map or representation of the former: they share the same abstract structure.¹¹

However, historically, the analysis of Galilean spacetime did not proceed like this. Modern analysis of Galilean spacetime (sometimes called “neo-Newtonian” spacetime or just “Newtonian spacetime”) was developed using the differential geometry methods developed to study General Relativity: what are now called “relativistic spacetimes.” This began in the 60s and 70s, with work by Trautman, Penrose, Stein, Ehlers, Earman, and others (based on earlier work, such as Cartan’s).¹² In Malament (2012, chap. 4), David Malament provides details of the differential geometry formulation of this topic. Galilean (or Newtonian) spacetime is defined as a structure of the form \[\mathcal{A}=(M,\nabla,h^{ab},t_{ab}), \qquad{(2)}\] where \(M\) is a manifold diffeomorphic to \(\mathbb{R}^{4}\), \(\nabla\) is a flat (torsion-free) affine connection on \(M\), and \(h^{ab},t_{ab}\) are tensor fields on \(M\) satisfying compatibility conditions, from which one can construct temporal and spatial metrics and simultaneity surfaces.¹³

The approach we develop here is entirely synthetic. The underlying geometric relations are betweenness (written \(\texttt{Bet}(p,q,r)\)), simultaneity (written \(p\sim q\)), and sim-congruence (written \(pq\equiv^{\sim}rs\)): these are relations on points. Inertial coordinate systems are then proved to exist by a Representation Theorem. An inertial coordinate system \(\Phi\) is nothing more than an isomorphism from the synthetic geometrical structure \((\mathbb{P},B,\sim,\equiv^{\sim})\) of Galilean spacetime (with carrier set \(\mathbb{P}\)) to a suitable “coordinate structure” built on the carrier set \(\mathbb{R}^{4}\). Below, we shall call this standard coordinate structure \(\mathbb{G}^{(1,3)}\) (Definition 4). So, we shall obtain, by analogy with (1), \[\Phi:\overbrace{(\mathbb{P},B,\sim,\equiv^{\sim})}^{\text{synthetic structure}}\to\overbrace{\ \mathbb{G}^{(1,3)}.}^{\text{coordinate structure}}\qquad{(3)}\]

Euclidean geometry, of course, was also first set out synthetically in Euclid’s Elements. However, Euclid’s Elements does not quite meet modern adequate standards of formal rigor. In particular, Moritz Pasch (1882) noted that certain betweenness properties of space were merely implicit in Euclid’s treatment. Influenced by Pasch and others, the synthetic axiomatization for Euclidean geometry was first made rigorous in Hilbert (1899), which was modified, extended, or simplified in a number of ways, one of which is Veblen (1904) (which extracted the purely betweenness part of Hilbert’s system: sometimes called the “axioms of order”).

Synthetic axiomatization for Minkowski spacetime geometry appeared soon after the classic work of Albert Einstein and Hermann Minkowski (i.e., Einstein 1905; Minkowski 1909) in Alfred Robb’s (1911) book. This led to a series of later synthetic developments, including Robb (1936), Ax (1978), Mundy (1986), Goldblatt (1987), Schutz (1997), and, most recently, Cocco and Babic (2021). As is now known, Minkowski spacetime can be axiomatized using a single binary relation, usually called \(\lambda\), with \(p\lambda q\) meaning “points \(p\) and \(q\) can be connected by a light signal”—the light-signal relation.¹⁴ As the reader probably knows, this induces a “light cone structure” on the carrier set of points. So, Minkowski spacetime can be defined as a structure \((\mathbb{P},\lambda)\) satisfying certain axioms, and one may prove that there is an isomorphism \(\Phi:(\mathbb{P},\lambda)\to(\mathbb{R}^{4},\lambda_{\mathbb{R}^{4}})\).¹⁵ Such an isomorphism is called a “Lorentz coordinate system.” Then the automorphism group \(\text{Aut}((\mathbb{R}^{4},\lambda_{\mathbb{R}^{4}}))\) of \((\mathbb{R}^{4},\lambda_{\mathbb{R}^{4}})\) is the Poincaré group.¹⁶

Galilean spacetime, however, is the basic spacetime of classical Newtonian (pre-relativistic) physics. In retrospect, it is a kind of “low energy limit” of Minkowski spacetime (when we let the speed of light approach infinity and all the light cones get “squashed” into simultaneity surfaces). But, unlike the case with Minkowski spacetime, the synthetic approach did not appear for a long time. As far as I know, the first brief sketch of a synthetic axiom system for Galilean spacetime appeared in Hartry Field’s Science Without Numbers (1980, chap. 6), some 80 years after Hilbert’s classic monograph, The Foundations of Geometry (1899), and close on three hundred years after Newton’s Principia (1687). Shortly after, John Burgess added further work on this in Burgess (1984) and then again in Burgess and Rosen (1997). Our work here is a descendant of and stimulated by theirs.¹⁷

The axiom system \(\mathsf{Gal}(1,3)\) we shall arrive at can be written as follows (see table 1 in section 3):

Here, \(\mathsf{BG}(4)\) is a group of nine axioms, the subsystem of order axioms for betweenness (see appendix A below). And \(\mathsf{EG}(3)^{\sim}\) is a group of eleven axioms, a relativized subsystem of axioms for “sim-congruence” and betweenness, obtained from Tarski’s formulation of Euclidean geometry for three dimensions (see appendix A). The three further axioms, \(\mathsf{Gal}3\), \(\mathsf{Gal}4\), and \(\mathsf{Gal}5\), “tie together” these subsystems.¹⁸

To summarize, then, how the rest of this paper goes, we shall use the two separate Representation Theorems for \(\mathsf{BG}(4)\) and \(\mathsf{EG}(3)\). The first of these (theorem 62 in appendix B below) asserts the existence of a “global” bijective coordinate system: \[\Phi:\mathbb{P}\to\mathbb{R}^{4},\qquad{(4)}\] on any (full) model \((\mathbb{P},B)\) of \(\mathsf{BG}(4)\), matching any given “4-frame” \(O,X,Y,Z,I\) and satisfying the betweenness representation condition, for any points \(p,q,r\in\mathbb{P}\):¹⁹ \[\begin{aligned} B(p,q,r) & \leftrightarrow B_{\mathbb{R}^{4}}(\Phi(p),\Phi(q),\Phi(r)), \end{aligned}\qquad{(5)}\] where \(B_{\mathbb{R}^{4}}\) is the standard betweenness relation on \(\mathbb{R}^{4}\). The second Representation Theorem (theorem 63 in appendix B) asserts the existence of a global coordinate system \(\psi\) on any (full) model \((\mathbb{P},B,\equiv)\) of three-dimensional Euclidean geometry \(\mathsf{EG}(3)\), matching a given “Euclidean 3-frame” \(O,X,Y,Z\) and satisfying the representation condition for congruence: \[\begin{aligned} pq\equiv rs & \leftrightarrow\psi(p)\psi(q)\equiv_{\mathbb{R}^{3}}\psi(r)\psi(s), \end{aligned}\qquad{(6)}\] where \(\equiv_{\mathbb{R}^{3}}\) is the standard congruence relation on \(\mathbb{R}^{3}\). In our system, the axioms \(\mathsf{EG}(3)\) are relativized to simultaneity hypersurfaces, yielding \(\mathsf{EG}(3)^{\sim}\). The relativization implements the requirement that each simultaneity hypersurface is a three-dimensional Euclidean space.

We can then combine these two Representation Theorems, applied to any full model \(M\models_{2}\mathsf{Gal}(1,3)\), to obtain the Representation Theorem for \(\mathsf{Gal}(1,3)\), which is our main theorem (theorem 55 in section 5). That is, assuming \((\mathbb{P},B,\sim,\equiv^{\sim})\) is a (full) model of \(\mathsf{Gal}(1,3)\), the existence of an isomorphism as stated in (3) above: \[\Phi:\overbrace{(\mathbb{P},B,\sim,\equiv^{\sim})}^{\text{synthetic structure}}\to\overbrace{\ \mathbb{G}^{(1,3)}.\ }^{\text{coordinate structure}}\qquad{(7)}\]

The crux of the proof of the main theorem are the Chronology Lemma (lemma 52) and the Congruence Lemma (lemma 54).

1 Definitions

Our central interest is \(\mathbb{G}^{(1,3)}\), the standard coordinate structure for four-dimensional Galilean spacetime. The carrier set of \(\mathbb{G}^{(1,3)}\) is \(\mathbb{R}^{4}\). Its distinguished relations are betweenness (10, a), simultaneity (10, b), and sim-congruence (10, d) on \(\mathbb{R}^{4}\). Note that \(\mathbb{G}^{(1,3)}\) does not carry a metric or distance function.

2 Derivation of (Extended) Galilean Transformations

What is the symmetry group of the standard coordinate structure \(\mathbb{G}^{(1,3)}\) for Galilean spacetime? We will see that its symmetry group is a certain Lie group \(\mathcal{G}^{e}(1,3)\), a 12-dimensional Lie group that extends the usual Galilean group \(\mathcal{G}(1,3)\) by two additional parameters, which determine coordinate scalings.

The constants \(\alpha_{1},\alpha_{2}\) in any extended Galilean matrix \(A\) determine scalings of the spatial and temporal coordinates, respectively. So, given some \(A\) in the extended Galilean matrix group and any \((\vec{x},t)\in\mathbb{R}^{4}\), \[A(\vec{x},t)=(\alpha_{1}R\vec{x}+\vec{v}t,\alpha_{2}t).\qquad{(18)}\]

Let’s set the relative rotation \(R\) to be \(\mathbb{I}\) and set the relative velocity \(\vec{v}\) to be zero: \[A(\vec{x},t)=(\alpha_{1}\vec{x},\alpha_{2}t).\qquad{(19)}\]

Thus, the spatial coordinates are scaled by \(\alpha_{1}\), and the temporal coordinate is scaled by \(\alpha_{2}\). Instead, let us set these scalings \(\alpha_{1},\alpha_{2}\) at \(1\) and consider the image \((\vec{x}',t')\) of the point with coordinates \((\vec{x},t)\) under an extended Galilean transformation: \[\vec{x}'=R\vec{x}+\vec{v}t+\vec{d},\qquad{(20)}\] \[t'=t+d_{t}.\qquad{(21)}\]

These are the usual Galilean transformations as given in physics textbooks, in usually simplified form (e.g., Sears, Zemansky and Young 1979, 252; Longair 1984, 87; or Rindler 1977, 3). The conventional Galilean group \(\mathcal{G}(1,3)\) is normally understood to be this 10-parameter Lie group: the ten parameters are these: four parameters for the spatial and temporal translations, \(\mathbf{d}\); three parameters (i.e., determined by the three Euler angles) for the rotation matrix \(R\); three parameters for the velocity \(\vec{v}\).

As we have defined it, the extended Galilean group \(\mathcal{G}^{e}(1,3)\) is a 12-parameter Lie group: the two additional parameters, \(\alpha_{1},\alpha_{2}\), permit coordinate scalings. These two extra degrees of freedom are a consequence of our synthetic treatment, and this is completely analogous to Euclidean betweenness and congruence being invariant under coordinate scaling. Indeed, \(\alpha_{1}\) and \(\alpha_{2}\) are gauge parameters in the oldest sense of the word.

3 Axiomatization of Galilean Spacetime: \(\mathsf{Gal}(1,3)\)

To begin, we state the informal physical meanings of our three primitive symbols:²³

We are now ready to state the (synthetic) axioms for Galilean spacetime.

In discussing a full model \(M\) of, say, \(\mathsf{BG}(4)\), I shall generally write “\(M\models_{2}\mathsf{BG}(4)\)” to make it clear that \(M\) is a full model of \(\mathsf{BG}(4)\). In other words, if \(M=(\mathbb{P},\dots)\), then \(M\models_{2}\forall\mathsf{X}_{i}\,\varphi(\mathsf{X}_{i})\) if and only if, for every subset \(U\subseteq\mathbb{P}\), \(\varphi[U]\) is true in \(M\).

\(\mathsf{BG}(4)\) is really an axiom group of nine axioms for \(\texttt{Bet}\).²⁵ These are given in definition 56 in appendix A. But, to simplify the description here, one may take their conjunction.²⁶ \(\mathsf{EG}(3)\) is also an axiom group, this time of eleven axioms. These are given in definition 57 in appendix A. The axiom \(\mathsf{EG}(3)^{\sim}\) listed above requires further explanation.²⁷

This construction is sketched, very briefly, in Field (1980, 54, n.33). First, one replaces \(\equiv\) by \(\equiv^{\sim}\) in each \(\mathsf{EG}(3)\) axiom. Next, one relativizes each axiom to the formula \(p\sim z\) (treating \(z\) as a parameter) so that the resulting axiom says that it holds for all points simultaneous with \(z\).²⁸ Next, one prefixes the result with \(\forall z\) and then takes the conjunction of the axioms. For example, under relativization, the \(\equiv\)-Transitivity axiom (E3) and the Pasch axiom (E6) become:

In addition to the given non-logical axioms, we also have the customary axioms for second-order logic (table 2):

I shall, in effect, however, assume an ambient set theory.²⁹ The reason is that I am not concerned with narrow proof-theoretic matters concerning the whole theory (for example, completeness) but rather with establishing some facts about the full models of the theory \(\mathsf{Gal}(1,3)\). Since we consider just full models, Comprehension and Extensionality are satisfied more or less by fiat.³⁰ This is completely analogous to our approach in giving the usual proof, essentially that of Dedekind (1888), of the categoricity of second-order arithmetic \(\mathsf{PA}_2\), although, as a matter of fact, the categoricity of \(\mathsf{PA}_2\) can be “internalized” as a proof inside \(\mathsf{PA}_2\) itself (see Simpson and Yokoyama 2013).

The three Galilean axioms \(\mathsf{Gal}3\), \(\mathsf{Gal}4\), and \(\mathsf{Gal}5\) are the glue that holds together the betweenness axioms \(\mathsf{BG}(4)\) and the Euclidean axioms \(\mathsf{EG}(3)^{\sim}\). The content of \(\mathsf{Gal}3\) and \(\mathsf{Gal}4\) seems evident. The final axiom \(\mathsf{Gal}5\) is the sole axiom that needs some further explanation.³¹ This axiom expresses the translation invariance of the \(\equiv^{\sim}\) relation and may be expressed using vector notation as follows: \[pq\equiv^{\sim}rs\to(p+\mathbf{v})(q+\mathbf{v})\equiv^{\sim}(r+\mathbf{v})(s+\mathbf{v}).\qquad{(22)}\]

In other words, if the (simultaneous) segments \(pq\) and \(rs\) have the same length, then the (simultaneous) segments \((p+\mathbf{v})(q+\mathbf{v})\) and \((r+\mathbf{v})(s+\mathbf{v})\) have the same length for any vector \(\mathbf{v}\).³²

An equivalent axiom can be expressed solely using the primitives \(\texttt{Bet}\), \(\sim\), and \(\equiv^{\sim}\) and quantifying over points. Roughly, the axiom \(\mathsf{Gal}5\) is equivalent to the following rather long-winded claim:

Note that the equality clause “\(\mathbf{v}_{p,p'}=\mathbf{v}_{q,q'}\)” means “\(p,q,p',q'\) is a parallelogram,” and the 4-place predicate “\(p_{1},p_{2},p_{3},p_{4}\) is a parallelogram” can be defined using \(\texttt{Bet}\) (see definition 15).

The second-order theories \(\mathsf{BG}(4)\) and \(\mathsf{EG}(3)\), with their point set variables, contain the second-order Continuity Axiom (Tarski 1959, 18): \[\begin{gathered} [\exists r\,(\forall p\in\mathsf{X}_{1})\,(\forall q\in\mathsf{X}_{2}) \texttt{Bet}(r,p,q)]\\ \to[\exists s\,(\forall p\in\mathsf{X}_{1})\,(\forall q\in\mathsf{X}_{2})\,\texttt{Bet}(p,s,q)]. \end{gathered}\qquad{(23)}\]

This geometrical continuity axiom, it may be noted, is closely analogous to the “Dedekind Cut Axiom,” which may be used as an axiom in the formalization of the second-order theory \(\mathsf{ALG}\) of real numbers:³³ \[\begin{gathered} (\forall\mathsf{X}_{1}\subseteq\mathbb{R})\,(\forall\mathsf{X}_{2}\subseteq\mathbb{R})\,(\mathsf{X}_{1}\neq\varnothing\wedge\mathsf{X}_{2}\neq\varnothing\wedge\overbrace{(\forall x\in\mathsf{X}_{1})\,(\forall y\in\mathsf{X}_{2})\,(x\leq y)}^{\mathsf{X}_{1}\text{ ``precedes" }\mathsf{X}_{2}}\\ \to\exists s\,\overbrace{(\forall x\in\mathsf{X}_{1})\,(\forall y\in\mathsf{X}_{2})\,(x\leq s\wedge s\leq y))}^{\text{the point $s$ ``cuts" $\mathsf{X}_{1}$ and $\mathsf{X}_{2}$}}. \end{gathered}\qquad{(24)}\]

The second-order theories \(\mathsf{BG}(4)\) and \(\mathsf{EG}(3)\) are, foundationally speaking, strong, and both interpret \(\mathsf{ALG}\). They have first-order versions—their “little brothers,” so to speak, which I shall call \(\mathsf{BG}_{0}(4)\) and \(\mathsf{EG}_{0}(3)\)—obtained by replacing the single Continuity Axiom by infinitely many instances of the Continuity axiom scheme: in these instances, there are only point variables.

The little brothers, \(\mathsf{BG}_{0}(4)\) and \(\mathsf{EG}_{0}(3)\), are meta-mathematically somewhat different from their big brothers. In particular, they are, in fact, complete (and, since they are recursively axiomatized, decidable), as established by a celebrated theorem of Alfred Tarski (1951). But the big brothers are incomplete because they interpret Peano arithmetic (\(\mathsf{PA}\)), and then Gödel’s incompleteness results apply. This observation leads to an important difficulty faced by Field’s nominalism:

4 Main Results About \(\mathsf{Gal}(1,3)\)

4.1 Definitions: Betweenness Geometry

The theory \(\mathsf{BG}(4)\) proves the existence of a 4-frame: this is simply the Lower Dimension Axiom (the axioms are listed in appendix A). It can be proved in \(\mathsf{BG}(4)\) that, given a line \(\ell\) and a point \(p\), there is a unique line \(\ell'\) parallel to \(\ell\) and containing \(p\) (this is called Playfair’s Axiom and is an equivalent of Euclid’s Parallel Postulate). From Playfair’s Axiom, it can be proved in \(\mathsf{BG}(4)\) that \(\parallel\) is an equivalence relation. A number of other theorems from plane and solid geometry can be established, including Desargues’s Theorem and Pappus’s Theorem. See Bennett (1995) for an explanation of these theorems. It can be proved that there is a bijection between any pair of lines. The claims mentioned so far are sufficient (the assumptions required include Desargues’s Theorem and Pappus’s Theorem) to establish that, given distinct parameters \(p,q\), the line \(\ell(p,q)\) is isomorphic to an ordered field.³⁵ The Continuity Axiom of \(\mathsf{BG}(4)\) then ensures that this field is order-complete. From this, we conclude that there is a (unique) isomorphism \(\varphi_{p,q}:\ell(p,q)\to\mathbb{R}\), i.e., \(\varphi_{p,q}(p)=0\) and \(\varphi_{p,q}(q)=1\). See also the proof sketch for theorem 62 below.

4.2 Definitions: Galilean Geometry

Turning to the system \(\mathsf{Gal}(1,3)\), we need separate definitions of notions pertaining to simultaneity (\(\sim\)) and sim-congruence (\(\equiv^{\sim}\)).

Beyond the notion of a 4-frame, we need a few more specialized notions of “frame” for Galilean spacetime.

4.3 Soundness

It is straightforward to demonstrate that \(\mathsf{Gal}(1,3)\) is true in the coordinate structure \(\mathbb{G}^{(1,3)}\) by verifying that each axiom of \(\mathsf{Gal}(1,3)\) is true in \(\mathbb{G}^{(1,3)}\).

4.4 Lemmas

4.5 Vector Methods

In the first part of this section, we first assume that we are considering a full model \(M\models_{2}\mathsf{BG}(4)\), with \(M=(\mathbb{P},B)\) (i.e., \(B\subseteq\mathbb{P}^{3}\) is the interpretation in \(M\) of the predicate \(\texttt{Bet}\)). And then, we further assume we are considering a full model \(M\models_{2}\mathsf{Gal}(1,3)\), with \(M=(\mathbb{P},B,\sim,\equiv^{\sim})\). We assume the material in appendix D, which introduces the new sorts: reals and vectors.³⁷ The vector displacement from \(p\) to \(q\) is written: \(\mathbf{v}_{p,q}\).³⁸ In particular, recall that, by theorem 68, the vector space \(\mathbb{V}\) of displacements is isomorphic to \(\mathbb{R}^{4}\) (as a vector space).³⁹

Since \(M\models_{2}\mathsf{BG}(4)\), we know, by theorem 62, that there exists a coordinate system \(\Phi:\mathbb{P}\to\mathbb{R}^{4}\) on \(M\), i.e., an isomorphism \(\Phi:(\mathbb{P},B)\to(\mathbb{R}^{4},B_{\mathbb{R}^{4}})\).

This is established inside the detailed proof of theorem 68 below.

This is a corollary of lemma 27.

Given a coordinate system \(\Phi\) and a point \(p\), the four components of \(\Phi(p)\) are written as follows: \[\Phi(p)=\begin{pmatrix}\Phi^{1}(p)\\\Phi^{2}(p)\\\Phi^{3}(p)\\\Phi^{4}(p)\end{pmatrix}.\qquad{(28)}\]

Note that the vector \(\mathbf{v}_{p,q}\) from \(p\) to \(q\) is entirely coordinate-independent.

Let us now assume we are considering a full model \(M\models_{2}\mathsf{Gal}(1,3)\), with \(M=(\mathbb{P},B,\sim,\equiv^{\sim})\).

Definition 34 yields:

From lemma 33, we obtain:

This is a corollary of the previous lemma.

4.6 Representation

In order to prove the Representation Theorem for \(\mathsf{Gal}(1,3)\), we need to establish three main lemmas. I call these the Chronology Lemma, the Galilean Frame Translation Invariance Lemma, and the Congruence Lemma.

4.7 The Chronology Lemma

4.8 The Galilean Frame Translation Invariance Lemma

That is, leaving the assumptions as stated, when we apply a translation (given by a vector \(\mathbf{v}\)) to a Galilean frame, so \(O'=O+\mathbf{v}\), etc., the result is also a Galilean frame: \[O,X,Y,Z,I\text{ is a Galilean 4-frame iff }O',X',Y',Z'\text{ is a Galilean 4-frame.}\qquad{(42)}\]

Proof. Without loss of generality, we may suppose that \(\mathbf{v}\) does not lie in the simultaneity hypersurface \(\Sigma_{O}\). For if it does, the vector will simply translate the frame “horizontally,” along within \(\Sigma_{O}\) and the Euclidean axioms, along with the fact that the temporal benchmark point \(I\) also moves “horizontally” too within the hypersurface \(\Sigma_{I}\), guarantee that \(O',X',Y',Z',I'\) is a Galilean 4-frame.

I will sketch how the proof goes. It is best illustrated by figure 2.

This is the sole part of our analysis appealing to the axiom \(\mathsf{Gal}5\), stating the translation invariance of \(\equiv^{\sim}\).

The five points \(O,X,Y,Z,I\) form a Galilean frame, and thus the four points \(O,X,Y,Z\) form a Euclidean sim 3-frame. So, in the lower simultaneity hypersurface, \(\Sigma_O\), we have a Euclidean sim 3-frame \(O,X,Y,Z\): the three legs \(OX\), \(OY\), and \(OZ\) are perpendicular and of equal length. (The point \(Z\) and the axis \(\ell(O,Z)\) are suppressed in figure 2.)

Consider the hypersurface \(\Sigma_{O'}\). By assumption, each of the points \(O',X',Y',Z'\) is obtained by adding the same displacement vector: \(\mathbf{v}=\mathbf{v}_{O,O'}\): \[\begin{gathered} O'=O+\mathbf{v},\quad X'=X+\mathbf{v},\\ Y'=Y+\mathbf{v},\quad Z'=Z+\mathbf{v}. \end{gathered}\qquad{(43)}\]

Since \(O,X,Y,Z\) are simultaneous, it follows, using lemma 45, that \(O',X',Y',Z'\) are simultaneous. So, all four points lie in \(\Sigma_{O'}\).

Next, we use the Translation Invariance axiom \(\mathsf{Gal}5\) of \(\mathsf{Gal}(1,3)\): \(\equiv^{\sim}\) is translation invariant. Since \(O,X,Y,Z\) form a Euclidean sim 3-frame, we may conclude, from the translation invariance of \(\equiv^{\sim}\), that \(O',X',Y',Z'\) is also a Euclidean sim 3-frame. Since \(\mathbf{v}\) does not lie parallel to \(\Sigma_{O}\), \(I'\) is not simultaneous with \(O',X',Y',Z'\). And, so, \(O',X',Y',Z',I'\) is a Galilean 4-frame.∎

4.9 The Congruence Lemma

Proof. We are given a structure \(M=(\mathbb{P},B,\sim,\equiv^{\sim})\), a Galilean frame, \(O,X,Y,Z,I\) in \(M\), and an isomorphism \(\Phi:(\mathbb{P},B,\sim)\to(\mathbb{R}^{4},B_{\mathbb{R}^{4}},\sim_{\mathbb{R}^{4}})\), matching \(O,X,Y,Z,I\). We shall call \(\Phi\) the “global isomorphism.” We claim that \(\equiv^{\sim}_{\mathbb{R}^{4}}\) represents \(\equiv^{\sim}\) with respect to \(\Phi\); that is, for simultaneous points \(p,q,r,s\), we have:⁴⁰ \[pq\equiv^{\sim} rs\leftrightarrow\Delta_{3}(\vec{\Phi}(p),\vec{\Phi}(q))=\Delta_3(\vec{\Phi}(r),\vec{\Phi}(s)).\qquad{(44)}\]

Consider figure 3:

By hypothesis, the five points \(O,X,Y,Z,I\) form a Galilean frame, and thus the four points \(O,X,Y,Z\) form a Euclidean sim 3-frame. For points in the lower simultaneity hypersurface, \(\Sigma_{O}\), we have, from the Euclidean axiom group \(\mathsf{EG}(3)^{\sim}\) in \(\mathsf{Gal}(1,3)\) and the Representation Theorem for Euclidean geometry (theorem 63), the existence of an isomorphism (i.e., coordinate system on \(\Sigma_{O}\)), \[\psi_{O}:(\Sigma_{O},B\upharpoonright_{\Sigma_{O}},(\equiv^{\sim})\upharpoonright_{\Sigma_{O}})\to(\mathbb{R}^{3},B_{\mathbb{R}^{3}},\equiv_{\mathbb{R}^{3}}),\qquad{(45)}\] that matches this Euclidean sim 3-frame \(O,X,Y,Z\). So, in the hypersurface \(\Sigma_{O}\), a “mini-representation theorem” holds. For any \(p,q,r,s\in\Sigma_{O}\), \[pq\equiv^{\sim}rs\leftrightarrow\vec{\psi}_{O}(p)\vec{\psi}_{O}(q)\equiv_{\mathbb{R}^{3}}\vec{\psi}_{O}(r),\vec{\psi}_{O}(s).\qquad{(46)}\]

Let \(\Phi_{O}\) be \(\Phi\upharpoonright_{\Sigma_{O}}\): the restriction of the global isomorphism \(\Phi\) to the hypersurface \(\Sigma_{O}\). We are also given that \(\Phi_{O}\) also matches \(O,X,Y,Z\). By the uniqueness of coordinate systems that match the same frame (lemma 66), we conclude: \[\psi_{O}=\Phi_{O}.\qquad{(47)}\]

Thus, by (46) and (47), \(\Phi_{O}\) satisfies: \[pq\equiv^{\sim}rs\leftrightarrow\vec{\Phi}_{O}(p)\vec{\Phi}_{O}(q)\equiv_{\mathbb{R}^{3}}\vec{\Phi}_{O}(r),\vec{\Phi}_{O}(s).\qquad{(48)}\]

We now repeat the same argument for an arbitrary simultaneity surface, \(\Sigma_{u}\).

Given any point \(u\), we consider the hypersurface \(\Sigma_{u}\). By lemma 46, the time axis \(\ell(O,I)\) intersects \(\Sigma_{u}\) at the corresponding “origin,” \(O_{u}\). By lemma 22, there are unique lines through \(X\), \(Y\), and \(Z\), each parallel to \(\ell(O,O_{u})\). By lemma 46 again, these intersect \(\Sigma_{u}\) at points \(X_{u},Y_{u},Z_{u}\). By lemma 44, the hypersurfaces \(\Sigma_{O}\) and \(\Sigma_{u}\) are parallel; this guarantees that each of the points \(O_{u},X_{u},Y_{u},Z_{u}\) is obtained by adding the same displacement vector: \(\mathbf{v}=\mathbf{v}_{O,O_{u}}\): \[\begin{gathered} O_{u}=O+\mathbf{v},\quad X_{u}=X+\mathbf{v},\\ Y_{u}=Y+\mathbf{v},\quad Z_{u}=Z+\mathbf{v}. \end{gathered}\qquad{(49)}\]

By the Translation Invariance of Galilean frames, lemma 53, since \(O,X,Y,Z,I\) form a Galilean 4-frame, we may conclude that \(O_{u},X_{u},Y_{u},Z_{u},I_{u}\) (where \(I_{u}=I+\mathbf{v}\)) also form a Galilean 4-frame. And thus, \(O_{u},X_{u},Y_{u},Z_{u}\) form a Euclidean sim 3-frame. By the Representation Theorem for Euclidean geometry, there is an isomorphism \(\psi_{u}\), which matches \(O_{u},X_{u},Y_{u},Z_{u}\). By similar reasoning to the case of \(\Sigma_{O}\), we define the restriction \(\Phi_{u}\) to be \(\Phi\upharpoonright_{\Sigma_{u}}\)—i.e., the restriction of the global isomorphism \(\Phi\) to the hypersurface \(\Sigma_{u}\). We can conclude: \[\psi_{u}=\Phi_{u}.\qquad{(50)}\] Thus, \(\Phi_{u}\) satisfies the following: for any points \(p,q,r,s\in\Sigma_{u}\), \[pq\equiv^{\sim}rs\quad\leftrightarrow\quad\vec{\Phi}_{u}(p)\,\vec{\Phi}_{u}(q)\equiv_{\mathbb{R}^{3}}\vec{\Phi}_{u}(r)\,\vec{\Phi}_{u}(s).\qquad{(51)}\] This is equivalent to (44).∎

5 Representation Theorem for \(\mathsf{Gal}(1,3)\)

Our main theorem is then the following:

Such isomorphisms \(\Phi:M\to\mathbb{G}^{(1,3)}\) are inertial charts on Galilean spacetime. They correspond, one-to-one, with Galilean frames. As we have seen, the transformation group between these isomorphisms (or, if you wish, between the Galilean frames) is precisely \(\mathcal{G}^{e}(1,3)\)—the extended Galilean group.

Appendices

Appendix A: Axioms

See Szczerba and Tarski (1979, 159–160) for the first-order two-dimensional theory \(\textsf{GA}_{2}\) (for “neutral” or “absolute geometry”), which lacks the Euclid Parallel axiom (which is called (E) in Szczerba and Tarski 1979 and is called (Euclid) above). Their system includes Desargues’s Theorem. But, for us, this axiom is no longer required, as it is provable from the remaining axioms in dimensions above two (Szczerba and Tarski 1979, 190). The above axiom system is the second-order, four-dimensional theory and contains (E), i.e., (Euclid). The relevant representation theorem follows from theorem 5.12 of Szczerba and Tarski (1979, 185, see also example 6.1). The same theorem is stated, somewhat indirectly, in Borsuk and Smielew (1960, 196–197). The representation theorem itself goes back to Veblen (1904).

The original source of this axiomatization is Tarski (1959) and Tarski and Givant (1999). See Tarski (1959, 19–20) for a formulation of the first-order two-dimensional theory, with twelve axioms and one axiom scheme (for continuity); and Tarski and Givant (1999) for a simplification down to ten axioms and one axiom scheme (for continuity). The above axiom system is the second-order, four-dimensional theory (i.e., the single Continuity Axiom is the second-order one).

Appendix B: Representation Theorems

The following two theorems are primarily due to Hilbert (1899), Veblen (1904), and Tarski (1959):⁴⁴

Proof. I give a brief sketch. Given a 4-frame \(O,X,Y,Z,I\) in \(M\), we first define four lines \(\ell(O,X),\ell(O,Y),\ell(O,Z)\), and \(\ell(O,I)\): these are the “\(x\)-axis,” “\(y\)-axis,” “\(z\)-axis,” and “\(t\)-axis” of the 4-frame. One can define (as in Hilbert 1899) geometrical operations \(+\), \(\times\), and a linear order \(\leq\) on each axis (relative to the two fixed parameters that determined that axis). These definitions are explained very clearly in Bennett (1995): for \(+\) at p. 48 and for \(\times\) at p. 62. Also, see Goldblatt (1987, 23–27). The definition of \(\leq\) is given in Tarski (1959, proof of theorem 1). Then, using the betweenness axioms, one shows that, on each axis, \(\ell(O,X),\ell(O,Y),\ell(O,Z)\), and \(\ell(O,I)\), these definitions specify an ordered field. For details (ignoring the order aspect), see Bennett (1995, 48–72, especially theorem 1, p. 72). What is more, the Continuity Axiom guarantees that this ordered field is a complete ordered field. Up to isomorphism, there is exactly one complete ordered field, and this is also rigid. Consequently, there is a (unique) isomorphism \(\varphi_{O,X}:\ell(O,X)\to\mathbb{R}\) (and similarly on each axis):

Given any point \(p\), one then constructs four “ordinates” \(p_{X},p_{Y},p_{Z},p_{I}\) on the four axes \(\ell(O,X),\ell(O,Y),\ell(O,Z),\ell(O,I)\) by certain parallel lines to these axes. Then, one defines the coordinate system \(\Phi\) as follows. Given any point \(p\in\mathbb{P}\), define: \[\Phi(p):=\begin{pmatrix}\varphi_{O,X}(p_{X})\\ \varphi_{O,Y}(p_{Y})\\ \varphi_{O,Z}(p_{Z})\\ \varphi_{O,I}(p_{I})\end{pmatrix}.\qquad{(55)}\]

It is clear that \(\Phi\) matches \(O,X,Y,Z,I\). Finally, one shows that \(\Phi\) is a bijection and that it satisfies the required isomorphism condition. Namely, for \(p,q,r\in\mathbb{P}\): \(B(p,q,r)\) iff \(B_{\mathbb{R}^{4}}(\Phi(p),\Phi(q),\Phi(r))\).∎

Roughly, this corresponds to theorem 1 of Tarski (1959), and a sketch of the proof is given there. The difference is that Tarski considers the two-dimensional first-order theory, whose axioms are what we’ve called \(\mathsf{EG}_{0}(2)\), with the first-order continuity axiom scheme. The Representation Theorem in Tarski (1959) asserts that, given a model \(M\models\mathsf{EG}_{0}(2)\) and a Euclidean frame, there is a real-closed field \(F\) such that the conditions (a), (b), (c) hold, with \(\mathbb{R}\) replaced by that field and “\(3\)” replaced by “\(2\).” When we strengthen to the second-order Continuity axiom, it follows that this field is in fact \(\mathbb{R}\).

Appendix C: Automorphisms and Coordinate Systems

This follows from two facts. First, if \(\Phi,\Psi:M\to(\mathbb{R}^{4},B_{\mathbb{R}^{4}})\) are isomorphisms, then \(\Psi\circ\Phi^{-1}\in\text{Aut}((\mathbb{R}^{4},B_{\mathbb{R}^{4}}))\). Second, we have \(\text{Aut}((\mathbb{R}^{4},B_{\mathbb{R}^{4}}))=\text{Aff}(4)\). (This is the result given in theorem 64 for the automorphisms of the standard coordinate structure \((\mathbb{R}^{4},B_{\mathbb{R}^{4}})\) for \(\mathsf{BG}(4)\).)

The proof applies the coordinate transformation equation (57) to the five points, \(O,X,Y,Z,I\), which gives five specific instances. The first of these implies that \(\mathbf{d}=\mathbf{0}\). The remaining four imply that the \(GL(4)\) matrix \(A\) is the identity matrix. Similar reasoning applies in any dimension and also to the Euclidean case.

Appendix D: Reals and Vectors

Given a model \((\mathbb{P},B)\models_{2}\mathsf{BG}(4)\), we know, by theorem 62, that it is isomorphic to the standard coordinate structure \((\mathbb{R}^{4},B_{\mathbb{R}^{4}})\).

Using abstraction (or, equivalently, a quotient construction), we can extend \((\mathbb{P},B)\) with a new sort (or “universe” or carrier set) \(\Re\) (of ratios) and operations \(0,1,+,\times,\leq\) to a two-sorted structure \((\mathbb{P},\Re;B; 0,1,+,\times,\leq)\) where the reduct \((\Re;0,1,+,\times,\leq)\) is isomorphic to \(\mathbb{R}\) (as an ordered field).⁴⁵ Call a triple \(p,q,r\) of points a configuration just if \(p\neq q\) and \(p,q,r\) are collinear. This abstraction proceeds by the equivalence relation on configurations \((p,q,r)\) of proportionateness. In geometrical terms, there are three basic cases of proportionateness:⁴⁶

A real, or ratio, is then an equivalence class \([(p,q,r)]\) with respect to proportionateness, and \(\Re\) is the set of these equivalence classes. One may define a zero \(0\) as \([(p,q,p)]\) and a unit \(1\) as \([(p,q,q)]\). One defines field operations \(+\), \(\times\), \(\leq\) in terms of the corresponding operations on a fixed line (see Bennett 1995). One readily checks that the result is that \(\Re\), with these operations, is a complete ordered field (and can then be identified with \(\mathbb{R}\)). Although we described this model theoretically, this construction can be “internalized” within \(\mathsf{BG}(4)\) by adding suitable abstraction axioms (a “definition by abstraction”) for a new sort, with variables \(\xi_{i}\) and a 3-place function symbol \(\xi(p,q,r)\), and then explicitly defining \(0\), \(1\), \(+\), \(\times\), and \(\leq\) on these new objects, and then proving that the resulting abstracta, i.e., the \(\xi(p,q,r)\) for any configuration \(p,q,r\), satisfy the second-order axioms for a complete ordered field.⁴⁷

We may further extend, with a new universe \(\mathbb{V}\) (of displacements, or vectors) and operations \(\mathbf{0},+,\cdot\), to a three-sorted structure \((\mathbb{P},\Re,\mathbb{V};B,0,1,+,\times,\leq;\mathbf{0},+,\cdot)\), where the reduct \((\mathbb{V},\Re;0,1,+,\times;\mathbf{0},+,\cdot)\) is isomorphic to \(\mathbb{R}^{4}\) (as a vector space).⁴⁸ This abstraction proceeds by the equivalence relation on ordered pairs \((p,q)\) of equipollence: \((p,q)\) is equipollent to \((r,s)\) just if \(p,q,s,r\) is a parallelogram:

A displacement, or vector, is then an equivalence class \([(p,q)]\) with respect to equipollence, and \(\mathbb{V}\) is the set of these equivalence classes. An equivalence class \([(p,q)]\) is written \(\mathbf{v}_{p,q}\). One may define the zero vector \(\mathbf{0}\) as \(\mathbf{v}_{p,p}\). One defines vector addition \(+\) so that \(\mathbf{v}_{p,q}+\mathbf{v}_{q,r}=\mathbf{v}_{p,r}\) holds (usually called Chasles’s Relation). One may define the scalar multiplication \(\cdot\) so that, when \(p\neq q\), \(\alpha\cdot\mathbf{v}_{p,q}=\mathbf{v}_{p,r}\) just if \(\alpha=[(p,q,r)]\); and, otherwise, \(\alpha\cdot\mathbf{0}=\mathbf{0}\). One checks that the vector space axioms are true and that \(\mathbb{V}\) is 4-dimensional.

Finally, by an explicit definition of an action \(+:\mathbb{P}\times\mathbb{V}\to\mathbb{P}\), we can further extend to \((\mathbb{P},\Re,\mathbb{V};B;0,1,+,\times,\leq;\mathbf{0},+,\cdot;+)\) such that \((\mathbb{P},\mathbb{V},+)\) is isomorphic to the affine space \(\mathbb{A}^{4}\).⁴⁹ The definition of the action \((p,\mathbf{v})\mapsto p+\mathbf{v}\) is: \(q=p+\mathbf{v}\) iff \(\mathbf{v}=\mathbf{v}_{p,q}\). One may then show that \(+\) is a free and transitive action of \(\mathbb{V}\) on \(\mathbb{P}\). The affine space obtained in this way (basically, from the vector space \(\mathbb{R}^{4}\), by “forgetting the origin”) is called \(\mathbb{A}^{4}\).

The discussion and constructions above may be summarized in the following three theorems (I follow the usual practice of conflating the name of a structure with the name of its carrier set):

Acknowledgements

I am grateful to two anonymous referees for their helpful comments. I am grateful to Professor Victor Pambuccian and Professor Robert Goldblatt for helping me clear up some confused thoughts of mine. I am grateful to Professor David Malament for detailed comments on an earlier draft of this article and for the suggestion of using vectors to simplify things. I am grateful to Joshua Babic and Lorenzo Cocco for some valuable advice. This work was supported by a research grant from the Polish National Science Center (Narodowe Centrum Nauki w Krakowie (NCN), Kraków, Poland), grant number 2020/39/B/HS1/02020.