We introduce a complete many-valued semantics for two normal lattice-based modal logics. This semantics is based on reflexive many-valued graphs. We discuss an interpretation and possible applications of this logical framework in the context of the formal analysis of the interaction between (competing) scientific theories.

@en

We introduce a proper multi-type display calculus for bilattice logic (with conflation) for which we prove soundness, completeness, conservativity, standard subformula property and cut elimination. Our proposal builds on the product representation of bilattices and applies the guidelines of the multi-type methodology in the design of display calculi.

@en

We introduce proper display calculi for basic monotonic modal logic, the conditional logic CK and a number of their axiomatic extensions. These calculi are sound, complete, conservative and enjoy cut elimination and subformula property. Our proposal applies the multi-type methodology in the design of display calculi, starting from a semantic analysis based on the translation from monotonic modal logic to normal bi-modal logic.

@en

In recent years, unified correspondence has been developed as a generalized Sahlqvist theory which applies uniformly to all signatures of normal and regular (distributive) lattice expansions. A fundamental tool for attaining this level of generality and uniformity is a principled way, based on order theory, to define the Sahlqvist and inductive formulas and inequalities in every such signature. This definition covers in particular all (bi-)intuitionistic modal logics. The theory of these logics has been intensively studied over the past seventy years in connection with classical polyadic modal logics, using versions of Gödel-McKinsey- Tarski translations, suitably defined in each signature, as main tools. In view of this state-of-the-art, it is natural to ask (1) whether a general perspective on Gödel-McKinsey- Tarski translations can be attained, also based on order-theoretic principles like those underlying the general definition of Sahlqvist and inductive formulas and inequalities, which accounts for the known Gödel-McKinsey-Tarski translations and applies uniformly to all signatures of normal (distributive) lattice expansions; (2) whether this general perspective can be used to transfer correspondence and canonicity theorems for Sahlqvist and inductive formulas and inequalities in all signatures described above under Gödel-McKinsey-Tarski translations. In the present paper, we set out to answer these questions. We answer (1) in the armative; as to (2), we prove the transfer of the correspondence theorem for inductive inequalities of arbitrary signatures of normal distributive lattice expansions. We also prove the transfer of canonicity for inductive inequalities, but only restricted to arbitrary normal modal expansions of bi-intuitionistic logic. We also analyze the difficulties involved in obtaining the transfer of canonicity outside this setting, and indicate a route to extend the transfer of canonicity to all signatures of normal distributive lattice expansions.

@en

By ‘informational entropy’, we understand an inherent boundary to knowability, due e.g. to perceptual, theoretical, evidential or linguistic limits. In this paper, we discuss a logical framework in which this boundary is incorporated into the semantic and deductive machinery, and outline how this framework can be used to model various situations in which informational entropy arises.

@en

Taking an algebraic perspective on the basic structures of Rough Concept Analysis as the starting point, in this paper we introduce some varieties of lattices expanded with normal modal operators which can be regarded as the natural rough algebra counterparts of certain subclasses of rough formal contexts, and introduce proper display calculi for the logics associated with these varieties which are sound, complete, conservative and with uniform cut elimination and subformula property. These calculi modularly extend the multi-type calculi for rough algebras to a ‘nondistributive’ (i.e. general lattice-based) setting.

@en

We extend the theory of unified correspondence to a broad class of logics with algebraic semantics given by varieties of normal lattice expansions (LEs), also known as ‘lattices with operators’. Specifically, we introduce a syntactic definition of the class of Sahlqvist formulas and inequalities which applies uniformly to each LE-signature and is given purely in terms of the order-theoretic properties of the algebraic interpretations of the logical connectives. We also introduce the algorithm ALBA, parametric in each LE-setting, which effectively computes first-order correspondents of LE-inequalities, and is guaranteed to succeed on a wide class of inequalities (the so-called inductive inequalities) which significantly extend the Sahlqvist class. Further, we show that every inequality on which ALBA succeeds is canonical. Projecting these results on specific signatures yields state-of-the-art correspondence and canonicity theory for many well known modal expansions of classical and intuitionistic logic and for substructural logics, from classical poly-modal logics to (bi-)intuitionistic modal logics to the Lambek calculus and its extensions, the Lambek-Grishin calculus, orthologic, the logic of (not necessarily distributive) De Morgan lattices, and the multiplicative-additive fragment of linear logic.

