Many logics in the relevant family can be given a proof theory in the style of Belnap's display logic. However, as originally given, the proof theory is essentially more expressive than the logics they seek to model. In this paper, we consider a modified proof theory which more closely models relevant logics. In addition, we use this proof theory to show decidability for a large range of substructural logics.

A method is presented for constructing natural deduction-style systems for propositional relevant logics. The method consists in first translating formulas of relevant logics into ternary relations, and then defining deduction rules for a corresponding logic of ternary relations. Proof systems of that form are given for various relevant logics. A class of algebras of ternary relations is introduced that provides a relation-algebraic semantics for relevant logics.

A similarity relation is a reflexive and symmetric binary relation between objects. Similarity is relative: it depends on the set of properties of objects used in determining their similarity or dissimilarity. A multi-modal logical language for reasoning about relative similarities is presented. The modalities correspond semantically to the upper and lower approximations of a set of objects by similarity relations corresponding to all subsets of a given set of properties of objects. A complete deduction system for the language is presented.

One of the important issues in research on knowledge based computer systems is development of methods for reasoning about knowledge. In the present paper semantics for knowledge operators is introduced. The underlying logic is developed with epistemic operators relative to indiscernibility. Facts about knowledge expressible in the logic are discussed, in particular common knowledge and joint knowledge of n group of agents. Some paradoxes of epistemic logic are shown to be eliminated in the given system. A formal logical analysis of (...) reasoning about knowledge is a subject of investigations both in logic and computer science, and several epistemic systems have been proposed to formalize the operator ‘an agent knows’. In the present paper we propose a formalization based on a semantic treatment of knowledge within the framework of rough set theory. The inspiration for the underlying epistemic logic came from the analysis of knowledge transfer in distributed systems developed in Orlowska and Sanders and from the author’s earlier work on indiscernibility and relative accessibility semantics. (shrink)

One of the important issues in research on knowledge based computer systems is development of methods for reasoning about knowledge. In the present paper semantics for knowledge operators is introduced. The underlying logic is developed with epistemic operators relative to indiscernibility. Facts about knowledge expressible in the logic are discussed, in particular common knowledge and joint knowledge of n group of agents. Some paradoxes of epistemic logic are shown to be eliminated in the given system. A formal logical analysis of (...) reasoning about knowledge is a subject of investigations both in logic and computer science , and several epistemic systems have been proposed to formalize the operator ‘an agent knows’. In the present paper we propose a formalization based on a semantic treatment of knowledge within the framework of rough set theory . The inspiration for the underlying epistemic logic came from the analysis of knowledge transfer in distributed systems developed in Orlowska and Sanders and from the author’s earlier work on indiscernibility and relative accessibility semantics. (shrink)

This important book provides a new unifying methodology for logic. It replaces the traditional view of logic as manipulating sets of formulas with the notion of structured families of labelled formulas with algebraic structures. This approach has far reaching consequences for the methodology of logics and their semantics, and the book studies the main features of such systems along with their applications. It will interest logicians, computer scientists, philosophers and linguists.

Cut reductions are defined for a Kripke-style formulation of modal logic in terms of indexed systems of sequents. A detailed proof of the normalization (cutelimination) theorem is given. The proof is uniform for the propositional modal systems with all combinations of reflexivity, symmetry and transitivity for the accessibility relation. Some new transformations of derivations (compared to standard sequent formulations) are needed, and some additional properties are to be checked. The display formulations [1] of the systems considered can be presented as (...) encodings of Kripke-style formulations. (shrink)

The purpose of the present paper is to show that modal propositional logics can be interpreted in a logic based on relational calculus. We consider languages with necessity operators [R], where R is an accessibility relation expression representing an element of the algebra of binary relations with operations −,∪,∩, −1 , ◦. The relational logic is based on relational calculus enriched by operations of weakest prespecification and weakest postspecification introduced in Hoare and He Jifeng and investigated in He Jifeng et (...) al . The logic is an extension of the system introduced in Or lowska and investigated in Buszkowski and Or lowska. (shrink)

