Chronological future modality in Minkowski spacetime. (English) Zbl 1082.03016
Balbiani, Philippe (ed.) et al., Advances in modal logic. Vol. 4. Selected papers from the 4th conference (AiML 2002), Toulouse, France, October 2002. London: King’s College Publications (ISBN 0-9543006-1-0/pbk; 0-9543006-2-9/hbk). 437-459 (2003).
From the introduction: The problem of logical foundations of contemporary physics was included by David Hilbert in the list of the most important mathematical problems and generated an interesting research area in nonclassical logic. Study of relativistic temporal logics is a natural topic within this area. Their investigation was initiated by Arthur Prior’s proposal in his book [Past, present and future. Oxford: Clarendon Press (1967; Zbl 0169.29802)], but at the early stage did not move fast – perhaps because relativistic time is both branching and dense, which is rather unusual for modal logic.
Let us recall that two basic relations in Minkowski spacetime are causal \((\prec)\) and chronological \((\preceq)\) accessibility. The causal future of a point-event \(x\) consists of all those points \(y\) to which a signal from \(x\) can be sent; \(x\prec y\) if this signal is slower than light.
The first significant result in relativistic temporal logic was the theorem by R. Goldblatt [Stud. Log. 39, 219–236 (1980; Zbl 0457.03019)] identifying the (“Diodorean”) modal logic of relation \(\preceq\) as the well-known S4.2. Then the second author [Stud. Log. 42, 63–80 (1983; Zbl 0541.03011)] described modal logics of domains on Minkowski plane ordered by \(\preceq\).
This paper makes the next essential step after the past twenty years. It solves one of three problems posed by Goldblatt [loc. cit.]: to axiomatize the modal logic of the frame \((\mathbb{R}^n,\prec)\). For this logic L\(_2\) we present an axiom system. Its axioms are widely known in modal logic, except for the specific axiom of 2-density, first introduced by Goldblatt [loc. cit.]. The logic L\(_2\) is rather standard, but the completeness proof for the intended interpretation is not so straightforward. The main technical problem is the proof of the finite model property. As 2-density is not preserved under filtration in the Lemmon-Segerberg style (when some worlds are identified), we use the Kripke-Gabbay method of selective filtration instead. This method allows us to extract a finite submodel from an infinite model. In our case selective filtration is applied to the canonical model in a combination with the method of maximal points, due to Kit Fine. The finite model characterization is convenient for obtaining complexity bounds of L\(_1\), L\(_2\); this subject is postponed until a further publication. The final part of the proof is a geometric construction of a p-morphism. In the last section we discuss applications of our results to many-dimensional modal logics, such as products and interval logics.
For the entire collection see [Zbl 1062.03008].
Let us recall that two basic relations in Minkowski spacetime are causal \((\prec)\) and chronological \((\preceq)\) accessibility. The causal future of a point-event \(x\) consists of all those points \(y\) to which a signal from \(x\) can be sent; \(x\prec y\) if this signal is slower than light.
The first significant result in relativistic temporal logic was the theorem by R. Goldblatt [Stud. Log. 39, 219–236 (1980; Zbl 0457.03019)] identifying the (“Diodorean”) modal logic of relation \(\preceq\) as the well-known S4.2. Then the second author [Stud. Log. 42, 63–80 (1983; Zbl 0541.03011)] described modal logics of domains on Minkowski plane ordered by \(\preceq\).
This paper makes the next essential step after the past twenty years. It solves one of three problems posed by Goldblatt [loc. cit.]: to axiomatize the modal logic of the frame \((\mathbb{R}^n,\prec)\). For this logic L\(_2\) we present an axiom system. Its axioms are widely known in modal logic, except for the specific axiom of 2-density, first introduced by Goldblatt [loc. cit.]. The logic L\(_2\) is rather standard, but the completeness proof for the intended interpretation is not so straightforward. The main technical problem is the proof of the finite model property. As 2-density is not preserved under filtration in the Lemmon-Segerberg style (when some worlds are identified), we use the Kripke-Gabbay method of selective filtration instead. This method allows us to extract a finite submodel from an infinite model. In our case selective filtration is applied to the canonical model in a combination with the method of maximal points, due to Kit Fine. The finite model characterization is convenient for obtaining complexity bounds of L\(_1\), L\(_2\); this subject is postponed until a further publication. The final part of the proof is a geometric construction of a p-morphism. In the last section we discuss applications of our results to many-dimensional modal logics, such as products and interval logics.
For the entire collection see [Zbl 1062.03008].
