It is proved that if a finitely axiomatizable modal logic L is elementary, then the validity problem for L, which asks whether a given finite Kripke frame validates L, is in P, which allows us to transfer complexity results in graph theory to the study of elementarity of modal logics.
Abstract
A modal logic is elementary if it is sound and complete with respect to an elementary class of Kripke frames. We prove that if a finitely axiomatizable modal logic L is elementary, then the validity problem for L, which asks whether a given finite Kripke frame validates L, is in P. This allows us to transfer complexity results in graph theory to the study of elementarity of modal logics. As an application, we construct infinitely many finitely axiomatizable K4-stable logics that are not elementary, assuming P $\neq$ NP. This result provides a conditional negative answer to an open question in [Bezhanishvili et al., 2018] for K4-stable logics.
Bisimulation is the basic equivalence between models in modal logic. Although bisimulation implies modal equivalence, the converse does not hold in general. Hennessy–Milner-style theorems find various conditions under which the converse holds, e.g. finiteness. In Kripke semantics, the condition of finiteness can be imp...
Helena Marciuš, Tin Perkov· Bulletin of the Section of L...· 0 citations
This paper provides a constructive decision procedure, that, given a formula, produces either a proof showing the formula to be valid or a finite countermodel falsifying the formula, thus also proving the finite model property for both logics.
Marianna Girlando, Roman Kuznets, Sonia Marin et al.· 1 citation
This paper gives a survey of propositional modal logic in an intuitionistic setting. Mainly intended for readers already familiar with classical modal logic, we discuss why there are two prominent families of such logics, intuitionistic modal logics (IMLs) and constructive modal logics (CMLs), what motivates their stud...
We construct an uncountable sequence of minimal varieties of modal algebras which do not contain any modal algebra whose Boolean reduct forms a powerset algebra. By algebraizabilty and duality between modal algebras and neighborhood frames, this yields a result stating that there exists an uncountable set of Post com...
Krzysztof A. Krawczyk· The Review of Symbolic Logic· 0 citations
The logic FOT is a team-based logic whose expressive power coincides with first-order logic at the level of both sentences and open formulas. In contrast to dependence and independence logics, which can define stronger second-order team properties, FOT is designed to capture exactly elementary team properties, modulo t...
A uniform proof-theoretic framework for non-contingency logic over a broad class of frame conditions is developed based on generalized path conditions (GPCs), a grammar-theoretic formalism that uniformly captures many standard modal frame properties.
Yun-Song Wang, Lukas Zenger· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
