In this paper, we investigate the many-valued version of coalgebraic modal logic through predicate lifting approach. Coalgebras, understood as generic transition systems, can serve as semantic structures for various kinds of modal logics. A well-known result in coalgebraic modal logic is that its completeness can be determined at the one-step level. We generalize the result to the finitely many-valued case by using the canonical model construction method. We prove the result for coalgebraic modal logics based on three different many-valued algebraic structures, including the finitely-valued Łukasiewicz algebra, the commutative integral Full-Lambek algebra (FL$_{ew}$-algebra) expanded with canonical constants and Baaz Delta, and the FL$_{ew}$-algebra expanded with valuation operations. In addition, we also prove the finite model property of the many-valued coalgebraic modal logic by using the filtration technique.
We prove strong completeness of a range of substructural logics with respect to a natural poset-based relational semantics using a coalgebraic version of completeness-via-canonicity. By formalizing the problem in the language of coalgebraic logics, we develop a modular theory which covers a wide variety of different logics under a single framework, and lends itself to further extensions. Moreover, we believe that the coalgebraic framework provides a systematic and principled way to study the relationship between resource models on the semantics side, and substructural logics on the syntactic s…
Canonical models are of central importance in modal logic, in particular as they witness strong completeness and hence compactness. While the canonical model construction is well understood for Kripke semantics, non-normal modal logics often present subtle difficulties - up to the point that canonical models may fail to exist, as is the case e.g. in most probabilistic logics. Here, we present a generic canonical model construction in the semantic framework of coalgebraic modal logic, which pinpoints coherence conditions between syntax and semantics of modal logics that guarantee strong complet…
We present a coalgebraic generalisation of Fischer and Ladner's Propositional Dynamic Logic (PDL) and Parikh's Game Logic (GL). In earlier work, we proved a generic strong completeness result for coalgebraic dynamic logics without iteration. The coalgebraic semantics of such programs is given by a monad T, and modalities are interpreted via a predicate lifting Î whose transpose is a monad morphism from T to the neighbourhood monad. In this paper, we show that if the monad T carries a complete semilattice structure, then we can define an iteration construct, and suitable notions of diamond-like…
This thesis aims to provide a suite of techniques to generate completeness results for coalgebraic logics with axioms of arbitrary rank. We have chosen to investigate the possibility to generalize what is arguably one of the most successful methods to prove completeness results in `classical' modal logic, namely completeness-via-canonicity. This technique is particularly well-suited to a coalgebraic generalization because of its clean and abstract algebraic formalism.
Modal fixpoint logics traditionally play a central role in computer science, in particular in artificial intelligence and concurrency. The mu-calculus and its relatives are among the most expressive logics of this type. However, popular fixpoint logics tend to trade expressivity for simplicity and readability, and in fact often live within the single variable fragment of the mu-calculus. The family of such flat fixpoint logics includes, e.g., LTL, CTL, and the logic of common knowledge. Extending this notion to the generic semantic framework of coalgebraic logic enables covering a wide range o…
A modal logic is \emph{non-iterative} if it can be defined by axioms that do not nest modal operators, and \emph{rank-1} if additionally all propositional variables in axioms are in scope of a modal operator. It is known that every syntactically defined rank-1 modal logic can be equipped with a canonical coalgebraic semantics, ensuring soundness and strong completeness. In the present work, we extend this result to non-iterative modal logics, showing that every non-iterative modal logic can be equipped with a canonical coalgebraic semantics defined in terms of a copointed functor, again ensuri…
Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic interpreted over coalgebras for an arbitrary set functor. We then consider invariance under behavioral equivalence of MSO-formulas. More specifically, we investigate whether the coalgebraic mu-calculus is the bisimulation-invariant fragment of the monadic second-order language for a given functor. Using automatatheoretic techniques and building on recent results by the third author, we show that in order to provide such a characterization result it suffices to find what we call an adequa…
In this paper, we present an abstract framework of many-valued modal logic with the interpretation of atomic propositions and modal operators as predicate lifting over coalgebras for an endofunctor on the category of sets. It generalizes Pattinson's stratification method for colagebraic modal logic to the many-valued setting. In contrast to standard techniques of canonical model construction and filtration, this method employs an induction principle to prove the soundness, completeness, and finite model property of the logics. As a consequence, we can lift a restriction on the previous approac…
An open problem posed by Milner asks for a proof that a certain axiomatisation, which Milner showed is sound with respect to bisimilarity for regular expressions, is also complete. One of the main difficulties of the problem is the lack of a full Kleene theorem, since there are automata that can not be specified, up to bisimilarity, by an expression. Grabmayer and Fokkink (2020) characterise those automata that can be expressed by regular expressions without the constant 1, and use this characterisation to give a positive answer to Milner's question for this subset of expressions. In this pape…
We study the finitary version of the coalgebraic logic introduced by L. Moss. The syntax of this logic, which is introduced uniformly with respect to a coalgebraic type functor, required to preserve weak pullbacks, extends that of classical propositional logic with a so-called coalgebraic cover modality depending on the type functor. Its semantics is defined in terms of a categorically defined relation lifting operation. As the main contributions of our paper we introduce a derivation system, and prove that it provides a sound and complete axiomatization for the collection of coalgebraically v…
Many-valued coalgebraic dynamic logics: Safety and strong completeness via reducibility
Bernoulli Institute for Mathematics, Computer Science and Artificial Intelligence, University of Groningen（格罗宁根大学伯努利数学、计算机科学与人工智能研究所）；Institute of Computer Science of the Czech Academy of Sciences（捷克科学院计算机科学研究所）
DFKI（德国人工智能研究中心）；Universität Bremen（不来梅大学）；Imperial College London（伦敦帝国理工学院）
Hybrid logic extends modal logic with support for reasoning about individual states, designated by so-called nominals. We study hybrid logic in the broad context of coalgebraic semantics, where Kripke frames are replaced with coalgebras for a given functor, thus covering a wide range of reasoning principles including, e.g., probabilistic, graded, default, or coalitional operators. Specifically, we establish generic criteria for a given coalgebraic hybrid logic to admit named canonical models, with ensuing completeness proofs for pure extensions on the one hand, and for an extended hybrid langu…
We present positive coalgebraic logic in full generality, and show how to obtain a positive coalgebraic logic from a boolean one. On the model side this involves canonically computing an endofunctor $T': Pos\to Pos$ from an endofunctor $T: Set\to Set$, in a procedure previously defined by the second author et alii called posetification. On the syntax side, it involves canonically computing a syntax-building functor $L': DL\to DL$ from a syntax-building functor $L: BA\to BA$, in a dual procedure which we call positivication. These operations are interesting in their own right and we explicitly …
Behavioural equivalences can be characterized via bisimulations, modal logics and spoiler-defender games. In this paper we review these three perspectives in a coalgebraic setting, which allows us to generalize from the particular branching type of a transition system. We are interested in qualitative notions (classical bisimulation) as well as quantitative notions (bisimulation metrics). Our first contribution is to introduce a spoiler-defender bisimulation game for coalgebras in the classical case. Second, we introduce such games for the metric case and furthermore define a real-valued modal…
The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we introduce the coalgebraic mu-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability for guarded formulas. Technically, this is achieved by reducing satisfiability to the existence of non-wellfounded tableaux, which is in turn eq…
The coalgebraic $μ$-calculus provides a generic semantic framework for fixpoint logics with branching types beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic $μ$-calculus includes an exponential time upper bound on satisfiability checking, which however requires a well-behaved set of tableau rules for the next-step modalities. Such rules are not available in all cases of interest, in particular ones involving either integer weights as in the graded $μ$-calculus, or real-valued weights in combination with non-linear arithmetic. I…
We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the "powerset monad" on categories, one is the preservation by T of "exactness" of certain squares. Both characterisations are generalisations of the "classical" results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises p…
Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then characterize the behaviors of GKAT expressions in this semantics, leading to a coequation that captures the covariety o…
Positive modal logic was introduced in an influential 1995 paper of Dunn as the positive fragment of standard modal logic. His completeness result consists of an axiomatization that derives all modal formulas that are valid on all Kripke frames and are built only from atomic propositions, conjunction, disjunction, box and diamond. In this paper, we provide a coalgebraic analysis of this theorem, which not only gives a conceptual proof based on duality theory, but also generalizes Dunn's result from Kripke frames to coalgebras for weak-pullback preserving functors. To facilitate this analysis w…
We advocate a declarative approach to proving properties of logic programs. Total correctness can be separated into correctness, completeness and clean termination; the latter includes non-floundering. Only clean termination depends on the operational semantics, in particular on the selection rule. We show how to deal with correctness and completeness in a declarative way, treating programs only from the logical point of view. Specifications used in this approach are interpretations (or theories). We point out that specifications for correctness may differ from those for completeness, as usual…
We study a many-valued generalization of Propositional Dynamic Logic where formulas in states and accessibility relations between states of a Kripke model are evaluated in a finite FL-algebra. One natural interpretation of this framework is related to reasoning about costs of performing structured actions. We prove that PDL over any finite FL-algebra is decidable. We also establish a general completeness result for a class of PDLs based on commutative integral FL-algebras with canonical constants.
We introduce BPDL, a combination of propositional dynamic logic PDL with the basic four-valued modal logic BK studied by Odintsov and Wansing (`Modal logics with Belnapian truth values', J. Appl. Non-Class. Log. 20, 279--301 (2010)). We modify the standard arguments based on canonical models and filtration to suit the four-valued context and prove weak completeness and decidability of BPDL.
After examining the {\bf P} versus {\bf NP} problem against the Kleene-Rosser paradox of the $λ$-calculus [94], it was found that it represents a counter-example to NP-completeness. We prove that it contradicts the proof of Cook's theorem. A logical formalization of the liar's paradox leads to the same result. This formalization of the liar's paradox into a computable form is a 2-valued instance of a fuzzy logic programming paradox discovered in the system of [90]. Three proofs that show that {\bf SAT} is (NOT) NP-complete are presented. The counter-example classes to NP-completeness are also …
We investigate some well-known (and a few not-so-well-known) many-valued logics that have a small number (3 or 4) of truth values. For some of them we complain that they do not have any \emph{logical} use (despite their perhaps having some intuitive semantic interest) and we look at ways to add features so as to make them useful, while retaining their intuitive appeal. At the end, we show some surprising results in the system FDE, and its relationships with features of other logics. We close with some new examples of "synonymous logics." An Appendix contains a natural deduction system for our …
Real-valued logics underlie an increasing number of neuro-symbolic approaches, though typically their logical inference capabilities are characterized only qualitatively. We provide foundations for establishing the correctness and power of such systems. We give a sound and strongly complete axiomatization that can be parametrized to cover essentially every real-valued logic, including all the common fuzzy logics. Our class of sentences are very rich, and each describes a set of possible real values for a collection of formulas of the real-valued logic, including which combinations of real valu…
In [Ban97] a connection among rough sets (in particular, pre-rough algebras) and three-valued Łukasiewicz logic Ł3 is pointed out. In this paper we present a temporal like semantics for Nilpotent Minimum logic NM ([Fod95, EG01]), in which the logic of every instant is given by Ł3: a completeness theorem will be shown. This is the prosecution of the work initiated in [AGM08] and [ABM09], in which the authors construct a temporal semantics for the many-valued logics of Gödel ([Göd32], [Dum59]) and Basic Logic ([Háj98]).
In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic (M-imply) is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4, proved by Ladner, and the Goedel translation from S4 into Intuitionistic Logic, the PSPACE- completeness of M-imply is drawn. The sub-formula principle for a deductive system for a logic L states that whenever F1,...,Fk proves A, there is a proof in which each formula occurrence is either a sub-fo…
Analytic proof calculi are introduced for box and diamond fragments of basic modal fuzzy logics that combine the Kripke semantics of modal logic K with the many-valued semantics of Gödel logic. The calculi are used to establish completeness and complexity results for these fragments.
Constructive S4 modal logics with the finite birelational frame property
IRIT, Toulouse University（图卢兹大学 IRIT）；LERIA, University of Angers（昂热大学 LERIA）；Department of Philosophy, University of Barcelona（巴塞罗那大学哲学系）；Department of Mathematics, Ghent University（根特大学数学系）
Modal logics for reasoning about the power of coalitions capture the notion of effectivity functions associated with game forms. The main goal of coalition logics is to provide formal tools for modeling the dynamics of a game frame whose states may correspond to different game forms. The two classes of effectivity functions studied are the families of playable and truly playable effectivity functions, respectively. In this paper we generalize the concept of effectivity function beyond the yes/no truth scale. This enables us to describe the situations in which the coalitions assess their effect…
Checking the admissibility of quasiequations in a finitely generated (i.e., generated by a finite set of finite algebras) quasivariety Q amounts to checking validity in a suitable finite free algebra of the quasivariety, and is therefore decidable. However, since free algebras may be large even for small sets of small algebras and very few generators, this naive method for checking admissibility in $\Q$ is not computationally feasible. In this paper, algorithms are introduced that generate a minimal (with respect to a multiset well-ordering on their cardinalities) finite set of algebras such t…
Spanish Council for Scientific Research (CSIC)（西班牙国家研究委员会）
Within the possibilistic approach to uncertainty modeling, the paper presents a modal logical system to reason about qualitative (comparative) statements of the possibility (and necessity) of fuzzy propositions. We relate this qualitative modal logic to the many--valued analogues MVS5 and MVKD45 of the well known modal logics of knowledge and belief S5 and KD45 respectively. Completeness results are obtained for such logics and therefore, they extend previous existing results for qualitative possibilistic logics in the classical non-fuzzy setting.
The aim of this paper is to propose a many-valued modal framework to formalize reasoning with both graded preferences and propositions, in the style of van Benthem et al.'s classical modal logics for preferences. To do so, we start from Bou et al.'s minimal modal logic over a finite and linearly ordered residuated lattice. We then define appropriate extensions on a multi-modal language with graded modalities, both for weak and strict preferences, and with truth-constants. Actually, the presence of truth-constants in the language allows us to show that the modal operators Box and Diamond of the…