@en

In the present paper, we endow the logics of topological quasi Boolean algebras, topological quasi Boolean algebras 5, intermediate algebras of types 1-3, and pre-rough algebras with proper multi-type display calculi which are sound, complete, conservative, and enjoy cut elimination and subformula property. Our proposal builds on an algebraic analysis and applies the principles of the multi-type methodology in the design of display calculi.

@en

We present a software tool for reasoning in and about propositional sequent calculi for modal logics of actions. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. The tool generates embeddings of the calculus in the theorem prover Isabelle/HOL for formalising proofs about D.EAK. Integrating propositional reasoning in D.EAK with inductive reasoning in Isabelle/HOL, we verify the solution of the muddy children puzzle for any number of muddy children. There also is a set of meta-tools that allows us to adapt the software for a wide variety of user defined calculi.

@en

We introduce the logic LRC, designed to describe and reason about agents’ abilities and capabilities in using resources. The proposed framework bridges two—up to now—mutually independent strands of literature: the one on logics of abilities and capabilities, developed within the theory of agency, and the one on logics of resources, motivated by program semantics. The logic LRC is suitable to describe and reason about key aspects of social behaviour in organizations. We prove a number of properties enjoyed by LRC (soundness, completeness, canonicity, and disjunction property) and its associated analytic calculus (conservativity, cut elimination, and subformula property). These results lay at the intersection of the algebraic theory of unified correspondence and the theory of multitype calculi in structural proof theory. Case studies are discussed which showcase several ways in which this framework can be extended and enriched while retaining its basic properties, so as to model an array of issues, both practically and theoretically relevant, spanning from planning problems to the logical foundations of the theory of organizations.

@en

