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)

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.

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)

The paper contains an exposition of some non standard approach to gentzenization of modal logics. The first section is devoted to short discussion of desirable properties of Gentzen systems and the short review of various sequential systems for modal logics. Two non standard, cut-free sequent systems are then presented, both based on the idea of using special modal sequents, in addition to usual ones. First of them, GSC I is well suited for nonsymmetric modal logics The second one, GSC II (...) is devised specially for symmetric, i.e. Blogics. GSC I and GSC II are not different formalizations, from the theoretical point of view GSC I may be seen as a simplification of the more general approach present in GSC II. They are considered separately, mainly because Blogics demand different, and more complicated, strategy in completeness proof, whereas non symmetric logics are easily and uniformly characterised by means of Fitting's Consistency Properties. The weakest modal logic captured by this formalization is minimal regular logic C, but many stronger logics are obtainable by addition of suitable structural rules, which conforms to Do en's methodology. Both variants of GSC satisfy also other, besides cut-freedom, desirable properties. (shrink)