Until not too many years ago, all logics except classical logic (and, perhaps, intuitionistic logic too) were considered to be things esoteric. Today this state of a airs seems to have completely been changed. There is a growing interest in many types of nonclassical logics: modal and temporal logics, substructural logics, paraconsistent logics, non-monotonic logics { the list is long. The diversity of systems that have been proposed and studied is so great that a need is felt by many researchers (...) to try to put some order in the present logical jungle. Thus Cl91], Ep90] and Wo88] are three recent books in which an attempt is made to develop a general theoretical framework for the study of logics. On the more pragmatic side, several systems have been developed with the goal of providing a computerized logical framework in which many di erent logical systems can be implemented in a uniform way. An example is the Edinburgh LF( HHP91]). (shrink)

The goal of this paper is to introduce a new Gentzen formulation of the modal logic S5. The history of this problem goes back to the fifties where a counter-example to cut-elimination was given for an otherwise natural and straightforward formulation of S5. Since then, several cut-free Gentzen style formulations of S5 have been given. However, all these systems are technically involved, and furthermore, they differ considerably from Gentzen's original formulation of classical logic. In this paper we give a new (...) sequent system for S5 which is a straightforward and technically simple extension of Gentzen's original sequent system for classical logic. A characteristic feature is the notion of a connection in a proof. The new system satisfies cut-elimination as well as the subformula property. Cut-elimination is proved by giving an algorithm for eliminating cuts. The fact that we give an algorithm for eliminating cuts makes it clear that our system is susceptible to a formulae-as-types computational interpretation. (shrink)

The notion of bilattice was introduced by Ginsberg, and further examined by Fitting, as a general framework for many applications. In the present paper we develop proof systems, which correspond to bilattices in an essential way. For this goal we introduce the notion of logical bilattices. We also show how they can be used for efficient inferences from possibly inconsistent data. For this we incorporate certain ideas of Kifer and Lozinskii, which happen to suit well the context of our work. (...) The outcome are paraconsistent logics with a lot of desirable properties.1. (shrink)

Two families of many-valued modal logics are investigated. Semantically, one family is characterized using Kripke models that allow formulas to take values in a finite many-valued logic, at each possible world. The second family generalizes this to allow the accessibility relation between worlds also to be many-valued. Gentzen sequent calculi are given for both versions, and soundness and completeness are established.

Suppose there are several experts, with some dominating others (expert A dominates expert B if B says something is true whenever A says it is). Suppose, further, that each of the experts has his or her own view of what is possible — in other words each of the experts has their own Kripke model in mind (subject, of course, to the dominance relation that may hold between experts). How will they assign truth values to sentences in a common modal (...) language, and on what sentences will they agree? This problem can be reformulated as one about many-valued Kripke models, allowing many-valued accessibility relations. This is a natural generalization of conventional Kripke models that has only recently been looked at. The equivalence between the many-valued version and the multiple expert one will be formally established. Finally we will axiomatize many-valued modal logics, and sketch a proof of completeness. (shrink)

In their useful logic for a computer network Shramko and Wansing generalize initial values of Belnap’s 4-valued logic to the set 16 to be the power-set of Belnap’s 4. This generalization results in a very specific algebraic structure — the trilattice SIXTEEN 3 with three orderings: information, truth and falsity. In this paper, a slightly different way of generalization is presented. As a base for further generalization a set 3 is chosen, where initial values are a — incoming data is (...) asserted, d — incoming data is denied, and u — incoming data is neither asserted nor denied, that corresponds to the answer “don’t know”. In so doing, the power-set of 3, that is the set 8 is considered. It turns out that there are not three but four orderings naturally defined on the set 8 that form the tetralattice EIGHT 4 . Besides three ordering relations mentioned above it is an extra uncertainty ordering. Quite predictably, the logics generated by a –order (truth order) and d –order (falsity order) coincide with first-degree entailment. Finally logic with two kinds of operations ( a –connectives and d –connectives) and consequence relation defined via a –ordering is considered. An adequate axiomatization for this logic is proposed. (shrink)

We present a cut-admissible system for the modal logic S5 in a formalism that makes explicit and intensive use of deep inference. Deep inference is induced by the methods applied so far in conceptually pure systems for this logic. The system enjoys systematicity and modularity, two important properties that should be satisfied by modal systems. Furthermore, it enjoys a simple and direct design: the rules are few and the modal rules are in exact correspondence to the modal axioms.

