Abstract
Natural language provides motivation for studying modal backwards-looking operators such as “now”, “then” and “actually” that evaluate their argument formula at some previously considered point instead of the current one. This paper investigates the expressive power over models of both propositional and first-order basic modal language enriched with such operators. Having defined an appropriate notion of bisimulation for first-order modal logic, I show that backwards-looking operators increase its expressive power quite mildly, contrary to beliefs widespread among philosophers of language and formal semanticists. That in turn presents a strong argument for the use of operator-based systems in the semantics of natural language, instead of systems with explicit quantification over worlds and times that have become a de-facto standard for such applications. The popularity of such explicit-quantification systems is shown to be based on the misinterpretation of a claim by Cresswell (Entities and indices, Kluwer, Dordrecht, 1990), which led many philosophers and linguists to assume (wrongly) that introducing “now” and “then” is expressively equivalent to explicitly quantifying over worlds and times.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Notes
From here on, I talk only about expressive power over models. For the application to natural language, that is arguably a more important kind of expressivity than expressivity over frames.
Quantified modal logic, also called first-order modal logic, is related to (propositional) modal logic the same way as first-order logic is related to propositional logic.
The term “backwards-looking operators” is due to (Saarinen 1978).
Currently with about 200 citations in the Google Scholar web service, which is a large number for a linguistic article.
Contrary to that, (Verkuyl 2008, pp. 130–132) argues that \(\mathbf {now}\) is semantically superfluous in modal logic. But Verkuyl does not discuss any quantificational examples like 2 which pose a true expressivity problem, and only considers sentences such as 1 for which \(\mathbf {now}\) is indeed semantically superfluous.
Perhaps more in the spirit of current explicit-quantification systems, in particular of the branch of formal semantics called LF semantics, would be the following alternative. There would be no intension operator \(^{\wedge t}\); \(\mathbf {now}\) would take as arguments functions from times; there will be a rule of freely applying \(\lambda t_i\) operators; and finally, a constraint would force the explicit variable next to “alive” to be bound by the closest \(\lambda \)-restrictor specifically when “alive” is modified by “now”, but not otherwise. The problem with such an account is that this last constraint is, so to speak, non-compositional: the variables on predicates like “alive” should generally not be subject to the closest-binder requirementm and only when we know that that predicate is in the scope of “now”, would a different constraint be imposed.
In fairness, some of those assumptions would be “independently justified”, in the sense that for many intensional phenomena of natural language, we would need similar ones anyway. For example, adding an extra binding-theoretic constraint specifically for time variables in the scope of “now” and “then” is not such a wild idea if we already adopted a number of such constraints anyway. But if we do not have to introduce any of this apparatus for restricting the enormous expressive power of the full FOL in the first place, that’s a different story.
It is usual to give a syntactic definition of a sentence, where a sentence is a formula without free variables. Semantically, such a formula does not depend on the assignment of values to variables. It is easy to give a purely syntactic definition of a \(\mathbf {Cr}\) sentence, but I find that the semantic definition in the main text makes the intuition behind the notion more prominent.
Another design choice is whether to add any sort of counterpart theory, cf. (Lewis 1968). Counterpart theory is often used to identify individuals at different points when point domains are disjoint, but can be added to any other kind of domain semantics as well. I will refrain from discussing counterpart theories altogether. See (Fara 2008) and references therein for combining a counterpart theory with ‘now’ and ‘actually’.
However, we can provide an analogue of the Hennessy-Milner theorem that states that the converse holds for a particular class of models. For \(\mathbf {ML}\), that is the class of image-finite models: those where every point has only a finite number of \(R\)-successors for each \(R\). The propositional proof shows that the relation of modal equivalence is itself a bisimulation in this case. The condition of image-finiteness allows the following argument to come through: suppose that \(w\) and \(w'\) are bisimilar, but for some \(v: wRv\), there is no bisimilar \(v':w'Rv'\). Then for each \(u'_i:w'Ru'_i\), there is \(\phi _i\) s.t. \(v'\models \phi _i\), but \(u'_i \not \models \phi _i\). As the set of all \(u'_i\) is finite, we can build formula \(\Diamond \bigwedge _i\phi _i\), which is true at \(w\) thanks to the existence of \(v\), but is false at \(w'\). This is contrary to assumption.
In the case of \(\mathbf {ML}^{FO}\), we need not only the assumption of finiteness for successor points, but also for domains of individuals. The argument for individuals would be along the following lines. Suppose that there are indistinguishable \(w\) and \(w'\) where \(\bar{a}\) at \(w\) has no correspondent \(\bar{b}\) at \(w'\). Then we collect all pairs of \(\pi \) and \(\phi \) that witness that a particular \(\bar{b}\) does not correspond to \(\bar{a}\), and as there is only a finite number of distinct \(\bar{b}\)s, we can collect them into one large formula \(\exists \bar{x} \bigwedge _i \pi _i\phi _i(\bar{x})\). At \(w\), tuple \(\bar{a}\) ensures that this formula is true, but at \(w'\) by construction there is no \(\bar{b}\) that would witness that. But then \(w\) and \(w'\) have different \(\mathbf {ML}^{FO}\) theories, contrary to assumption. When the number of distinct tuples is not finite, we cannot gather all \(\pi \) and \(\phi \) into a single formula, hence the converse to Theorem 2 would not hold in such a case.
This informal characterization of the difference which introducing \(\mathbf {then}\)-operators makes is similar to the one given by (Meyer 2009).
When not genuinely backwards-looking, those operators essentially act as unbound hybrid \(@i\) operators.
(Meyer 2009) is another philosophical take on the problem of expressivity of “now” and “then” operators. Meyer (p. 229) aims to show “that now and then are eliminable in quantified tense logic, provided we endow it with enough quantificational structure.” What he means by “enough quantificational structure” is including into the language a set membership predicate and existential quantification over sets. With that much, we can easily express Russell’s paradox: \(\exists s(s \not \in s)\).
Even if one does not worry about paradoxes, adding quantification over sets we become able to express second-order properties (e.g., distinguish the standard model of Peano arithmetic from non-standard models), thus going a long way beyond the expressive resources of FOL. Using set theory, Meyer can indeed eliminate “now” and “then” operators. One wonders, however, if such a solution “deals with the problem in the most natural way”, as Meyer puts it (p. 242). As we have seen, “now” and “then” operators actually make the basic modal language only slightly more expressive, so it is hardly surprising that by going as far as second-order expressivity we can become able to eliminate them.
Both Cresswell and Meyer aim to trivialize the contribution of “now” and “then” operators: Cresswell argues that such operators increase the expressive power of the language up to that of FOL, and Meyer argues that in a language that can express second-order properties, “now” and “then” are redundant anyway. The framework we developed in this paper allows us to understand the actual contribution of such operators without trying to fully reduce them to some familiar, and vastly more expressive, system. Our model-theoretic analysis allows us to distinguish cases where the addition of \(\mathbf {then}\) makes a difference from cases where it doesn’t.
The actual position of (Benthem 1977) is in fact nothing of the sort. As van Benthem himself puts it (p. 436): “From a technical point of view, tense logics could be considered to be sublogics of predicate logic. \(<\)...\(>\) But, as tense logics become stronger and stronger (containing ever more exotic operators), predicate logic itself becomes a serious rival as regards elegance and simplicity” (emphasis mine).
References
Areces, C., Blackburn, P., & Marx, M. (2001). Hybrid logics: Characterization, interpolation and complexity. The Journal of Symbolic Logic, 66(3), 977–1010.
Areces, C., Figueira, D., Figueira, S., & Mera, S. (2011). The expressive power of memory logics. Review of Symbolic Logic, 4(2), 290–318.
Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal logic, volume 53 of Cambridge tracts in theoretical computer science. Cambridge: Cambridge University Press.
Blackburn, P., & Seligman, J. (1995). Hybrid languages. Journal of Logic, Language and Information, 4, 251–272.
Blackburn, P., & Seligman, J. (1998). What are hybrid languages? In M. Kracht, M. de Rijke, H. Wansing, & M. Zakharyaschev (Eds.), Advances in modal logic (Vol. 1, pp. 41–62). Stanford: CSLI Publications.
Blackburn, P. and van Benthem, J. (2007). Modal logic: A semantic perspective. In Blackburn et al., (Eds.) chapter 1. Amsterdam: Elsevier.
Blackburn, P., van Benthem, J. F., and Wolter, F., editors (2007). Handbook of modal logic, volume 3 of Studies in logic and practical reasoning. Elsevier.
Cresswell, M. (1990). Entities and indices. Dordrecht: Kluwer.
Cresswell, M. (1991). In defense of the barcan formula. Logique et Analyse, 135–136, 271–282.
Fara, D. G. (2008). Relative-sameness counterpart theory. The Review of Symbolic Logic, 1(2), 167–189.
Fitting, M. and Mendelsohn, R. L. (1998). First-order modal logic, volume 277 of synthese library. Kluwer, Dordrecht.
Gabbay, D. M. (1981). An irreflexivity lemma with applications to axiomatizations of conditions on linear frames. In U. Mönnich (Ed.), Aspects of philosophical logic (pp. 67–89). Dordrecht: Reidel.
Goranko, V., & Passy, S. (1992). Using the universal modality: Gains and questions. Journal of Logic and Computation, 2(1), 5–30.
Grädel, E., & Otto, M. (1999). On logics with two variables. Theoretical Computer Science, 224, 73–113.
Kamp, H. (1971). Formal properties of “now”. Theoria, 37, 227–273.
Lewis, D. K. (1968). Counterpart theory and quantified modal logic. Journal of Philosophy, 65(5), 113–126.
Meyer, U. (2009). ‘Now’ and ‘then’ in tense logic. Journal of Philosophical Logic, 38(2), 229–247.
Percus, O. (2000). Constraints on some other variables in syntax. Natural Language Semantics, 8, 173–229.
Recanati, F. (2007). Perspectival thought: A plea for (moderate) relativism. Oxford: Oxford University Press.
Saarinen, E. (1978). Backward-looking operators in tense logic and in natural language. In J. Hintikka, I. Niiniluoto, & E. Saarinen (Eds.), Essays on mathematical and philosophical logic (pp. 341–367). Dordrecht: Reidel.
Schlenker, P. (2003). A plea for monsters. Linguistics and Philosophy, 26, 29–120.
ten Cate, B. D. (2005). Model theory for extended modal languages. PhD thesis, ILLC, University of Amsterdam.
van Benthem, J. F. (1977). Tense logic and standard logic. Logique et Analyse, 20, 41–83.
Verkuyl, H. (2008). Binary tense, volume 187 of CSLI lecture notes. Stanford: CSLI Publications.
Acknowledgments
I am grateful to Patrick Blackburn, Benjamine George, Salvador Mascarenhas, Philippe Schlenker and Wolfgang Sternefeld for discussions of the material, and to the anonymous reviewers, whose comments have helped to significantly improve the paper both in form and in substance. All remaining errors are, of course, my own. The final stages of the work on the paper have been partially supported by the Alexander von Humboldt foundation, which is hereby gratefully acknowledged.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Yanovich, I. Expressive Power of “Now” and “Then” Operators. J of Log Lang and Inf 24, 65–93 (2015). https://doi.org/10.1007/s10849-014-9210-3
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10849-014-9210-3