The paper presents a family of propositional epistemic logics such that languages of these logics are extended by quantification over modal operators or over agents of knowledge and extended by predicate symbols that take modal operators as arguments. Denote this family by \}\). There exist epistemic logics whose languages have the above mentioned properties :311–350, 1995; Lomuscio and Colombetti in Proceedings of ATAL 1996. Lecture Notes in Computer Science, vol 1193, pp 71–85, 1996). But these logics are obtained from first-order (...) modal logics, while a logic of \}\) can be regarded as a propositional multi-modal logic whose language includes quantifiers over modal operators and predicate symbols that take modal operators as arguments. Among the logics of \}\) there are logics with a syntactical distinction between two readings of epistemic sentences: de dicto and de re. We show the decidability of logics of \}\) with the help of the loosely guarded fragment of first-order logic. Namely, we generalize LGF to a higher-order decidable loosely guarded fragment. The latter fragment allows us to construct various decidable propositional epistemic logics with quantification over modal operators. The family of this logics coincides with \}\). There are decidable propositional logics such that these logics implicitly contain quantification over agents of knowledge, but languages of these logics are usual propositional epistemic languages without quantifiers and predicate symbols :345–378, 1993). Some logics of \}\) can be regarded as counterparts of logics defined in Grove and Halpern :345–378, 1993). We prove that the satisfiability problem for these logics of \}\) is Pspace-complete using their counterparts in Grove and Halpern :345–378, 1993). (shrink)

We prove that the positive fragment of first-order intuitionistic logic in the language with two individual variables and a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable. This holds true regardless of whether we consider semantics with expanding or constant domains. We then generalise this result to intervals \ and \, where QKC is the logic of the weak law of the excluded middle and QBL and QFL are first-order counterparts of Visser’s basic and formal logics, (...) respectively. We also show that, for most “natural” first-order modal logics, the two-variable fragment with a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable, regardless of whether we consider semantics with expanding or constant domains. These include all sublogics of QKTB, QGL, and QGrz—among them, QK, QT, QKB, QD, QK4, and QS4. (shrink)

As a remedy for the bad computational behaviour of first-order temporal logic (FOTL), it has recently been proposed to restrict the application of temporal operators to formulas with at most one free variable thereby obtaining so-called monodic fragments of FOTL. In this paper, we are concerned with constructing tableau algorithms for monodic fragments based on decidable fragments of first-order logic like the two-variable fragment or the guarded fragment. We present a general framework that shows how existing decision procedures for first-order (...) fragments can be used for constructing a tableau algorithm for the corresponding monodic fragment of FOTL. Some example instantiations of the framework are presented. (shrink)

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 ∃x◻φ, e.g., knowing how to achieve φ roughly means that there exists a way such that you know that it is a way to ensure that φ. 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, 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 the new modality and know-that operator in an epistemic setting. (shrink)

In this paper, the predicate counterparts, defined both axiomatically and semantically by means of Kripke frames, of the modal propositional logics $\textbf {GL}$, $\textbf {Grz}$, $\textbf {wGrz}$ and their extensions are considered. It is proved that the set of semantical consequences on Kripke frames of every logic between $\textbf {QwGrz}$ and $\textbf {QGL.3}$ or between $\textbf {QwGrz}$ and $\textbf {QGrz.3}$ is $\Pi ^1_1$-hard even in languages with three (sometimes, two) individual variables, two (sometimes, one) unary predicate letters, and a single (...) proposition letter. As a corollary, it is proved that infinite families of modal predicate axiomatic systems, based on the classical first-order logic and the modal propositional logics $\textbf {GL}$, $\textbf {Grz}$, $\textbf {wGrz}$ are not Kripke complete. Both $\Pi ^1_1$-hardness and Kripke incompleteness results of the paper do not depend on whether the logics contain the Barcan formula. (shrink)