The monodic fragment of propositional term modal logic (Q2001365)

The paper deals with so-called term modal logics (TML), introduced by \textit{M. Fitting} et al. [Stud. Log. 69, No. 1, 133--169 (2001; Zbl 0992.03026)]. In such logics, modalities are indexed by variables for agents, and these can be quantified over. According to the authors, the sentence ``every Christian believes in the existence of God'' is formalised in TML as \[ \forall x (\mbox{christian}(x) \rightarrow \Box_x \exists y \mbox{ God}(y)) \] The focus of the present paper is on the propositional fragment PTML of the logic, where the atoms are restricted to propositions. The paper starts by working out a suitable notion of bisimulation for this fragment, and it uses it to show that the tree property holds. This one tells us that, if a formula is satisfiable, then it is satisfiable at the root of a tree-like model. This is established by adapting the well-known method of unraveling, where transitions in the original model are explicitely represented as states in the new model. Next -- and this is the main result in the paper -- it is shown that the (as the authors call it) ``monodic'' fragment of the logic is decidable even though the full logic is not. The monodic fragment is defined as the subset of the language obtained by imposing the syntactical restriction that there must be no more than one free variable inside the scope of a modality. For instance \(\forall x \exists y \Box_x \Box_y p\) does not belong to the monodic fragment, while \(\forall x \Box_x \Box_x p\) does. Reviewer's comments: \(\#\)1 `monodic' is a neologism, formed by analogy with `monadic' (as in monadic predicate calculus) \(\#\)2 The basic idea is to let a quantifier bind a subscripted variable. This can be done even in the context of a propositional multi-modal logic. It is interestring to remark that a similar suggestion was made by \textit{B. Hansson} in deontic logic [Theoria 36, 241--248 (1971; Zbl 0231.02025)]. His approach is motivated by the observation that ``If we say `it is obligatory to do \(p\)' in a context where there is no tacit reference to a specific individual, we often mean `it is obligatory for everyone to do \(p\)' (p. 246) The obligation to do \(p\) is thus analysed as ``\(\forall x\) \(O_x p\)''. One may wish to go one step further, and work with variables ranging over \textit{sets} of agents, distinguishing between the authorities issuing the norms and their addressees. This is done by \textit{P. Bailhache} in his paper [Log. Anal., Nouv. Sér. 24, 65--80 (1981; Zbl 0463.03002)].