The addition of "actually" operators to modal languages allows us to capture important inferential behaviours which cannot be adequately captured in logics formulated in simpler languages. Previous work on modal logics containing "actually" operators has concentrated entirely upon extensions of KT5 and has employed a particular modeltheoretic treatment of them. This paper proves completeness and decidability results for a range of normal and nonnormal but quasi-normal propositional modal logics containing "actually" operators, the weakest of which are conservative extensions of K, (...) using a novel generalisation of the standard semantics. (shrink)

In this note we show that the classical modal technology of Sahlqvist formulas gives quick proofs of the completeness theorems in [8] (D. Gregory, Completeness and decidability results for some propositional modal logics containing "actually" operators, Journal of Philosophical Logic 30(1): 57-78, 2001) and vastly generalizes them. Moreover, as a corollary, interpolation theorems for the logics considered in [8] are obtained. We then compare Gregory's modal language enriched with an "actually" operator with the work of Arthur Prior now known under (...) the name of hybrid logic. This analysis relates the "actually" axioms to standard hybrid axioms, yields the decidability results in [8], and provides a number of complexity results. Finally, we use a bisimulation argument to show that the hybrid language is strictly more expressive than Gregory's language. (shrink)

In this note we show that the classical modal technology of Sahlqvist formulas gives quick proofs of the completeness theorems in [8] (D. Gregory, Completeness and decidability results for some propositional modal logics containing “actually” operators, Journal of Philosophical Logic 30(1): 57–78, 2001) and vastly generalizes them. Moreover, as a corollary, interpolation theorems for the logics considered in [8] are obtained. We then compare Gregory's modal language enriched with an “actually” operator with the work of Arthur Prior now known under (...) the name of hybrid logic. This analysis relates the “actually” axioms to standard hybrid axioms, yields the decidability results in [8], and provides a number of complexity results. Finally, we use a bisimulation argument to show that the hybrid language is strictly more expressive than Gregory's language. (shrink)

In this paper, I investigate a system of quantified modal logic, due in many respects to Bressan (see [2]), from several perspectives -- both semantic and proof-theoretic. As Anderson and Belnap note in [1]: "It seems to be generally conceded that formal systems are natural or substantial if they can be looked at from several points of view. We tend to think of systems as artificial or ad hoc if most of their formal properties arise from some one notational system (...) in terms of which they are described." My efforts in this paper will be in part to lend substantiality to the system in question. Several formulation of the system are given and proved equivalent in appropriate senses. Also, some comments are made concerning possible alternative formulations. (shrink)