We investigate the effect on the complexity of adding the universal modality and the reflexive transitive closure modality to modal logics. From the examples in the literature, one might conjecture that adding the reflexive transitive closure modality is at least as hard as adding the universal modality, and that adding either of these modalities to a multi-modal logic where the modalities do not interact can only increase the complexity to EXPTIME-complete. We show that the first conjecture holds under reasonable assumptions (...) and that, except for a number of special cases which we fully characterize, the hardness part of the second conjecture is true. However, the upper bound part of the second conjecture fails miserably: we show that there exists a uni-modal, decidable, finitely axiomatizable, and canonical logic for which adding the universal modality causes undecidability and for which adding the reflexive transitive closure modality causes high undecidability. (shrink)

Substructural logics are traditionally obtained by dropping some or all of the structural rules from Gentzen's sequent calculi LK or LJ. It is well known that the usual logical connectives then split into more than one connective. Alternatively, one can start with the Lambek calculus, which contains these multiple connectives, and obtain numerous logics like: exponential-free linear logic, relevant logic, BCK logic, and intuitionistic logic, in an incremental way. Each of these logics also has a classical counterpart, and some also (...) have a 'cyclic' counterpart. These logics have been studied extensively and are quite well understood.Generalising further, one can start with intuitionistic Bi-Lambek logic, which contains the dual of every connective from the Lambek calculus. The addition of the structural rules then gives Bi-linear, Bi-relevant, Bi-BCK and Bi-intuitionistic logic, again in an incremental way. Each of these logics also has a classical counterpart, and some even have a 'cyclic' counterpart. These extensions of Bi-Lambek logic are not so well understood. Cut-elimination for Classical Bi-Lambek logic, for example, is not completely clear since some cut rules have side conditions requiring that certain constituents be empty or non-empty.The display logic of Nuel Belnap is a general Gentzen-style proof theoretical framework designed to capture many different logics in one uniform setting. The beauty of display logic is a general cut-elimination theorem, due to Belnap, which applies whenever the rules of the display calculus obey certain, easily checked, conditions. The original display logic, and its various incarnations, are not suitable for capturing bi-intuitionistic and bi-classical logics in a uniform way. We remedy this situation by giving a single Display calculus for the Bi-Lambek Calculus, from which all the well-known extensions are obtained by the incremental addition of structural rules to a constant core of logical introduction rules.We highlight the inherent duality and symmetry within this framework obtaining 'four proofs for the price of one'. We give algebraic semantics for the Bi-Lambek logics and prove that our calculi are sound and complete with respect to these semantics. We show how to define an alternative display calculus for bi-classical substructural logics using negations, instead of implications, as primitives.Borrowing from other display calculi, we show how to extend our display calculus to handle bi-intuitionistic or bi-classical substructural logics containing the forward and backward modalities familiar from tense logic, the exponentials of linear logic, the converse operator familiar from relation algebra, four negations, and two unusual modalities corresponding to the non-classical analogues of Sheffer's 'dagger' and 'stroke', all in a modular way.Using the Gaggle Theory of Dunn we outline relational semantics for the binary and unary intensional connectives, but make no attempt to do so for the extensional connectives, or the exponentials.Finally, we flesh out a suggestion of Lambek to embed intuitionistic logic using two unusual 'exponentials', and show that these 'exponentials' are essentially tense logical modalities, quite at odds with the usual exponentials.Using a refinement of the display property, you can pick and choose from these possibilities to construct a display calculus for your needs. (shrink)

ABSTRACT In this paper we introduce and investigate various classes of multimodal logics based on frames with relative accessibility relations. We discuss their applicability to representation and analysis of incomplete information. We provide axiom systems for these logics and we prove their completeness.

We study a knowledge logic that assumes that to each set of agents, an indiscernibility relation is associated and the agents decide the membership of objects or states up to this indiscernibility relation. Its language contains a family of relative knowledge operators. We prove the decidability of the satisfiability problem, we show its EXPTIME-completeness and as a side-effect, we define a complete Hilbert-style axiomatization.