In Belnap's useful 4-valued logic, the set 2 = {T, F} of classical truth values is generalized to the set 4 = ������(2) = {Ø, {T}, {F}, {T, F}}. In the present paper, we argue in favor of extending this process to the set 16 = ᵍ (4) (and beyond). It turns out that this generalization is well-motivated and leads from the bilattice FOUR₂ with an information and a truth-and-falsity ordering to another algebraic structure, namely the trilattice SIXTEEN₃ with an (...) information ordering together with a truth ordering and a (distinct) falsity ordering. Interestingly, the logics generated separately by the algebraic operations under the truth order and under the falsity order in SIXTEEN₃ coincide with the logic of FOUR₂, namely first degree entailment. This observation may be taken as a further indication of the significance of first degree entailment. In the present setting, however, it becomes rather natural to consider also logical systems in the language obtained by combining the vocabulary of the logic of the truth order and the falsity order. We semantically define the logics of the two orderings in the extended language and in both cases axiomatize a certain fragment comprising three unary operations: a negation, an involution, and their combination. We also suggest two other definitions of logics in the full language, including a bi-consequence system. In other words, in addition to presenting first degree entailment as a useful 16-valued logic, we define further useful 16-valued logics for reasoning about truth and (non-)falsity. We expect these logics to be an interesting and useful instrument in information processing, especially when we deal with a net of hierarchically interconnected computers. We also briefly discuss Arieli's and Avron's notion of a logical bilattice and state a number of open problems for future research. (shrink)

1.1 In standard modal logics, the worlds are 2-valued in the following sense: there are 2 values that a sentence may take at a world. Technically, however, there is no reason why this has to be the case. The worlds could be many-valued. This paper presents one simple approach to a major family of many-valued modal logics, together with an illustration of why this family is philosophically interesting.

In this paper, we present a simple sequent calculus for the modal propositional logic S5. We prove that this sequent calculus is theoremwise equivalent to the Hilbert-style system S5, that it is contraction-free and cut-free, and finally that it is decidable. All results are proved in a purely syntactic way.

Let K be the least normal modal logic and BK its Belnapian version, which enriches K with ‘strong negation’. We carry out a systematic study of the lattice of logics containing BK based on: • introducing the classes of so-called explosive, complete and classical Belnapian modal logics; • assigning to every normal modal logic three special conservative extensions in these classes; • associating with every Belnapian modal logic its explosive, complete and classical counterparts. We investigate the relationships between special extensions (...) and counterparts, provide certain handy characterisations and suggest a useful decomposition of the lattice of logics containing BK. (shrink)

Various four- and three-valued modal propositional logics are studied. The basic systems are modal extensions BK and BS4 of Belnap and Dunn's four-valued logic of firstdegree entailment. Three-valued extensions of BK and BS4 are considered as well. These logics are introduced semantically by means of relational models with two distinct evaluation relations, one for verification and the other for falsification. Axiom systems are defined and shown to be sound and complete with respect to the relational semantics and with respect to (...) twist structures over modal algebras. Sound and complete tableau calculi are presented as well. Moreover, a number of constructive non-modal logics with strong negation are faithfully embedded into BS4, into its three-valued extension B3S4, or into temporal BS4, BtS4. These logics include David Nelson's three-valued logic N3, the four-valued logic N4 bottom, the connexive logic C, and several extensions of bi-intuitionistic logic by strong negation. (shrink)

The relationships between various modal logics based on Belnap and Dunn’s paraconsistent four-valued logic FDE are investigated. It is shown that the paraconsistent modal logic \, which lacks a primitive possibility operator \, is definitionally equivalent with the logic \, which has both \ and \ as primitive modalities. Next, a tableau calculus for the paraconsistent modal logic KN4 introduced by L. Goble is defined and used to show that KN4 is definitionally equivalent with \ without the absurdity constant. Moreover, (...) a tableau calculus is defined for the modal bilattice logic MBL introduced and investigated by A. Jung, U. Rivieccio, and R. Jansana. MBL is a generalization of BK that in its Kripke semantics makes use of a four-valued accessibility relation. It is shown that MBL can be faithfully embedded into the bimodal logic \ over the non-modal vocabulary of MBL. On the way from \ to MBL, the Fischer Servi-style modal logic \ is defined as the set of all modal formulas valid under a modified standard translation into first-order FDE, and \ is shown to be characterized by the class of all models for \. Moreover, \ is axiomatized and this axiom system is proved to be strongly sound and complete with respect to the class of models for \. Moreover, the notion of definitional equivalence is suitably weakened, so as to show that \ and \ are weakly definitionally equivalent. (shrink)

We shall be concerned with the modal logic BK—which is based on the Belnap–Dunn four-valued matrix, and can be viewed as being obtained from the least normal modal logic K by adding ‘strong negation’. Though all four values ‘truth’, ‘falsity’, ‘neither’ and ‘both’ are employed in its Kripke semantics, only the first two are expressible as terms. We show that expanding the original language of BK to include constants for ‘neither’ or/and ‘both’ leads to quite unexpected results. To be more (...) precise, adding one of these constants has the effect of eliminating the respective value at the level of BK-extensions. In particular, if one adds both of these, then the corresponding lattice of extensions turns out to be isomorphic to that of ordinary normal modal logics. (shrink)

