Takahiro Sawasaki

STIT logic is a family of logics of agency that have received attention in the literature. Despite a variety of developments, most of the existing studies on STIT logic are based on propositional logic. Such propositional STIT logics have computational advantages, but in these logics it seems difficult to distinguish the de re and de dicto readings of sentences about choice independently of models and assignments. To overcome this expressive limitation, this paper presents a cstit-based atemporal first-order STIT logic and its finite domain version as members of a family of term-modal logics possibly with a generalized axiom of independence of agents. The main result is that our proposed Hilbert-style systems for term-modal logics with the alethic modality, equality and non-rigid terms, when they have the (generalized) axiom of independence of agents only if the number of agents is finite, are strongly complete. In particular, the strong completeness of a Hilbert-style system for our first-order STIT logic of finite domain is proved.

STIT logic is a family of logics of agency that have received attention in the literature. Despite a variety of developments, most of the existing studies on STIT logic are based on propositional logic. Such propositional STIT logics have computational advantages, but in these logics it seems difficult to distinguish the _de re_ and _de dicto_ readings of sentences about choice independently of models and assignments. To overcome this expressive limitation, this paper presents a cstit-based atemporal first-order STIT logic and its finite domain version as members of a family of term-modal logics possibly with a generalized axiom of independence of agents. The main result is that our proposed Hilbert-style systems for term-modal logics with the alethic modality, equality and non-rigid terms, when they have the (generalized) axiom of independence of agents only if the number of agents is finite, are strongly complete. In particular, the strong completeness of a Hilbert-style system for our first-order STIT logic of finite domain is proved.

In this paper, we prove the semantic incompleteness of some expansions of the Hilbert-style system for the minimal normal term-modal logic with equality and non-rigid terms that were proposed in Liberman et al. (2020) “Dynamic Term-modal Logics for First-order Epistemic Planning.” Term-modal logic is a family of first-order modal logics having term-modal operators indexed with terms in the first-order language. While some first-order formula is valid over the corresponding class of frames in the involved Kripke semantics, it is not provable in those expansions. We show this fact by introducing a non-standard Kripke semantics which makes the meanings of constants and function symbols relative to the meanings of relation symbols combined with them. We also address an incorrect frame correspondence result given in Liberman et al. (2020).