We extend unified correspondence theory to Kripke frames with impossible worlds and their associated regular modal logics. These are logics the modal connectives of which are not required to be normal: only the weaker properties of additivity ◊x∨◊y=◊(x∨y) and multiplicativity □x∧□y=□(x∧y) are required. Conceptually, it has been argued that their lacking necessitation makes regular modal logics better suited than normal modal logics at the formalization of epistemic and deontic settings. From a technical viewpoint, regularity proves to be very natural and adequate for the treatment of algebraic canonicity Jónsson-style. Indeed, additivity and multiplicativity turn out to be key to extend Jónsson’s original proof of canonicity to the full Sahlqvist class of certain regular distributive modal logics naturally generalizing distributive modal logic. Most interestingly, additivity and multiplicativity are key to Jónsson-style canonicity also in the original (i.e. normal DML. Our contributions include: the definition of Sahlqvist inequalities for regular modal logics on a distributive lattice propositional base; the proof of their canonicity following Jónsson’s strategy; the adaptation of the algorithm ALBA to the setting of regular modal logics on two non-classical (distributive lattice and intuitionistic) bases; the proof that the adapted ALBA is guaranteed to succeed on a syntactically defined class which properly includes the Sahlqvist one; finally, the application of the previous results so as to obtain proofs, alternative to Kripke’s, of the strong completeness of Lemmon’s epistemic logics E2-E5 with respect to elementary classes of Kripke frames with impossible worlds. @en

The theory of canonical extensions typically considers extensions of maps A→B to maps Aδ→Bδ. In the present article, the theory of canonical extensions of maps A→Bδ to maps Aδ→Bδ is developed, and is applied to obtain a new canonicity proof for those inequalities in the language of Distributive Modal Logic (DML) on which the algorithm ALBA [9] is successful. @en

In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.

@en

We establish a formal connection between algorithmic correspondence theory and certain dual characterization results for finite lattices, similar to Nation's characterization of a hierarchy of pseudovarieties of finite lattices, progressively generalizing finite distributive lattices. This formal connection is mediated through monotone modal logic. Indeed, we adapt the correspondence algorithm ALBA to the setting of monotone modal logic, and we use a certain duality-induced encoding of finite lattices as monotone neighbourhood frames to translate lattice terms into formulas in monotone modal logic.

@en

Categorization systems are widely studied in psychology, sociology, and organization theory as information-structuring devices which are critical to decision-making processes. In the present paper, we introduce a sound and complete epistemic logic of categories and agents' categorical perception. The Kripke-style semantics of this logic is given in terms of data structures based on two domains: one domain representing objects (e.g. market products) and one domain representing the features of the objects which are relevant to the agents' decision-making. We use this framework to discuss and propose logic-based formalizations of some core concepts from psychological, sociological, and organizational research in categorization theory.

@en

The present article provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. Dynamic epistemic logic is one of the best known members of a family of logical systems that have been successfully applied to diverse scientific disciplines, but the proof-theoretic treatment of which presents many difficulties. After an illustration of the proof-theoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display calculi, a proof-theoretic paradigm that has been successfully employed to give a proof-theoretic semantic account of modal and substructural logics. Then, we review some of the most significant proposals of proof systems for dynamic epistemic logics, and we critically reflect on them in the light of the previously introduced proof-theoretic semantic principles. The contributions of the present article include a generalization of Belnap's cut-elimination metatheorem for display calculi, and a revised version of the display-style calculus D.EAK [30]. We verify that the revised version satisfies the previously mentioned proof-theoretic semantic principles, and show that it enjoys cut-elimination as a consequence of the generalized metatheorem.

@en

The present article aims at establishing formal connections between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap. These connections have been seminally observed and exploited by Marcus Kracht, in the context of his characterization of the modal axioms (which he calls primitive formulas) which can be effectively transformed into ‘analytic’ structural rules of display calculi. In this context, a rule is ‘analytic’ if adding it to a display calculus preserves Belnap’s cut-elimination theorem. In recent years, the state-of-the-art in correspondence theory has been uniformly extended from classical modal logic to diverse families of non-classical logics, ranging from (bi-)intuitionistic (modal) logics, linear, relevant and other substructural logics, to hybrid logics and mu-calculi. This generalization has given rise to a theory called unified correspondence, the most important technical tools of which are the algorithm ALBA, and the syntactic characterization of Sahlqvist-type classes of formulas and inequalities which is uniform in the setting of normal DLE-logics (logics the algebraic semantics of which is based on bounded distributive lattices). We apply unified correspondence theory, with its tools and insights, to extend Kracht’s results and prove his claims in the setting of DLE-logics. The results of the present article characterize the space of properly displayable DLE-logics. @en

RS-frames were introduced by Gehrke as relational semantics for substructural logics. They are two-sorted structures, based on RS-polarities with additional relations used to interpret modalities. We propose an intuitive, epistemic interpretation of RS-frames for modal logic, in terms of categorization systems and agents’ subjective interpretations of these systems. Categorization systems are a key to any decision-making process and are widely studied in the social and management sciences. A set of objects together with a set of properties and an incidence relation connecting objects with their properties forms a polarity which can be ‘pruned’ into an RS-polarity. Potential categories emerge as the Galois-stable sets of this polarity, just like the concepts of Formal Concept Analysis. An agent’s beliefs about objects and their properties (which might be partial) is modelled by a relation which gives rise to a normal modal operator expressing the agent’s beliefs about category membership. Fixed-points of the iterations of the belief modalities of all agents are used to model categories constructed through social interaction.

@en

In the present article, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The display approach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag-Moss-Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination.

@en