A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.

A modal extension of multilattice logic, called modal multilattice logic, is introduced as a Gentzen-type sequent calculus \. Theorems for embedding \ into a Gentzen-type sequent calculus S4C and vice versa are proved. The cut-elimination theorem for \ is shown. A Kripke semantics for \ is introduced, and the completeness theorem with respect to this semantics is proved. Moreover, the duality principle is proved as a characteristic property of \.

In this paper, bi-intuitionistic multilattice logic, which is a combination of multilattice logic and the bi-intuitionistic logic also known as Heyting–Brouwer logic, is introduced as a Gentzen-type sequent calculus. A Kripke semantics is developed for this logic, and the completeness theorem with respect to this semantics is proved via theorems for embedding this logic into bi-intuitionistic logic. The logic proposed is an extension of first-degree entailment logic and can be regarded as a bi-intuitionistic variant of the original classical multilattice logic (...) determined by the algebraic structure of multilattices. Similar completeness and embedding results are also shown for another logic called bi-intuitionistic connexive multilattice logic, obtained by replacing the connectives of intuitionistic implication and co-implication with their connexive variants. (shrink)

Hypersequent calculus, developed by A. Avron, is one of the most interesting proof systems suitable for nonclassical logics. Although HC has rather simple form, it increases significantly the expressive power of standard sequent calculi. In particular, HC proved to be very useful in the field of proof theory of various nonclassical logics. It may seem surprising that it was not applied to temporal logics so far. In what follows, we discuss different approaches to formalization of logics of linear frames and (...) provide a cut-free HC formalization ofKt4.3, the minimal temporal logic of linear frames, and some of its extensions. The novelty of our approach is that hypersequents are defined not as finite sets but as finite lists of ordinary sequents. Such a solution allows both linearity of time flow, and symmetry of past and future, to be incorporated by means of six temporal rules. Extensions of the basic calculus with simple structural rules cover logics of serial and dense frames. Completeness is proved by Schütte/Hintikka-style argument using models built from saturated hypersequents. (shrink)

We aim at an exposition of some nonstandard cut-free Gentzen formalization for S5, called DSC . DSC operates on two types of sequents instead of one, and shifting of wffs from one side of a sequent to the other is regulated by special rules and subject to some restrictions. Despite of this apparent inconvenience it seems to be simpler than other, known Gentzen-style systems for S5. The number of additional formal machinery is kept in reasonable bounds. Rules have subformula-property, hence (...) constructing of proofs in DSC is quite simple. DSC is a case study of S5 in the wider perspective of MSC , where sequents of arbitrary number of modal types are considered . MSC proves especially useful for obtaining cut-free formalizations of symmetric logics . S5, due to its special properties, allows for many simplifications in the general apparatus of MSC, in particular we cut down on the number of types of sequents and on the number of special, structural rules. (shrink)

Hypersequent calculi can formalize various non-classical logics. In [9] we presented a non-commutative variant of HC for the weakest temporal logic of linear frames Kt4.3 and some its extensions for dense and serial flow of time. The system was proved to be cut-free HC formalization of respective temporal logics by means of Schütte/Hintikka-style semantical argument using models built from saturated hypersequents. In this paper we present a variant of this calculus for Kt4.3 with a constructive syntactical proof of cut elimination.

Shramko [. Truth, falsehood, information and beyond: The American plan generalized. In K. Bimbo, J. Michael Dunn on information based logics, outstanding contributions to logic...

This revised and considerably expanded 2nd edition brings together a wide range of topics, including modal, tense, conditional, intuitionist, many-valued, paraconsistent, relevant, and fuzzy logics. Part 1, on propositional logic, is the old Introduction, but contains much new material. Part 2 is entirely new, and covers quantification and identity for all the logics in Part 1. The material is unified by the underlying theme of world semantics. All of the topics are explained clearly using devices such as tableau proofs, and (...) their relation to current philosophical issues and debates are discussed. Students with a basic understanding of classical logic will find this book an invaluable introduction to an area that has become of central importance in both logic and philosophy. It will also interest people working in mathematics and computer science who wish to know about the area. (shrink)

In this paper I introduce a sequent system for the propositional modal logic S5. Derivations of valid sequents in the system are shown to correspond to proofs in a novel natural deduction system of circuit proofs (reminiscient of proofnets in linear logic, or multiple-conclusion calculi for classical logic). -/- The sequent derivations and proofnets are both simple extensions of sequents and proofnets for classical propositional logic, in which the new machinery—to take account of the modal vocabulary—is directly motivated in terms (...) of the simple, universal Kripke semantics for S5. The sequent system is cut-free and the circuit proofs are normalising. (shrink)