Robin Hirsch

The temporal logic of two-dimensional Minkowski spacetime is decidable

Joint work with Mark Reynolds.

We consider Minkowski spacetime, the set of all point-events of spacetime under the relation of causal accessibility. That is, x can access y if an electromagnetic or (slower than light) mechanical signal could be sent from x to y.

We use Prior's tense language of F and P representing causal accessibility and its converse relation. We consider two versions, one where the accessibility relation is reflexive and one where it is irreflexive.

In either case, it is not known if the logic is decidable or even axiomatisable and this has been an open problem for decades. We make a small step forward by proving, for the case where the accessibility relation is irreflexive, that the set of valid formulas over two-dimensional Minkowski spacetime is decidable; decidability for the reflexive case follows from this. The complexity of either problem is EXPTIME at worst.

We provide a temporal formula that distinguishes between three-dimensional and two-dimensional Minkowski spacetime and another temporal formula that distinguishes the two-dimensional case where the underlying field is the real numbers from the case where instead we use the rational numbers.