Some Results on Causal Modalities in General Spacetimes

Technical Summary: Some Results on Causal Modalities in General Spacetimes

Problem Statement
The paper addresses the classification of modal logics induced by causal structures in spacetimes. While the modal logics for the chronological ($\ll$) and causal ($\preceq$) relations in Minkowski spacetime are well-established (identified as $OI.2$ and $S4.2$, respectively), the logic of the "after" relation ($\alpha$)—the strict variant of the causal relation where $x \alpha y$ iff there exists a non-degenerate causal curve from $x$ to $y$—remains less understood. Previous work by Shapirovsky and Shehtman established that the after modality in Minkowski space satisfies a specific formula (the "after formula"), but it was unknown whether this holds for arbitrary spacetimes or what the complete modal logic of Minkowski space with the after relation is. Furthermore, the modal properties of general spacetimes, which may possess complex global topologies distinct from Minkowski space, had not been systematically investigated.

Methodology
The authors employ a combination of differential geometry and modal logic.

1. Geometric Framework: The study is grounded in the definitions of smooth spacetimes (Lorentzian manifolds with time orientation). The authors utilize standard causal relations ($\preceq, \ll, \to$) and introduce the "after" relation ($\alpha$). They analyze these relations along the "causal ladder," a hierarchy of spacetime properties ranging from totally vicious to globally hyperbolic.
2. Modal Logic Framework: The authors utilize Kripke semantics, mapping spacetime points to worlds and causal relations to accessibility relations. They investigate which normal modal logics (e.g., $S4$, $D4$, $OI$) and specific axioms (such as the "after formula" $a\alpha f$) are valid in these frames.
3. Proof Techniques:
   • Geodesic Normal Coordinates: To extend results from Minkowski space to arbitrary spacetimes, the authors use the exponential map to construct local convex normal neighborhoods. This allows them to lift local Minkowski properties to general manifolds.
   • Counter-models and Bisimulation: To demonstrate the limits of expressivity (e.g., regarding distinguishing properties), the authors construct specific finite frames and use bisimulation arguments.
   • Topological Arguments: Proofs involving the "push-up rule" and the separation of lightlike and timelike curves rely on the openness of chronological cones and the properties of achronal lightlike geodesics.

Key Contributions and Results

1. The After Formula in General Spacetimes:
   The primary result (Theorem 4.6) proves that the "after formula" ($a\alpha f$), previously known to hold in Minkowski space, is valid in the after modality of any smooth spacetime. The formula corresponds to a first-order property involving the existence of a common future point for unrelated successors. The proof relies on a key geometric lemma (Lemma 4.5): if $x \alpha y \alpha y_1, y_2$ and $y_1, y_2$ are spacelike separated, then $x \ll y_i$ for some $i$. This is established by analyzing the behavior of causal curves in geodesic normal coordinates. Consequently, the logic $D4da$ (defined as $D4 + ad + a\alpha f$) is a subset of the logic of the after relation for any spacetime.

2. Dimensional Expressivity (2D vs. Higher Dimensions):
   The authors introduce a modified formula, $a\alpha 2f$, which is the after formula without the initial diamond operator. They prove that this formula holds in all two-dimensional spacetimes (Theorem 5.4) but fails in Minkowski spaces of dimension $1+n$ where $n \ge 2$ (Lemma 5.3). This demonstrates that the modal logic of two-dimensional spacetimes is strictly more expressive than that of higher-dimensional spacetimes regarding the after relation. The authors conjecture that for $n \ge 3$, the formula $a\alpha 2f$ fails in causally non-totally vicious (cNTV) spacetimes.

3. Refinement of the Causal Ladder:
   The paper introduces the property "causally non-totally vicious" (cNTV), defined as the existence of a point $x$ such that not $x \alpha x$. This property separates the loss of reflexivity in the causal relation from the gain of irreflexivity. The authors map these properties to the causal ladder (Figure 2), showing how different levels (e.g., chronological, causal, distinguishing) affect the validity of specific modal logics.

   • Totally Vicious: All causal relations coincide, yielding $S4$.
   • Chronological: The logic for $\ll$ gains the Gabbay rule (irreflexivity), becoming $OI + (Gabb)$.
   • Causal: The logic for $\alpha$ gains the Gabbay rule, becoming $D4da + (Gabb)$.
   • Distinguishing: The authors prove (Theorems 6.10, 6.11) that neither past-distinguishing nor future-distinguishing properties are modally definable by any single modal formula, as they are not preserved under bisimulation.

4. Limitations of Modal Logic:
   The paper notes that modal logic cannot fully characterize spacetime geometry. For instance, all Minkowski spaces of dimension greater than three share the same modal logic, and spacetimes on the same rung of the causal ladder (e.g., different globally hyperbolic spacetimes) can exhibit distinct logics.

Significance and Claims
The paper claims to advance the classification of modal logics for spacetimes by moving beyond the specific case of Minkowski space to arbitrary smooth manifolds. Its significance lies in:

• Establishing the universality of the "after formula" across all spacetimes, providing a robust lower bound for the logic of the after relation.
• Demonstrating a clear modal distinction between two-dimensional and higher-dimensional spacetimes, suggesting that dimensionality is a factor detectable by specific modal axioms.
• Refining the causal ladder by introducing the cNTV property, which allows for a more granular analysis of how causal structure influences modal logic.
• Clarifying the boundaries of modal expressivity, specifically showing that while some causal properties (like irreflexivity) are modally definable, others (like distinguishing) are not.

The authors maintain a modest stance, acknowledging that the complete modal logic of Minkowski space with the after relation remains an open problem and that their results primarily establish containment relations and specific validities rather than a full axiomatization for all spacetime types.