Some Results on Causal Modalities in General Spacetimes
June 30, 2026
Abstract
Causality is one of the fundamental structures of spacetimes, determining the possible behaviour and propagation of physical information. Causal structure can be analysed through the various modal logics it induces. The modal logics for the chronological and causal relations of the archetypal Minkowski spacetime have been classified. However, only partial results have been achieved for the strict variant of the causal relation, known as the after relation. Towards classification, it was shown by Shapirovsky and Shehtman that the after modality in Minkowski space satisfies a formula we call the ‘after formula’.
The present work continues this analysis towards arbitrary spacetimes. In particular, we prove that the after modality in any smooth spacetime satisfies the after formula. We introduce a related modal formula that demonstrates that the logic of two-dimensional spacetimes are more expressive than higher-dimensional ones. Lastly, we study the interrelation between the logical properties and physical properties along the causal ladder.
1 Introduction↩︎
There has been some research into the modal logic of Minkowski space, the spacetime of special relativity (Example 1). One of the early works is by Goldblatt [@Goldblatt1980], who showed that the modal logic of any \(1+n\)-dimensional Minkowski spacetime with the causal relation \(\preccurlyeq\), moving up to and possibly at the speed of light, is \(\mathbf{S4.2}\). Shehtman [@Shehtman1983] also observed similar results around that time for various \(\mathbf{S4}\) logics. Shapirovsky and Shehtman [@Shapirovsky2002] showed that the chronological relation \(\ll\), moving strictly slower than the speed of light, again for any \(1+n\)-dimensional Minkowski spacetime, is given by the modal logic \(\mathbf{OI.2}\), which is a sublogic of \(\mathbf{S4.2}\). The general definitions of \(\preccurlyeq,\ll\) are given in Section 2.
Recent works, such as [@Hirsch2018; @Hirsch2022], have been investigating the temporal modal logic, using both past and future modalities, of the strict variant of the causal relation (what is referred to as the after relation; see Section [sec:spacetime:causalstruct]). However, it has only been shown in two-dimensional Minkowski spacetime that the temporal logic of the after relation is decidable [@Hirsch2018]. Whilst the frames of Minkowski spacetime with the chronological and causal relation are complete with respect to their logics, it is unknown what the modal logic of Minkowski spacetime with the after relation is, and whether it is complete, although previous works have noted it has distinct properties [@Goldblatt1980; @Shapirovsky2005]. Mainly, it was proved that the modal logic of the after relation satisfies a formula we call the after formula (Section 4.1).
To the best of our knowledge, the modal logics of general spacetimes has not been investigated.1 What is the modal logic of a general spacetime? Some properties can be derived from the general differential geometric setup, such as that \(\ll\) is transitive and 2-dense (\(\mathbf{OI}\)) and \(\preccurlyeq\) is a preorder (\(\mathbf{S4}\)). One of the main difficulties in providing a more refined characterisation lies in the fact that, even though spacetimes locally behave like Minkowski space (locally inheriting the logic), general spacetimes can vary greatly in global topology and causal structure. Our main result (Theorem 4) proves that the after relation of any spacetime satisfies the after formula. Moreover, we study how the modal logics of the spacetime vary along where it sits on the so-called causal ladder (Sections 2.2 and 6).
2 Spacetimes and Causal Structure↩︎
We recall the basic definitions of causal structure in smooth spacetimes [@penrose1972TechniquesDifferentialTopology; @landsman2021FoundationsGeneralRelativity]. Formally, a spacetime is a (real second countable Hausdorff) smooth manifold \(M\) equipped with a Lorentzian metric \(g\) and a time orientation \(T\). The metric defines at each point \(x\in M\) a nondegenerate symmetric bilinear form \(g_x\colon T_xM\times T_xM\to \mathbb{R}\) on the tangent space, to be thought of as a generalised inner product. The difference is that \(g_x\) need not be positive definite, meaning non-zero vectors may have zero or even negative length. The Lorentzian signature is interpreted as one time dimension and \(n\) spatial dimensions. The time orientation \(T\) is a global smooth vector field that determines a consistent notion of future.
The fundamental causal relations are defined in terms of certain classes of curves induced by the metric (see Figure 1). For our purposes a curve is a continuous (piecewise) smooth function \(\gamma\colon I\to M\) defined on an interval \(I\subseteq \mathbb{R}\), and its image is the set \({\mathop{\mathrm{im}}(\gamma)= \{\gamma(t):t\in I\}}\). For \(x,y\in M\) we define the causal(ity), chronology and horismos relation as follows, respectively:
\(x\preccurlyeq y\) iff there exists a causal curve (moving up to lightspeed) from \(x\) to \(y\), or \(x=y\);
\(x\ll y\) iff there exists a timelike curve (moving slower than lightspeed) from \(x\) to \(y\);
\(x\rightarrow y\) iff there exists a lightlike curve (moving at lightspeed) from \(x\) to \(y\), or \(x=y\) (i.e., \(x\preccurlyeq y\) and not \(x \ll y\)).
For more detailed definitions see [@minguzzi2019LorentzianCausalityTheory]. Additionally, we define the after (or strictly causal) and reflexive chronological relation as follows, respectively:
\(x \mathrel{\scalebox{0.85}{\alpha}}y\) iff there exists a causal curve from \(x\) to \(y\) (read as “\(y\) happens after \(x\)”);
\(x \mathrel{\underline{\ll}}y\) iff there exists a timelike curve from \(x\) to \(y\), or \(x=y\).
The after relation, introduced in [@robb1914TheoryTimeSpace], is the ‘strict’ version of \(\preccurlyeq\), since causal curves are by definition non-degenerate, only allowing a reflexive pair \(x\mathrel{\scalebox{0.85}{\alpha}}x\) when there exists a causal loop from \(x\) to \(x\). We say \(x\) and \(y\) are spacelike separated if not \(x\preccurlyeq y\) and not \(y\preccurlyeq x\).
Example 1 (Minkowski spacetime). An important spacetime is \(1+n\)-dimensional Minkowski space, based on the manifold \(\mathbb{R}^{1+n}\). We denote a point \(x\in \mathbb{R}^{1+n}\) in components as \({(x^0,\vec{x})=(x^0,x^1,\ldots,x^n)}\). The metric and induced causal relations are then as follows (see Figure 1 for intuition): \[\eta(x,y) = -x^0y^0 + \sum_{i=1}^n x^iy^i, \quad\text{and}\quad \begin{array}{cc} x \ll y & \quad \text{iff}\quad y^0 > x^0 + \left\lVert\vec{y}-\vec{x}\right\rVert, \\ x \preccurlyeq y &\quad\text{iff}\quad y^0 \geq x^0 + \left\lVert\vec{y}-\vec{x}\right\rVert, \\ x \rightarrow y &\quad\text{iff}\quad y^0 = x^0 + \left\lVert\vec{y}-\vec{x}\right\rVert. \end{array} \label{eq:minkowski32causal32relations}\qquad{(1)}\]
2.1 Properties of the causal relations↩︎
A central theme of this work is characterising the (modal) properties of the causal relations of a spacetime. We first collect some well-established results from the literature [@penrose1972TechniquesDifferentialTopology; @kronheimer1967StructureCausalSpaces].
Definition 1. A relation \({\mathrel{\triangleleft}} \subseteq S \times S\) is called semi-full if:
(seriality) \(\forall x \in S\), there exists \(y \in S\) such that \(x \mathrel{\triangleleft}y\);
(2-dense) if \(x \mathrel{\triangleleft}y_1, y_2\), there exists \(z \in S\) such that \(x \mathrel{\triangleleft}z \mathrel{\triangleleft}y_1, y_2\).
Lemma 1. We have the following relations and properties of the causal orders:
2
\(x\ll y \implies x\mathrel{\scalebox{0.85}{\alpha}}y \implies x\preccurlyeq y\);
if \(x\neq y\) then \(x\mathrel{\scalebox{0.85}{\alpha}}y\) iff \(x\ll y\) or \(x\rightarrow y\);
\(\ll\) is semi-full, \(\mathrel{\scalebox{0.85}{\alpha}}\) is serial;
\(\ll\), \(\mathrel{\underline{\ll}}\), \(\mathrel{\scalebox{0.85}{\alpha}}\), \(\preccurlyeq\) are transitive;
\(\preccurlyeq\), \(\mathrel{\underline{\ll}},\rightarrow\) are reflexive.
We have that for \(x, y, z \in M\): \[x\ll y \preccurlyeq z \implies x\ll z \qquad\text{and}\qquad x\preccurlyeq y \ll z \implies x\ll z.\]
2.2 The Causal Ladder↩︎
The causal ladder [@minguzzi2019LorentzianCausalityTheory] provides a classification of spacetimes based on the properties of their causal relations. A basic version of it, sufficient for the present work, is depicted in Figure 2 (with the weakest property at the top). Below we define the properties needed in this work (see Section 6); for more disambiguated versions see e.g., [@minguzzi2019LorentzianCausalityTheory]. Let \(J^\pm\) and \(I^\pm\) denote the up/down closures of \(\preccurlyeq\) and \(\ll\), respectively. So \(J^{+}(x):=\{y\in M:x\preccurlyeq y\}\) and \(J^{-}(x):= \{ z\in M: z\preccurlyeq x\}\), and similarly for \(I^\pm\).
Definition 2. A spacetime is called:
**totally vicious* if \(x\ll x\) for all \(x\in M\) (i.e., \(\ll\) is reflexive). A spacetime is non-totally vicious (NTV) if there is some \(x \in M\) such that not \(x \ll x\) (i.e., \(\ll\) is not reflexive);*
**chronological* if not \(x \ll x\) for all \(x \in M\) (i.e., \(\ll\) is irreflexive);*
**causal* if \(x \preccurlyeq y\) and \(y \preccurlyeq x\) imply \(x = y\) (i.e., \(\preccurlyeq\) is anti-symmetric);*
**past-distinguishing* (resp. future-distinguishing) if \(I^{-}(x) = I^{-}(y)\) (resp. \(I^{+}(x) = I^{+}(y)\)) implies \(x = y\). If a spacetime is both past- and future-distinguishing it is called distinguishing;*
**globally hyperbolic* if the causal diamonds \(J^{+}(x)\cap J^{-}(y)\) are compact in the manifold topology for all \(x,y\in M\).*
For proofs of implication between the different properties, see [@Minguzzi08; @minguzzi2019LorentzianCausalityTheory]. We note that the implications are strict, e.g., there are chronological spacetimes that are not causal. The study of the causal ladder and the underlying dependencies is one of the cornerstones of modern mathematical relativity theory.
We provide two examples of spacetime that reside on different levels of the causal ladder, but we will see other examples throughout the paper.
Example 2. Minkowski space is globally hyperbolic.
Example 3. The spacetime depicted in Figure [fig:cntvchron:cntv] is a non-totally vicious spacetime. The manifold is \(\mathbb{R} \times S^1\), the surface of an infinitely long unit cylinder, and the lightcones are tilted from \(90^\circ\) to being upright at \(0^\circ\). This is known as the Misner spacetime, see [@minguzzi2019LorentzianCausalityTheory] for details. It is non-totally vicious because points on the dotted line, \((0, \theta)\), cannot chronologically reach themselves (even though causally they can).
2.3 Causally Non-Totally Vicious: A New Property for the Causal Ladder↩︎
Causal ladder properties can have multiple and equivalent definitions. In particular, the causal step has an interesting equivalent condition.
Lemma 2. Let \(M\) be a spacetime. Then \(M\) is causal, i.e., \(\preccurlyeq\) is anti-symmetric, iff \(\mathrel{\scalebox{0.85}{\alpha}}\) is irreflexive.
Both the chronological and causal properties on the causal ladder are affecting the spacetime in a similar way, but affect different relations. With the chronological relation, \(\ll\), there is a difference between losing reflexivity (being non-totally vicious) and gaining irreflexivity (being chronological). However, the causal property in the ladder combines the loss of reflexivity and gaining of irreflexivity on \(\scalebox{0.85}{\alpha}\) into one ladder property. By changing the perspective of the causal property affecting \(\mathrel{\scalebox{0.85}{\alpha}}\), we can introduce a class of spacetimes that separates the notion of losing reflexivity and gaining irreflexivity. Thus, we get a causal analogue of non-total vicious.
Definition 3. A spacetime is causally non-totally vicious (cNTV) iff \(\exists x \in M\) such that not \(x \mathrel{\scalebox{0.85}{\alpha}}x\).
The cNTV property makes \(\scalebox{0.85}{\alpha}\) lose reflexivity and now the causal property only gives \(\scalebox{0.85}{\alpha}\) the irreflexive property, separating the relational properties into individual steps on the causal ladder. There is an obvious question to ask: where does cNTV sit on the causal ladder?
A causal spacetime is cNTV, and a cNTV spacetime is NTV.
The proof of these implications is simply based on the definitions of the properties and is obvious.
Then, what is the relation between a spacetime being cNTV and it being chronological?
Theorem 1. We have that
there are chronological spacetimes that are not cNTV (Figure [fig:cntvchron:chron]);
there are cNTV spacetimes that are not chronological (Figure [fig:cntvchron:cntv]).
Proof. The proof of both can be observed in the spacetimes depicted in Figure 3, where each has one property but not the other. Both spacetimes use the same manifold, \(\mathbb{R} \times S^{1}\). The metric of Figure [fig:cntvchron:chron] is just quotiented Minkowski space, and Figure [fig:cntvchron:cntv] is Misner spacetime from Example 3. ◻
It is clear that a causal spacetime is cNTV and chronological, but we further have that a spacetime that is cNTV and chronological is not necessarily causal. A counterexample can be observed by taking the spacetime in Figure [fig:cntvchron:chron] and removing a point from it.
The cNTV property changes one end of the causal ladder to look different to the original ladder. Our additions to the causal ladder in Figure 2 are in bold. In Section 6, we will see how introducing the cNTV property into the causal ladder will make a clearer distinction of the modal logic of a spacetime to its position on the causal ladder.
3 Modal Logic↩︎
Now we introduce modal logic, which includes the standard logical connectives (conjuction, disjunction, etc.), atomic propositions, and modal operators (\(\square, \lozenge\)). Throughout, we assume a finite set of atomic propositions, \(AP= \{p_1, p_2, \dots\}\). We refer to [@Blackburn2001; @BoxesAndDiamonds] for common definitions and theorems. Throughout, we make use of Kripke frames, \(\langle M, \mathrel{\triangleleft} \rangle\), using \(M\) to denote the set of points/worlds and \(\mathrel{\triangleleft}\) to denote the relation. For models we use \(V: AP\to 2^{M}\) to denote the evaluation function. For a relation, \(\mathrel{\triangleleft}\), let \(\mathrel{\triangleleft}^{-1} = \{ (y,x) : (x, y) \in~\mathrel{\triangleleft}\}\). For \(x \in M\), let \(\mathrel{\triangleleft}(x) = \{y \in M: x\mathrel{\triangleleft}y\}\); and for \(S \subseteq M\), let \(\mathrel{\triangleleft}(S) = \bigcup_{x \in S} \mathrel{\triangleleft}(x)\). We use the standard grammar of modal logic and entailment for a model (\(\langle M, \mathrel{\triangleleft}, V \rangle\if\relax\detokenize{x}\relax\else,\fi x \models \phi\)).
We denote the Necessitation rule (\(\frac{A}{\square A}\)) as (Nec) and we have the modal formula \(K := \square(A \rightarrow B) \rightarrow (\square A \rightarrow \square B)\) that holds in all frames. Other common modal formula are defined along with their corresponding properties of frames: \[\begin{align} a4 := \lozenge\lozenge A \rightarrow \lozenge A,~\text{transitivity}; && aT := A \rightarrow \lozenge A,~\text{reflexivity}; \\ aD := \lozenge\top,~\text{seriality}; && ad := \lozenge A \rightarrow \lozenge\lozenge A,~\text{density}; \\ ad_2 := \lozenge A \land \lozenge B \rightarrow \lozenge(\lozenge A \land \lozenge B),~\text{2-density}; && a2 := \lozenge\square A \rightarrow \square\lozenge A,~\text{confluence.\footnotemark} \end{align}\]
The smallest modal logic is \(\mathbf{K}\), which contains the standard propositional logic axioms, modus ponens, \(K\), and (Nec). A normal modal logic is the smallest modal logic that consists of \(\mathbf{K}\); any extra (valid) formulae \(a_1, a_2 \dots\); and any formula that can be obtained from applying the rules in \(\mathbf{K}\) on the formulae given. The respective logic is denoted \(\mathbf{K}+ a_1 + a_2 +\dots\) .
We denote some normal modal logics derived from the formulas given above: \[\begin{align} & \mathbf{K4} := \mathbf{K}+ a4, & \mathbf{T} := \mathbf{K}+ aT, \\ & \mathbf{D4} := \mathbf{K4}+ aD, & \mathbf{S4} := \mathbf{K4} + aT, \\ & \mathbf{OI} := \mathbf{D4} + ad_2, & \boldsymbol{\Lambda.2} := \boldsymbol{\Lambda} + a2; \end{align}\] where \(\boldsymbol{\Lambda}\) is an arbitrary normal modal logic. Each of these has a combination of the properties of the corresponding modal formula.
As standard, for a set of formulae, \(\Gamma\), and a formula, \(\phi\), let \(\Gamma \vdash \phi\) mean that \(\phi\) can be logically derived from \(\Gamma\) (\(\phi \in \mathbf{K}+ \Gamma\)) and \(\Gamma \nvdash \phi\) iff \(\Gamma \vdash \lnot \phi\). For a frame, \(F = \langle M, \mathrel{\triangleleft} \rangle\), we write \(\mathcal{L}(F)\) to mean the set of formula that are satisfied under all possible evaluations of \(F\). This set of formula could be some logic, \(\boldsymbol{\Lambda}\), and we may write \(\mathcal{L}(F) = \boldsymbol{\Lambda}\).
We introduce Gabbay’s Irreflexive Rule [@Gabbay1981]. The rule is
For a normal modal logic \(\boldsymbol{\Lambda}\) without reflexivity (\(aT\)), let \(\boldsymbol{\Lambda} + \text{(Gabb)}\) be the smallest modal logic of \(\boldsymbol{\Lambda}\) with the addition of being closed under \(\text{(Gabb)}\). A frame whose logic is \(\boldsymbol{\Lambda} + \text{(Gabb)}\) is irreflexive.
4 Spacetime and Modal Logic↩︎
We begin by looking at modal logic within the context of a generic spacetime. No assumptions are made on where the spacetime lies on the causal ladder. We analyse the normal modal logics that act as a subset for the modal logic of spacetimes.
Given the definitions of the various causal relations, the relational properties they have (known from Lemma [lem:relcommonproperties]), and the properties on frames that normal modal logics describe; we have the following results on all spacetimes.
Corollary 1. Let \(M\) be a spacetime. Then, we have that
\(\mathbf{S4} \subseteq \mathcal{L}(\langle M, \mathrel{\underline{\ll}} \rangle), \mathcal{L}(\langle M, \preccurlyeq \rangle)\);
\(\mathbf{OI} \subseteq \mathcal{L}(\langle M, \ll \rangle)\);
\(\mathbf{D4} + ad \subseteq \mathcal{L}(\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle)\).
This can be seen simply from the fact that the normal modal logics yield frames that have the associated properties and the causal relations have those properties. For instance, \(\mathbf{S4}\) yields frames that are transitive and reflexive, and \(\preccurlyeq\) is a transitive and reflexive relation.
4.1 The After Formula↩︎
In [@Shapirovsky2005], it was shown that the formula, which we refer to as the after formula, \[a \scalebox{0.85}{\alpha}f:= \lozenge( \lozenge(p_1 \land \lnot p_2 \land \square\lnot p_2) \land \lozenge(p_2 \land \lnot p_1 \land \square\lnot p_1)) \land \lozenge q \rightarrow \lozenge(\lozenge p_1 \land \lozenge q) \lor \lozenge(\lozenge p_2 \land \lozenge q),\] holds in the modal logic of any \(1+n\)-dimensional Minkowski spacetime with the \(\mathrel{\scalebox{0.85}{\alpha}}\) relation. This formula corresponds to the first-order property: \[\label{eq:afterformula:firstorder} \begin{align} \forall x, y, y_1, y_2, z &\Big[ \left(x \mathrel{\triangleleft}y \land y \mathrel{\triangleleft}y_1 \land y \mathrel{\triangleleft}y_2 \land x \mathrel{\triangleleft}z \land y_1 \neq y_2 \land \lnot(y_1 \mathrel{\triangleleft}y_2) \land \lnot(y_2 \mathrel{\triangleleft}y_1) \right) \\ &\rightarrow \exists t \left(x \mathrel{\triangleleft}t \land t \mathrel{\triangleleft}z \land (t \mathrel{\triangleleft}y_1 \lor t \mathrel{\triangleleft}y_2 ) \right) \Big]. \footnotemark \end{align}\tag{1}\] Observe that \(a \scalebox{0.85}{\alpha}f\) is a modified version of 3-density: if two (unrelated) points are related by a common point from the root and there is a third point that can be reached from the root, then at least one of the two points and the third point must share a common point from the root. In fact, \(a \scalebox{0.85}{\alpha}f\) is a Sahlqvist formula (see [@Blackburn2001]), which provides properties such as canonicity, first-order correspondence (as already demonstrated in Equation 1 ), etc.
We make the following observation of \(a \scalebox{0.85}{\alpha}f\) within the scope of normal modal logics:
Lemma 3. We have
\(\mathbf{D4.2} + ad \nvdash a \scalebox{0.85}{\alpha}f\);
\(\mathbf{T} \nvdash a \scalebox{0.85}{\alpha}f\);
\(\mathbf{K4} + ad_2 \vdash a \scalebox{0.85}{\alpha}f\).
Proof.
Claims [lem:aaf:d4462d] and [lem:aaf:t] are proven by models that act as counterexamples given in Figures [fig:afnotin:d4d] and [fig:afnotin:T] respectively.
For [lem:aaf:k4d2], let \(\mathcal{M} = \langle M, \mathrel{\triangleleft}, V \rangle\) be a \(\mathbf{K4} + ad_2\) model and let \(x \in M\). If we have that \[\mathcal{M}\if\relax\detokenize{x}\relax\else,\fi x \models \lozenge( \lozenge(p_1 \land \lnot p_2 \land \square\lnot p_2) \land \lozenge(p_2 \land \lnot p_1 \land \square\lnot p_1)) \land \lozenge q;\] then \(\mathcal{M}\if\relax\detokenize{x}\relax\else,\fi x \models \lozenge p_1\) (by transitivity and properties of \(\land\)). Since we have \(\mathcal{M}\if\relax\detokenize{x}\relax\else,\fi x \models \lozenge p_1 \land \lozenge q\), then by 2-density we must have that \(\mathcal{M}\if\relax\detokenize{x}\relax\else,\fi x \models \lozenge(\lozenge p_1 \land \lozenge q)\) and therefore \(\mathcal{M}\if\relax\detokenize{x}\relax\else,\fi x \models a \scalebox{0.85}{\alpha}f\). Since \(x, \mathcal{M}\) are generic, then \(\mathbf{K4} + ad_2 \vdash a \scalebox{0.85}{\alpha}f\). ◻
Note that reflexivity implies 2-density. Additionally, since \(\mathbf{D4.2} + ad \nvdash a \scalebox{0.85}{\alpha}f\), then any sub-logics of \(\mathbf{D4.2} + ad\) (\(\mathbf{D4}\), \(\mathbf{K4}\), …) do not contain \(a \scalebox{0.85}{\alpha}f\). Conversely, any logics that contain \(\mathbf{K4} + ad_2\) as a sub-logic, such as \(\mathbf{S4}\), contain \(a \scalebox{0.85}{\alpha}f\). Therefore, since \(a \scalebox{0.85}{\alpha}f\) holds in transitive and 2-dense (or reflexive) frames, then it holds in frames that use a spacetime and one of \(\ll\), \(\mathrel{\underline{\ll}}\) or \(\preccurlyeq\).
Let \(\mathbf{D4da}:= \mathbf{D4} + ad + a \scalebox{0.85}{\alpha}f\).2 Since \(ad\) and \(a \scalebox{0.85}{\alpha}f\) are Sahlqvist formula, then by the Sahlqvist Theorem [@Blackburn2001] canonicty is achieved for the formulas and \(\mathbf{D4da}\).
Corollary 2. The logic \(\mathbf{D4da}\) is canonical.
4.2 Geodesic Normal Coordinates↩︎
In this section we define and collect some technical results from causality theory that are needed to prove the after formula holds in general spacetimes. We refer to [@landsman2021FoundationsGeneralRelativity] for details.
Given any subset \(A\subseteq M\), we write \(x\ll_A y\) if there exists a fd timelike curve from \(x\) to \(y\) that lies entirely within \(A\). Clearly \(x\ll_A y\) implies \(x\ll y\). Define \(\preccurlyeq_A\) and \(\mathrel{\scalebox{0.85}{\alpha}}_A\) similarly.
A curve \(\gamma\) is called a geodesic if it is length extremising (technically: \(\nabla_{\dot{\gamma}}\dot{\gamma}=0\) with respect to the Levi-Civita connection), which is interpreted as the motion of a non-accelerating, free falling body. For the present work it is important to note that geodesics are locally uniquely determined by their starting position and initial velocity. This ensures the existence of the exponential map: for \(x\in M\) it is the smooth map \(\exp_x\colon \mathcal{V}_x\subseteq T_xM\to M\) defined on a suitable open neighbourhood \(\mathcal{V}_x\) of \(0\) by \(\exp_x(v):=\gamma_v(1)\), where \(\gamma_v\) is the unique geodesic with \(\gamma_v(0)=x\) and \(\dot{\gamma}_v(0)=v\). The region \(\mathcal{V}_x\) can be shrunk to a convex open neighbourhood of \(0\) such that \(\exp_x\) becomes a diffeomorphism onto its image \(\exp_x(\mathcal{U}_x)=U_x\), which is called a (convex) normal neighbourhood of \(x\). This diffeomorphism facilitates what is known as geodesic normal coordinates. Under these coordinates, geodesics within the neighbourhood \(U_x\) emanating from \(x\) correspond precisely to straight line segments in \(T_xM\) through the origin.
Theorem 2. Every \(x\in M\) admits an open convex normal neighbourhood \(U_x\subseteq M\) together with a diffeomorphism \({\Phi:=\exp_x^{-1}\colon U_x\to \mathcal{U}_x}\) onto an open convex neighbourhood \(\mathcal{U}_x\) of the origin in Minkowski space, such that \(\Phi(x)=0\), affinely parametrised geodesics \(\gamma\) in \(U_x\) with \(\gamma(0)=x\) are transformed into straight lines as \(\Phi\circ \gamma (t)= t\dot{\gamma}(0)\), and for every \(y\in U_x\) we have: \[\label{eq:local32relations} x \ll_{U_x} y \iff 0 \ll\Phi(y), \qquad x \preccurlyeq_{U_x} y \iff 0 \preccurlyeq\Phi(y), \qquad x \mathrel{\scalebox{0.85}{\alpha}}_{U_x} y \iff 0 \mathrel{\scalebox{0.85}{\alpha}}\Phi(y).\qquad{(2)}\]
Proof. See [@landsman2021FoundationsGeneralRelativity] and [@minguzzi2019LorentzianCausalityTheory]. ◻
Of course, the dual of Equation ?? also holds, where \(y\) appears in the past of \(x\). Note however that \(\Phi\) does not preserve the causal relations between arbitrary points in \(U_x\): only to and from the basepoint \(x\).
4.3 After Formula in Spacetime↩︎
As mentioned previously, it was shown in [@Shapirovsky2005] that the after formula is satisfied in the after modality of any Minkowski space.
Consider \(1+n\)-dimensional Minkowski space \(\mathbb{R}^{1+n}\) with its after relation \(\mathrel{\scalebox{0.85}{\alpha}}\). Then \[\langle \mathbb{R}^{1+n}, \mathrel{\scalebox{0.85}{\alpha}} \rangle\if\relax\detokenize{}\relax\else,\fi \models a\scalebox{0.85}{\alpha}f.\]
Now we generalise this result, showing that \(a \scalebox{0.85}{\alpha}f\) holds in any spacetime. The main technical step towards proving this is to show the following property: if \(x\mathrel{\scalebox{0.85}{\alpha}}y \mathrel{\scalebox{0.85}{\alpha}}y_1,y_2\) and \(y_1\neq y_2\) are spacelike separated, then \(x\ll y_i\) for some \(i\). First we give an elementary proof in Minkowski space (Lemma 4 and Corollary 3), which is then lifted to arbitrary spacetimes using geodesic normal coordinates (Theorem 2). The key intuition is that in the extreme scenario that \(x\mathrel{\scalebox{0.85}{\alpha}}y\mathrel{\scalebox{0.85}{\alpha}}y_j\) represents a lightline, the fact that \(y_i\) is spacelike separated from \(y_j\) means that it must necessarily move away from this lightline, and so must be in the interior cone of \(x\). This behaviour lifts from Minkowski space to general spacetimes.
4.4 Proof of Theorem 4↩︎
As mentioned in Section 4.3, the main technical step is to prove: if \(x\mathrel{\scalebox{0.85}{\alpha}}y \mathrel{\scalebox{0.85}{\alpha}}y_1,y_2\) and \(y_1\neq y_2\) are spacelike separated, then \(x\ll y_i\) for some \(i\). We first do this in Minkowski space.
Lemma 4. In Minkowski space, let \(x\rightarrow y \rightarrow y_1,y_2\) and \(x\rightarrow y_1,y_2\). Then \(y_1\rightarrow y_2\) or \(y_2\rightarrow y_1\).
Proof. Take some arbitrary \(z\) in the intersection of the lightcones of \(x\) and \(y\). Then we get from Equation ?? that \(\left\lVert\vec{z}-\vec{x}\right\rVert= z^0- x^0\) and \(\left\lVert\vec{z}-\vec{y}\right\rVert=z^0-y^0\), and hence \[\left\lVert\vec{z}-\vec{x}\right\rVert-\left\lVert\vec{z}-\vec{y}\right\rVert = y^0 -x^0 = \left\lVert\vec{y}-\vec{x}\right\rVert.\] This shows that equality is attained in the triangle inequality: \[\left\lVert\vec{z}-\vec{x}\right\rVert \leq \left\lVert\vec{z}-\vec{y}\right\rVert + \left\lVert\vec{y}-\vec{x}\right\rVert,\] which occurs precisely when there exists a scalar \(\lambda\geq 0\) with \(\vec{z}-\vec{y}=\lambda(\vec{y}-\vec{x})\). In particular, for our situation, we get \(\lambda_1,\lambda_2\geq 0\) with \(\vec{y_i} = \vec{y}+ \lambda_i(\vec{y}-\vec{x})\). Note now by \(y\rightarrow y_i\) that \[y_i^0 = y^0 + \left\lVert\vec{y_i}-\vec{y}\right\rVert = y^0 + \lambda_i\left\lVert\vec{y}-\vec{x}\right\rVert = y^0 + \lambda_i(y^0-x^0),\] so in particular \(y_2^0 - y_1^0 = (\lambda_2-\lambda_1)(y^0-x^0)\). Similarly note \(\vec{y_2}-\vec{y_1} = (\lambda_2-\lambda_1)(\vec{y}-\vec{x})\), and so we get \[\left\lVert\vec{y_2}-\vec{y_1}\right\rVert = |\lambda_2-\lambda_1|\left\lVert\vec{y}-\vec{x}\right\rVert = |\lambda_2-\lambda_1|(y^0-x^0) = |y_2^0 - y_1^0|,\] which is precisely what it means for \(y_1\rightarrow y_2\) or \(y_2\rightarrow y_1\) to hold. ◻
Corollary 3. In Minkowski space, if \(x\mathrel{\scalebox{0.85}{\alpha}}y\mathrel{\scalebox{0.85}{\alpha}}y_1,y_2\) and \(y_1\neq y_2\) are spacelike separated, then \({x\ll y_i}\) for some \(i\).
Proof. Transitivity implies \(x\mathrel{\scalebox{0.85}{\alpha}}y_1,y_2\). So either \(x\ll y_i\) for some \(i\), in which case we are done, or \(x\rightarrow y_1,y_2\). Moreover, if \(x\ll y\) or \(y\ll y_i\) for some \(i\) we get the desired relation via the push-up rule. We are therefore left to consider the case that \(x\rightarrow y\rightarrow y_1,y_2\). However, by Lemma 4, this would imply \(y_1\rightarrow y_2\) or \(y_2\rightarrow y_1\), contradicting that \(y_1\) and \(y_2\) are spacelike separated. ◻
The next few lemmas generalise this result to arbitrary spacetimes. We need some more definitions. A subset \(A\subseteq M\) is called achronal if \(I^{+}(A)\cap A=\varnothing\), and a curve \(\gamma\) is called achronal if \(\mathop{\mathrm{im}}(\gamma)\) is achronal, where we recall for \(\gamma\colon I\to M\) that \(\mathop{\mathrm{im}}(\gamma)=\{\gamma(t):t\in I\}\). Explicitly, this means there are no times \(s,t\) so that \(\gamma(s)\ll\gamma(t)\). A geodesic from \(p\) to \(q\) is called maximising if it has greater or equal length than every other causal curve from \(p\) to \(q\). We then have the powerful result [@minguzzi2019LorentzianCausalityTheory], saying achronal lightlike geodesics are precisely the maximising lightlike ones.
Theorem 3. Let \(\gamma\) be a causal curve connecting \(p\) to \(q\neq p\). Either: there is a timelike curve \(\sigma\) from \(p\) to \(q\) whose length is strictly greater than that of \(\gamma\); or \(\gamma\) is a maximising geodesic (up to parametrisation). In particular, if there are no timelike curves connecting \(p\) to \(q\) then \(\gamma\) is an achronal lightlike geodesic (up to parametrisation).
Lemma 5. Let \(U\subseteq M\) be open, and take \(p,q\in U\). If there exists a causal curve \(\gamma\) in \(U\) from \(p\) to \(q\neq p\) that is not an achronal lightlike geodesic, then \(p\ll_U q\).
Proof. Consider the spacetime \((U,g|_U)\). Applying Theorem 3 to the given curve \(\gamma\) in \(U\) from \(p\) to \(q\neq p\), either we get a timelike curve \(\sigma\) facilitating \(p\ll_U q\), in which case we are done, or \(\gamma\) is a maximising geodesic. If \(\gamma\) is itself timelike we are also done, but if \(\gamma\) is a maximising lightlike geodesic then it is achronal, contradicting the hypothesis. ◻
Lemma 6. Let \(x\in M\), and take geodesic normal coordinates \(\Phi\colon U_x\to \mathcal{U}_x\) from Theorem 2. Suppose \(p,q\in U_x\) satisfy \({p\mathrel{\scalebox{0.85}{\alpha}}_{U_x} x \mathrel{\scalebox{0.85}{\alpha}}_{U_x} q}\). If \(\Phi(p)\ll\Phi(q)\) in Minkowski space, then \(p\ll_{U_x} q\).
Proof. If \(p\ll_{U_x} x\) or \(x\ll_{U_x} q\) then the desired result follows from the push-up rule. Suppose therefore that \(p\rightarrow_{U_x} x\) and \(x\rightarrow_{U_x} q\). Let \(\scalebox{0.85}{\alpha}\) and \(\beta\) be the curves facilitating these relations, and let \(\gamma\) be their concatenation. We claim that \(\gamma\) is not a lightlike geodesic, so in particular not an achronal lightlike geodesic. From that, the desired \(p\ll_{U_x}q\) will follow by Lemma 5.
Suppose for the sake of contradiction that \(\gamma\) is a lightlike geodesic, affinely parametrised and so that \({\gamma(0)=x}\). Then the curve \(\Phi\circ \gamma\) is the straight line passing through the origin with velocity \(\dot{\gamma}(0)\), which immediately gives \(\Phi(p)\rightarrow\Phi(q)\), a contradiction to \(\Phi(p)\ll\Phi(q)\). ◻
In any spacetime, if \(x\mathrel{\scalebox{0.85}{\alpha}}y \mathrel{\scalebox{0.85}{\alpha}}y_1,y_2\) and \(y_1\neq y_2\) are spacelike separated, then \(x\ll y_i\) for some \(i\).
Proof. Let \(\gamma,\delta_1,\delta_2\) denote the causal curves corresponding to \(x\mathrel{\scalebox{0.85}{\alpha}}y\) and \(y\mathrel{\scalebox{0.85}{\alpha}}y_1,y_2\), respectively. Without loss of generality, suppose that \(\delta_i\) are parametrised on the unit interval \([0,1]\to M\). Consider the set \({S= \delta_1^{-1}(\mathop{\mathrm{im}}(\delta_2))}\), which is nonempty since \(\delta_1(0)=\delta_2(0)\) and a strict subset of \([0,1]\) because \({y_1\neq y_2}\) are spacelike separated. Since \([0,1]\) is compact and \(\delta_2\) is continuous, \(\mathop{\mathrm{im}}(\delta_2)\) is compact in \(M\). Since \(M\) is Hausdorff, \(\mathop{\mathrm{im}}(\delta_2)\) is thus closed, and by continuity of \(\delta_1\) the preimage \(S\) is closed. Hence \(S\) has a maximum element \(t_0\), the latest time at which \(\delta_1\) overlaps \(\delta_2\). We can further reparametrise \(\delta_2\) without loss of generality such that \(\delta_1(t_0)=\delta_2(t_0)\), and hence \(\delta_1\) and \(\delta_2\) never intersect after \(t_0\). Let \({y':= \delta_1(t_0)=\delta_2(t_0)}\) be the last intersection point; see the left diagram in Figure 5. Note if \(t_0=0\) then \(y'= y\).
Using Theorem 2, choose a convex normal neighbourhood \(U_{y'}\subseteq M\) and geodesic normal coordinates \(\Phi\colon U_{y'}\to \mathcal{U}_{y'}\). Since \(U_{y'}\) is open and \(\delta_i\) are continuous with \(\delta_i(t_0)=y'\), we can find time intervals \(\epsilon_i>0\) such that \(t_0+\epsilon_i\leq 1\) and on \([t_0,t_0+\epsilon_i]\) the curves \(\delta_i\) stay in \(U_{y'}\). For any \({t\in (t_0,t_0+\epsilon_i]}\) we then get that \(y'\mathrel{\scalebox{0.85}{\alpha}}_{U_{y'}} \delta_i(t)\), and by ?? we have \(0\mathrel{\scalebox{0.85}{\alpha}}\Phi\circ \delta_i(t)\) in \(\mathcal{U}_{y'}\). From this it follows that \({\delta_i(t) \neq y'}\) for every \(t\in (t_0,t_0+\epsilon_i]\), otherwise \(y'\mathrel{\scalebox{0.85}{\alpha}}_{U_{y'}} y'\) and hence \(0\mathrel{\scalebox{0.85}{\alpha}}0\), which is impossible in Minkowski space. Using this, we see from Equation ?? that the time coordinate \({(\Phi\circ \delta_i(t))^0}\) must be strictly greater than zero for all \({t\in (t_0,t_0+\epsilon_i]}\). In particular there exists some \(\epsilon >0\) that is below the endpoints: \({\epsilon < (\Phi\circ \delta_i(t_0+\epsilon_i))^0}\), meaning that eventually the curves \(\Phi\circ \delta_i\) are above the hyperplane \({\{ x\in \mathbb{R}^{1+n}: x^0= \epsilon\}}\). By the intermediate value theorem there exists \({t_i\in (t_0,t_0+\epsilon_i]}\) so that the curves are precisely on the hyperplane: \((\Phi\circ\delta_i(t_i))^0 = \epsilon\). Using this, define the distinct points \(p_i:=\delta_i(t_i)\), from which we get the distinct points \(z_i:=\Phi(p_i)\) on the hypersurface, meaning that \(z_1\neq z_2\) are spacelike separated.
We similarly pick a point \(p\) in the past of \(y'\). If \(t_0>0\), find some \(\epsilon_0>0\) so that \(\delta_1\) remains within \(U_{y'}\) on the interval \([t_0-\epsilon_0,t_0]\), and define \(p:= \delta_1(t_0-\epsilon_0)\) and \(z:=\Phi(p)\); see the right diagram in Figure 5. In the case that \(t_0=0\), so \(y'=y\), pick \(p\) analogously but on the curve \(\gamma\) instead.
In total, we have the situation in the normal neighbourhood \(U_{y'}\) that \(p\mathrel{\scalebox{0.85}{\alpha}}_{U_{y'}} y' \mathrel{\scalebox{0.85}{\alpha}}_{U_{y'}} p_1,p_2\). Using ?? and its dual, we get the situation in the region \(\mathcal{U}_{y'}\) of Minkowski space that \(z\mathrel{\scalebox{0.85}{\alpha}}0 \mathrel{\scalebox{0.85}{\alpha}}z_1,z_2\) where \(z_1\neq z_2\) are spacelike separated, so by Corollary 3 we get \(z\ll z_k\) for some \(k\). Applying Lemma 6 we hence get \(p\ll_{U_{y'}} p_k\).
Finally, by construction we have \(x\mathrel{\scalebox{0.85}{\alpha}}p\) and \(p_i\mathrel{\scalebox{0.85}{\alpha}}y_i\), so globally \(x\mathrel{\scalebox{0.85}{\alpha}}p \ll p_k \mathrel{\scalebox{0.85}{\alpha}}y_k\), and the desired result follows by the push-up rule: \(x\ll y_k\). ◻
Note that the proof (given in Appendix [apx:lemma:unique32lightlines32in32any32spacetime]) still works if \(x=y\), in which case from \(x\mathrel{\scalebox{0.85}{\alpha}}x\) we get a causal curve from \(x\) to itself, which is all that is needed for the proof. A visualisation of the proof of Lemma [lemma:unique32lightlines32in32any32spacetime] is in Figure 5.
![Figure 5: Visualisation of the proof for Lemma [lemma:unique32lightlines32in32any32spacetime] using two-dimensional Minkowski spacetime. Dashed (solid) lines represent chronological (causal) curves. The dotted region on the left denotes U_{y'}, and the dotted line on the right depicts the spacelike hypersurface defined by x^0=\epsilon.](/article/2606.31927/_pdflatex/taquybds.png "fig:")
Theorem 4. Let \(M\) be a spacetime and \(\mathrel{\scalebox{0.85}{\alpha}}\) its after relation. Then \[\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle\if\relax\detokenize{}\relax\else,\fi \models a\scalebox{0.85}{\alpha}f.\]
Proof. Take \(x, y, y_1, y_2, z \in M\) such that \(x \mathrel{\scalebox{0.85}{\alpha}}y, y_1, y_2, z\) and \(y \mathrel{\scalebox{0.85}{\alpha}}y_1, y_2\), where \(y_1 \neq y_2\) are unrelated by \(\mathrel{\scalebox{0.85}{\alpha}}\). This implies \(y_1\) and \(y_2\) are spacelike separated. We need to find \(t\in M\) such that \(x\mathrel{\scalebox{0.85}{\alpha}}t \mathrel{\scalebox{0.85}{\alpha}}y_i, z\), for some \(i\). First, by Lemma [lemma:unique32lightlines32in32any32spacetime] we can assume without loss of generality that \(x\ll y_1\). In the case \(x=z\) the result is trivial (pick \(t=x\)), so assume \(x\neq z\). Thus we have a case distinction of whether \(x\ll z\) or \(x\rightarrow z\) (Lemma 1). In the first case, the existence of \(t\in M\setminus \{x\}\) with \(x\ll t\ll y_1,z\) follows immediately from 2-density of \(\ll\).
Instead, suppose that \(x \rightarrow z\). Let \(\gamma\) be the timelike curve connecting \(x\ll y_1\) and let \(\delta\) be the lightcurve connecting \(x\rightarrow z\). Take a point \(p\in \mathop{\mathrm{im}}(\gamma)\setminus\{x\}\) so that \(x\ll p\ll y_1\). Then \(x\in I^{-}(p)\), and since chronological cones are open there must exist a point \(t\in I^{-}(p)\cap \mathop{\mathrm{im}}(\delta)\setminus\{x\}\), which hence satisfies \(x\mathrel{\scalebox{0.85}{\alpha}}t \mathrel{\scalebox{0.85}{\alpha}}y_1\) and \(x \mathrel{\scalebox{0.85}{\alpha}}t \mathrel{\scalebox{0.85}{\alpha}}z\), as desired. ◻
Finally, we build on Corollary 1 using Theorem 4 and Lemma 3.
Corollary 4. For any spacetime \(M\) we have that \(\mathbf{D4da}\subseteq \mathcal{L}(\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle)\).
What this section shows is that there is a connection between the push-up rule, which naturally occurs in spacetimes, and \(a \scalebox{0.85}{\alpha}f\). Many of the proofs that we have used for \(a \scalebox{0.85}{\alpha}f\) are reliant on the push-up rule. An exploration of the push-up rule and its link to Kripke frames (possibly with multiple relations) is warranted, but left to future work.
5 Two-dimensional Spacetimes↩︎
It remains an open problem as to what the modal logic of Minkowski spacetime with \(\mathrel{\scalebox{0.85}{\alpha}}\) is, but it is known that the logic of two-dimensional Minkowski spacetime is unique to any \(1+n\)-dimensional Minkowski spacetime (\(n > 2\)) [@Shapirovsky2005].
5.1 After Formula for Two Dimensions↩︎
Consider the formula, \[a \scalebox{0.85}{\alpha}_2 f:= \lozenge(p_1 \land \lnot p_2 \land \square\lnot p_2) \land \lozenge(p_2 \land \lnot p_1 \land \square\lnot p_1) \land \lozenge q \rightarrow \lozenge(\lozenge p_1 \land \lozenge q) \lor \lozenge(\lozenge p_2 \land \lozenge q),\] which is \(a \scalebox{0.85}{\alpha}f\) without the first diamond.3 It corresponds to the following first order property: \[\begin{align} \forall x, y_1, y_2, z & \Big[ [x \mathrel{\triangleleft}y_1 \land x \mathrel{\triangleleft}y_2 \land x \mathrel{\triangleleft}z \land y_1 \neq y_2 \land \lnot(y_1 \mathrel{\triangleleft}y_2) \land \lnot(y_2 \mathrel{\triangleleft}y_1) ] \\ & \quad \to \exists t (x \mathrel{\triangleleft}t \land t \mathrel{\triangleleft}z \land (t \mathrel{\triangleleft}y_1 \lor t \mathrel{\triangleleft}y_2 )) \Big]. \end{align}\] This formula is a Sahlqvist formula and, therefore, any canonical normal modal logic that adds \(a \scalebox{0.85}{\alpha}_2 f\) is canonical. Even though \(a \scalebox{0.85}{\alpha}_2 f\) is a simple modification to \(a \scalebox{0.85}{\alpha}f\), we can show that it is strictly more expressive within the context of spacetimes.
Theorem 5. We have that
\(\mathbf{K4} + a \scalebox{0.85}{\alpha}_2 f\vdash a \scalebox{0.85}{\alpha}f\);
\(\mathbf{D4da}\nvdash a \scalebox{0.85}{\alpha}_2 f\).
Proof. [thm:aftertwoexpress:expressive]: Let \(\mathcal{M} = \langle M, \mathrel{\triangleleft}, V \rangle\) be a \(\mathbf{K4} + a \scalebox{0.85}{\alpha}_2 f\) model and \(x \in M\). Assume that \(\mathcal{M}\if\relax\detokenize{x}\relax\else,\fi x \models \lozenge(\lozenge(p_1 \land \lnot p_2 \land \lnot \square p_2) \land \lozenge(p_2 \land \lnot p_1 \land \lnot \square p_1)) \land \lozenge q\). Let \(x \mathrel{\triangleleft}y\) such that \(\mathcal{M}\if\relax\detokenize{y}\relax\else,\fi y \models \lozenge(p_1 \land \lnot p_2 \land \lnot \square p_2) \land \lozenge(p_2 \land \lnot p_1 \land \lnot \square p_1)\), then \(\mathcal{M}\if\relax\detokenize{x}\relax\else,\fi x \models \lozenge\lozenge(p_1 \land \lnot p_2 \land \lnot \square p_2) \land \lozenge\lozenge(p_2 \land \lnot p_1 \land \lnot \square p_1)\).
Since \(\mathcal{M}\) is transitive, then we have \(\mathcal{M}\if\relax\detokenize{x}\relax\else,\fi x \models \lozenge(p_1 \land \lnot p_2 \land \lnot \square p_2) \land \lozenge(p_2 \land \lnot p_1 \land \lnot \square p_1) \land \lozenge q\). As \(\mathcal{M}\) is a \(a \scalebox{0.85}{\alpha}_2 f\) model, we have \(\mathcal{M}\if\relax\detokenize{x}\relax\else,\fi x \models \lozenge(\lozenge p_1 \land \lozenge q) \lor \lozenge(\lozenge p_2 \land \lozenge q)\) and therefore \(\mathcal{M}\if\relax\detokenize{x}\relax\else,\fi x \models a \scalebox{0.85}{\alpha}f\). Because \(x\) and \(\mathcal{M}\) are general, then \(\mathbf{K4} + a \scalebox{0.85}{\alpha}_2 f\vdash a \scalebox{0.85}{\alpha}f\).
[thm:aftertwoexpress:inexpressive]: A counterexample is provided by the finite model given in Figure [fig:aftertwoexpress]. The frame has all the properties of \(\mathbf{D4da}\), but cannot express \(a \scalebox{0.85}{\alpha}_2 f\). One of the points \(p_1\) or \(p_2\) must share a common point with \(q\) after the root but they do not. ◻
For finite (spacetime) frames, \(a \scalebox{0.85}{\alpha}_2 f\) says that if there are successor clusters from an irreflexive point, there are at most two of them each possibly with their own unique chains of clusters (light lines).
5.2 Separability of Two-Dimensional Spacetimes↩︎
With the after relation, we can see that \(a \scalebox{0.85}{\alpha}_2 f\) holds in two-dimensional Minkowski spacetime but does not hold in any other \(1+n\)-dimensional Minkowski spacetime.
Lemma 7. Let \(M = \mathbb{R}^{1+n}\) and \(\mathrel{\scalebox{0.85}{\alpha}}\) be the after relation on Minkowski spacetime. We have that
\(\langle \mathbb{R}^2, \mathrel{\scalebox{0.85}{\alpha}} \rangle\if\relax\detokenize{}\relax\else,\fi \models a \scalebox{0.85}{\alpha}_2 f\)
\(\langle \mathbb{R}^{1+n}, \mathrel{\scalebox{0.85}{\alpha}} \rangle\if\relax\detokenize{}\relax\else,\fi \not\models a \scalebox{0.85}{\alpha}_2 f\) for \(n \geq 2\)
Proof. The argument is similar to [@Shapirovsky2005]. ◻
It turns out that \(a \scalebox{0.85}{\alpha}_2 f\) holds in any two-dimensional spacetime.
Let \(M\) be a two-dimensional spacetime. Then, \[\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle\if\relax\detokenize{}\relax\else,\fi \models a \scalebox{0.85}{\alpha}_2 f.\]
Proof. Let \(x \mathrel{\scalebox{0.85}{\alpha}}y_1, y_2, z\) with \(y_1 \neq y_2\) and \(y_i \not\mathrel{\scalebox{0.85}{\alpha}}y_j\). We need to prove there exists \(t\in M\) such that \(x\mathrel{\scalebox{0.85}{\alpha}}t\mathrel{\scalebox{0.85}{\alpha}}z, y_i\) for some \(i\). Again, in the case that \(x=y_i\) or \(x=z\) simply take \(t=x\). Thus assume all points are distinct from \(x\), so \(\mathrel{\scalebox{0.85}{\alpha}}\) is described via Lemma 1.
If \(x \ll y_i\) for some \(i\) and \(x \ll z\), then by 2-density of \(\ll\) we are done.
Suppose now that \(x \rightarrow y_1, y_2, z\), and let \(\delta_1,\delta_2,\gamma\) be the corresponding causal curves. Since \(x\rightarrow y_i\), there are no timelike curves from \(x\) to \(y_i\), and hence by Theorem 3 each \(\delta_i\) is an achronal lightlike geodesic (up to reparametrisation). Similarly, since \(x\rightarrow z\), the curve \(\gamma\) is an achronal lightlike geodesic from \(x\) to \(z\).
Choose a convex normal neighbourhood \(U_x\) of \(x\), and consider the restrictions of \(\delta_1,\delta_2,\gamma\) to \(U_x\). In a two-dimensional spacetime there are exactly two future-directed lightlike velocities at \(x\), and hence exactly two future-directed lightlike geodesics emanating from \(x\) in \(U_x\). Moreover, since \(y_1\) and \(y_2\) are spacelike separated, the geodesics \(\delta_1\) and \(\delta_2\) cannot coincide, and so the velocities of \(\delta_1\) and \(\delta_2\) at \(x\) correspond to the two distinct lightlike directions in \(T_xM\). Since \(\gamma\) is also lightlike, its velocity at \(x\) must therefore be equal to that of, say, \(\delta_1\). Pick a point \(t\in \mathop{\mathrm{im}}(\gamma)\cap \mathop{\mathrm{im}}(\delta_1)\cap U_x\setminus\{x\}\) sufficiently close to \(x\) so that \(t\) lies on the subcurves from \(x\) to \(z\) and from \(x\) to \(y_1\), so that \(x\mathrel{\scalebox{0.85}{\alpha}}t\mathrel{\scalebox{0.85}{\alpha}}y_1,z\), as desired.
Finally, consider the scenario \(x \rightarrow y_1, y_2\) and \(x \ll z\). Let \(\delta_1,\delta_2\) be the achronal lightlike geodesics from \(x\) to \(y_1,y_2\) (as above), and let \(\gamma\) be a timelike curve from \(x\) to \(z\). Pick a point \({z'\in \mathop{\mathrm{im}}(\gamma)\setminus\{x,z\}}\) sufficiently close to \(x\) so that \(x\ll z'\ll z\). Since \(I^{-}(z')\) is open and contains \(x\), and \(\delta_1\) is continuous with \(\delta_1(0)=x\), there exists \({t\in \mathop{\mathrm{im}}(\delta_1)\setminus\{x\}}\) sufficiently close to \(x\) such that \(t\in I^{-}(z')\). Then \({x\mathrel{\scalebox{0.85}{\alpha}}t\mathrel{\scalebox{0.85}{\alpha}}y_1}\). Moreover \(t\ll z'\) implies \(t\mathrel{\scalebox{0.85}{\alpha}}z'\mathrel{\scalebox{0.85}{\alpha}}z\), hence \(t\mathrel{\scalebox{0.85}{\alpha}}z\). Thus \(x\mathrel{\scalebox{0.85}{\alpha}}t\mathrel{\scalebox{0.85}{\alpha}}y_1,z\), completing the proof. ◻
Denote \(\mathbf{D4da_2}:= \mathbf{D4} + ad + a \scalebox{0.85}{\alpha}_2 f\). It is clear from Theorem 5 that \(\mathbf{D4da}\subset \mathbf{D4da_2}\).
Corollary 5. Let \(M\) be a \(2\)-dimensional spacetime. Then \(\mathbf{D4da_2}\subseteq \mathcal{L}(\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle)\).
In Lemma 7, we were shown how \(a \scalebox{0.85}{\alpha}_2 f\) only holds in two dimensions, providing a separation from \(1+n\)-dimensional Minkowski spacetime. However, to show a full separation of the logics of 2-dimensional spacetimes from higher dimensional ones, it needs to be shown that \(a \scalebox{0.85}{\alpha}_2 f\) does not hold in higher dimensional spacetimes. We note that non-cNTV spacetimes are reflexive in \(\mathrel{\scalebox{0.85}{\alpha}}\), meaning that \(a \scalebox{0.85}{\alpha}_2 f\) holds in those spacetimes. However, for cNTV spacetimes of dimension greater than 3, it is likely that \(a \scalebox{0.85}{\alpha}_2 f\) does not hold. Proving this requires that any high dimensional, cNTV spacetime has at least 3 different light lines from a point irreflexive in \(\mathrel{\scalebox{0.85}{\alpha}}\).
We end this section by forming the following conjecture.
Let \(n \geq 3\). For any cNTV \(n\)-dimensional spacetime, \(M\), we have that \(\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle\if\relax\detokenize{}\relax\else,\fi \not\models a \scalebox{0.85}{\alpha}_2 f\) (\(\mathbf{D4da_2}\nsubseteq \mathcal{L}(\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle)\)).
6 Effects of Causal Ladder Properties on Modal Logics↩︎
We now analyse the modal logic of spacetimes on different levels of the causal ladder. The proofs are fairly obvious throughout, simply relying on the properties of the relevant causal relation.
We have the following obvious result.
Corollary 6. Let \(M\) be a spacetime and \(\ll\) and \(\mathrel{\scalebox{0.85}{\alpha}}\) be the respective causal relations, then:
if \(\ll\) is reflexive, \(\mathbf{S4} \subseteq \mathcal{L}(\langle M, \ll \rangle)\);
if \(\mathrel{\scalebox{0.85}{\alpha}}\) is reflexive, \(\mathbf{S4} \subseteq \mathcal{L}(\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle)\).
6.1 Totally and Non-totally Vicious↩︎
Totally vicious spacetimes are reflexive in \(\ll\) and, consequently, in \(\mathrel{\scalebox{0.85}{\alpha}}\). Note that \(\ll\) and \(\mathrel{\underline{\ll}}\) become indistinguishable from one another (\(x \ll y\) iff \(x \mathrel{\underline{\ll}}y\)), and similarly for \(\mathrel{\scalebox{0.85}{\alpha}}\) and \(\preccurlyeq\). What becomes more apparent is that \(\ll\) and \(\preccurlyeq\) are indistinguishable.
Lemma 8. Let \(M\) be a totally vicious spacetime and \(x, y \in M\). Then \(x \ll y\) iff \(x \preccurlyeq y\).
Proof. If \(x \ll y\), there is a timelike path from \(x\) to \(y\), which is also a causal path. Therefore, \(x \preccurlyeq y\). If \(x \preccurlyeq y\), then we have that \(x \ll y\) since \(y \ll y\) and the push-up rule is used to obtain the result. ◻
This leads to the following result.
Theorem 6. Let \(M\) be a totally vicious spacetime. Then, \[\mathbf{S4} \subseteq \mathcal{L}(\langle M, \ll \rangle) = \mathcal{L}(\langle M, \mathrel{\underline{\ll}} \rangle) = \mathcal{L}(\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle) = \mathcal{L}(\langle M, \preccurlyeq \rangle).\]
For non-totally vicious spacetimes, the logics for \(\ll\) are restricted since reflexivity is lost.
Theorem 7. If \(M\) is a non-totally vicious spacetime, then \(\mathbf{S4} \nsubseteq \mathcal{L}(\langle M, \ll \rangle)\).
Note that \(\mathrel{\scalebox{0.85}{\alpha}}\) and \(\preccurlyeq\) are not affected by a spacetime being NTV (\(\mathrel{\scalebox{0.85}{\alpha}}\) is still reflexive), and therefore their modal logics are not affected either.
Corollary 7. If \(M\) is NTV and not cNTV, then \(\mathbf{S4} \subseteq \mathcal{L}(\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle) = \mathcal{L}(\langle M, \preccurlyeq \rangle)\).
6.2 Chronological↩︎
Irreflexivity of \(\ll\) means that the normal modal logic does not fundamentally change from a non-totally vicious spacetime. However, by considering \(\text{(Gabb)}\), we obtain the following.
Theorem 8. If \(M\) is a chronological spacetime, then \(\mathbf{OI} + \text{(Gabb)}\subseteq \mathcal{L}(\langle M, \ll \rangle)\).
Note how the logic of \(\mathrel{\scalebox{0.85}{\alpha}}\) or the reflexive causal relations have not changed at the levels of non-totally vicious and chronological from a totally vicious spacetime.
6.3 Causally Non-Totally Vicious (cNTV)↩︎
Having introduced the notion of cNTV in Section 2.3, we now see the results of separating the causal condition in the modal logic of \(\mathrel{\scalebox{0.85}{\alpha}}\).
Theorem 9. If \(M\) is a causally non-totally vicious spacetime, then \(\mathbf{S4} \nsubseteq \mathcal{L}(\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle)\).
When considering a spacetime that is both chronological and cNTV, the two respective theorems are used together to reveal that both \(\ll\) and \(\mathrel{\scalebox{0.85}{\alpha}}\) have different modal logics from a NTV spacetime.
6.4 Causal↩︎
A causal spacetime, in a similar way to a chronological spacetime, does not change the normal modal logics of its causal relations, but the logic under \(\mathrel{\scalebox{0.85}{\alpha}}\) can be changed if \(\text{(Gabb)}\) is considered.
Theorem 10. If \(M\) is a causal spacetime, then \(\mathbf{D4da}+ \text{(Gabb)}\subseteq \mathcal{L}(\langle M, \mathrel{\scalebox{0.85}{\alpha}} \rangle)\).
6.5 Distinguishing↩︎
We begin first by extending the notion of a spacetime being distinguishing into the Kripke frame setting.
Definition 4. Let \(F = \langle M, \mathrel{\triangleleft} \rangle\). We say \(F\) is future-distinguishing if for all \(x,y \in M\) whenever \({\mathrel{\triangleleft}}(x) = {\mathrel{\triangleleft}}(y)\), then \(x = y\). We say \(F\) is past-distinguishing if for all \(x,y \in M\) whenever \({\mathrel{\triangleleft}^{-1}}(x) =~{\mathrel{\triangleleft}^{-1}}(y)\), then \(x = y\). Finally, \(F\) is distinguishing if it is both past- and future-distinguishing.
Thus, the spacetime definition of distinguishing is preserved when considering the frame of a spacetime with \(\ll\) (since \(I^{\pm}(x) = {\mathrel{\triangleleft}}^{\pm 1}(x)\)). Our goal is to find some normal modal logic that can capture distinguishing spacetimes. However, despite being able to maintain definitions across domains, it becomes clear that a past-distinguishing frame has no associated modal formula. The proofs of the following results are by bisimulation, see [@Blackburn2001] for more information.
Theorem 11. There is no modal formula, \(\phi\), such that if \(\langle M, \mathrel{\triangleleft} \rangle \models \phi\) then \(\langle M, \mathrel{\triangleleft} \rangle\) is past-distinguishing.
Proof. The frames in Figure [fig:pastdistframes] are bisimilar and so act as a counterexample. ◻
Similarly, future-distinguishing frames have no associated modal formula.
Theorem 12. There is no modal formula, \(\phi\), such that if \(\langle M, \mathrel{\triangleleft} \rangle \models \phi\) then \(\langle M, \mathrel{\triangleleft} \rangle\) is future-distinguishing.
Proof. A contradiction is obtained by reversing the relation in Figure [fig:pastdistframes] (\(F_1' = \langle W_1, R_1^{-1} \rangle\), \(F_2' = \langle W_2, R_2^{-1} \rangle\)) and observing a similar bisimulation from \(F_1'\) to \(F_2'\). ◻
Corollary 8. A frame being distinguishing is not modally definable.
Proof. In Figure [fig:pastdistframes] we have that the frame \(F_1\) is (past- and future-)distinguishing, but it is bisimilar to \(F_2\), which is not (past-)distinguishing. ◻
7 Discussion↩︎
7.0.0.1 Modal logics of the causal ladder.
|c|c|c|c|
&
Spacetime Type (\(M\)) & \(\chron\)& \(\after\) & \(\chroneq~/\caus\)
Totally Vicious & \(\mathbf{S4} \subseteq L\) & \(\mathbf{S4} \subseteq L\) & \(\mathbf{S4} \subseteq L\)
Non-Totally Vicious & \(\mathbf{OI} \subseteq L\) & &
Chronological & \(\mathbf{OI}+\gabb \subseteq L\) & &
Causally Non-Totally Vicious & \(\mathbf{OI}\) & \(\afterlogic \subseteq L\) &
cNTV and Chronological & \(\mathbf{OI}+\gabb \subseteq L\) & &
Casual & & \(\afterlogic+\gabb \subseteq L\) &
Distinguishing & & &
\(\vdots\) &
Globally hyperbolic & \(\mathbf{OI}+\gabb \subseteq L\) & \(\afterlogic +\gabb \subseteq L\) & \(\mathbf{S4} \subseteq L\)
Table ¿tbl:tab:modalladder? shows the containment of the various modal logics for spacetimes and their various causal relations on different levels of the causal ladder. As explored in Section 5, the modal logic for two-dimensional spacetimes replaces \(\mathbf{D4da}\) with \(\mathbf{D4da_2}\) in Table ¿tbl:tab:modalladder?. The later levels of the causal ladder require new rules or additional operations to distinguish between their logics on the ladder.
7.0.0.2 Other effects on the logic.
Note that spacetimes on the same rung of the causal ladder may nevertheless exhibit distinct modal logics. For instance, contrast ordinary two-dimensional Minkowski space with the \(2^{-}\)-Minkowski spacetime: \(\{(t,x)\in\mathbb{R}^2: t <0\}\), inheriting the same causal structure as in Example 1. Both are globally hyperbolic but the logics of those spacetimes under the causal (chronological) relation are \(\mathbf{S4.2}\) [@Goldblatt1980] (\(\mathbf{OI.2}\) [@Shapirovsky2002]) and \(\mathbf{S4}\) (\(\mathbf{OI}\)) [@Shapirovsky2005] respectively.
Conversely, it is clear that the modal structure is not expressive enough to completely characterise the spacetime, since all Minkowski spaces of total dimension greater than three share the same modal logic. More can perhaps be said using a multi-modal logic, where it is possible to quantify over causal and chronological curves, and then employing Malament’s theorem [@malament1977ClassContinuousTimelike].
7.0.0.3 Multiple time dimensions.
There is a notion of spacetimes with multiple time dimensions. A \(n\)-spatial, \(t\)-temporal dimensional (or \((n,t)\)-dimensional) spacetime can then be described as working on a \(n+t\)-dimensional manifold. Our universe, \((3,1)\)-dimensional, can be considered “nice”. By changing the number of spatial or temporal dimensions, the resulting universe could be considered either too simple or too unstable (not “nice”). For instance, Tegmark [@Tegmark1997] provides various arguments for why observers cannot exist in \((n,t)\)-dimensional universes where \((n, t) \neq (3,1)\), but the arguments made are not rigorous.
One fundamental question to ask is whether there is a fundamental logical reason that these universes are not “nice”. In Section 5.2, we showed that modal logic seems expressible enough to distinguish between \((1,1)\)-dimensional and \((n,1)\)-dimensional spacetimes (\(n \geq 2\)), but it is unlikely to distinguish any other (spatial) dimensional spacetime. Extending our definition of \(\square\) and \(\lozenge\) on the causal relations to higher temporal dimensions, or using multimodal logic to represent causal relations in different time dimensions, could provide the start towards a logical language to discuss what universes are “nice” or not.
Acknowledgements↩︎
We thank Prakash Panangaden for helpful comments and feedback that helped improve our exposition, and for spotting a gap in the proof of Section 4.3. This work has been partially funded by the French National Research Agency (ANR) within the framework of “Plan France 2030”, under the research projects EPIQ ANR-22-PETQ-0007, HQI-Acquisition ANR-22-PNCQ-0001 and HQI-R&D ANR-22-PNCQ-0002.
Though there are related approaches such as via domain theory [@martin2006DomainSpacetimeIntervals] or orthomodular lattices [@casini2002LogicCausallyClosed].↩︎
In [@Shapirovsky2005], the logic \(\mathbf{L\scalebox{0.85}{\alpha}_0} = \mathbf{D4da}\mathbf{.2} = \mathbf{D4.2} + ad + a \scalebox{0.85}{\alpha}f\) is used for an analysis on Minkowski spacetime.↩︎
Read as the after-2 formula/axiom.↩︎