We provide a Hilbert-style axiomatization of the logic of , as well as a two-dimensional semantics with respect to which our logics are sound and complete. Our completeness results are quite general, pertaining to all such actuality logics that extend a normal and canonical modal basis. We also show that our logics have the strong finite model property and permit straightforward first-order extensions.

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, which led many philosophers and linguists to assume that introducing “now” and “then” is expressively equivalent to explicitly quantifying over worlds and times. (shrink)

In the paper (Braüner, 2001) we gave a minimal condition for the existence of a homophonic theory of truth for a modal or tense logic. In the present paper we generalise this result to arbitrary modal logics and we also show that a modal logic permits the existence of a homophonic theory of truth if and only if it permits the definition of a socalled master modality. Moreover, we explore a connection between the master modality and hybrid logic: We show (...) that if attention is restricted to bidirectional frames, then the expressive power of the master modality is exactly what is needed to translate the bounded fragment of first-order logic into hybrid logic in a truth preserving way. We believe that this throws new light on Arthur Prior's fourth grade tense logic. (shrink)

We prove that every first-order formula that is invariant under quasi-injective bisimulations is equivalent to a formula of the hybrid logic . Our proof uses a variation of the usual unravelling technique. We also briefly survey related results, and show in a standard way that it is undecidable whether a first-order formula is invariant under quasi-injective bisimulations.