Generalized Bundled Fragments of First-order Modal Logic

Beyond know-thatbundled fragmentsProceeding Paper
Mo Liu, Anantha Padmanabha, R. Ramanujam and Yanjing Wang
MFCS 2022
Publication year: 2022

When we bundle quantifiers and modalities together (as in $\exists x \Box$, $\Diamond \forall x$ etc.) in first-order modal logic (FOML), we get new logical operators whose combinations produce interesting \textit{bundled} fragments of FOML. It is well-known that finding decidable fragments of \FOML is hard, but existing work shows that certain bundled fragments are decidable [Padmanabha et al 2018], without any restriction on the arity of predicates, the number of variables, or the modal scope. In this paper, we explore generalized bundles such as $\forall x\forall y \Box, \forall x\exists y \Diamond$ etc., and map the terrain with regard to decidability, presenting both decidability and undecidability results. In particular, we propose the loosely bundled fragment which is decidable over increasing domains and encompasses all known decidable bundled fragments.

Bundled fragments of first-order modal logic: (un)decidability

Beyond know-thatbundled fragmentsProceeding Paper
Padmanabha, Anantha and Ramanujam, R. and Wang, Yanjing
In Proceedings of Foundations of Software Technology and Theoretical Computer Science (FSTTCS) 2018, 2018
Publication year: 2018

Abstract: Quantified modal logic provides a natural logical language for reasoning about modal attitudes even while retaining the richness of quantification for referring to predicates over domains. But then most fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic) have been shown to be decidable. In this paper, we study fragments that bundle quantifiers and modalities together, inspired by earlier work on epistemic logics of know-how/why/what. As always with quantified modal logics, it makes a significant difference whether the domain stays the same across worlds, or not. In particular, we show that the bundle \forall \Box is undecidable over constant domain interpretations, even with only monadic predicates, whereas \exists \Box bundle is decidable. On the other hand, over increasing domain interpretations, we get decidability with both \forall \Box and \exists \Box bundles with unrestricted predicates. In these cases, we also obtain tableau based procedures that run in PSPACE. We further show that the \exists \Box bundle cannot distinguish between constant domain and increasing domain interpretations.

A New Modal Framework for Epistemic Logic

Beyond know-thatbundled fragmentsProceeding PaperSelectedTARK
Wang, Yanjing
Proceedings of Conference on Theoretical Aspects of Rationality and Knowledge (TARK) 2017, 251: 515—534, 2017
Publication year: 2017

Abstract: Recent years witnessed a growing interest in non-standard epistemic logics of knowing whether, knowing how, knowing what, knowing why and so on. The new epistemic modalities introduced in those logics all share, in their semantics, the general schema of \exists x\phi, e.g., knowing how to achieve \phi roughly means that there exists a way such that you know that it is a way to ensure that \phi Moreover, the resulting logics are decidable. Inspired by those particular logics, in this work, we propose a very general and powerful framework based on quantifier-free predicate language extended by a new modality x, which packs exactly x together. We show that the resulting language, though much more expressive, shares many good properties of the basic propositional modal logic over arbitrary models, such as finite-tree-model property and van Benthem-like characterization w.r.t. first-order modal logic. We axiomatize the logic over S5 frames with intuitive axioms to capture the interaction between x and know-that operator in an epistemic setting.