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.

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 provide a general investigation of Logic in which the notion of a simple consequence relation is taken to be fundamental. Our notion is more general than the usual one since we give up monotonicity and use multisets rather than sets. We use our notion for characterizing several known logics (including Linear Logic and non-monotonic logics) and for a general, semantics-independent classi cation of standard connectives via equations on consequence relations (these include Girard's \multiplicatives" and \additives"). We next investigate the (...) standard methods for uniformly representing consequence relations: Hilbert type, Natural Deduction and Gentzen type. The advantages and disadvantages of using each system and what should be taken as.. (shrink)

The purpose of this work is to present Gentzen-style formulations of S5 and S4 based on sequents of higher levels. Sequents of level 1 are like ordinary sequents, sequents of level 1 have collections of sequents of level 1 on the left and right of the turnstile, etc. Rules for modal constants involve sequents of level 2, whereas rules for customary logical constants of first-order logic with identity involve only sequents of level 1. A restriction on Thinning on the right (...) of level 2, which when applied to Thinning on the right of level 1 produces intuitionistic out of classical logic (without changing anything else), produces S4 out of S5 (without changing anything else). This characterization of modal constants with sequents of level 2 is unique in the following sense. If constants which differ only graphically are given a formally identical characterization, they can be shown inter-replaceable (not only uniformly) with the original constants salva provability. Customary characterizations of modal constants with sequents of level 1, as well as characterizations in Hilbert-style axiomatizations, are not unique in this sense. This parallels the case with implication, which is not uniquely characterized in Hilbert-style axiomatizations, but can be uniquely characterized with sequents of level 1. These results bear upon theories of philosophical logic which attempt to characterize logical constants syntactically. They also provide an illustration of how alternative logics differ only in their structural rules, whereas their rules for logical constants are identical. (shrink)

From the reviews: "A good textbook can improve a lecture course enormously, especially when the material of the lecture includes many technical details. Van Dalen's book, the success and popularity of which may be suspected from this steady interest in it, contains a thorough introduction to elementary classical logic in a relaxed way, suitable for mathematics students who just want to get to know logic. The presentation always points out the connections of logic to other parts of mathematics. The reader (...) immediately see the logic is "just another branch of mathematics" and not something more sacred." Acta Scientiarum Mathematicarum, Hungary. (shrink)

This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much (...) more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included. (shrink)

8.3 The consistency proof -- 8.4 Applications of the consistency proof -- 8.5 Second-order arithmetic -- Problems -- Chapter 9: Set Theory -- 9.1 Axioms for sets -- 9.2 Development of set theory -- 9.3 Ordinals -- 9.4 Cardinals -- 9.5 Interpretations of set theory -- 9.6 Constructible sets -- 9.7 The axiom of constructibility -- 9.8 Forcing -- 9.9 The independence proofs -- 9.10 Large cardinals -- Problems -- Appendix The Word Problem -- Index.

This volume presents the proceedings of the First International Static Analysis Symposium (SAS '94), held in Namur, Belgium in September 1994. The proceedings comprise 25 full refereed papers selected from 70 submissions as well as four invited contributions by Charles Consel, Saumya K. Debray, Thomas W. Getzinger, and Nicolas Halbwachs. The papers address static analysis aspects for various programming paradigms and cover the following topics: generic algorithms for fixpoint computations; program optimization, transformation and verification; strictness-related analyses; type-based analyses and type (...) inference; dependency analyses and abstract domain construction. (shrink)

This paper gives an overview on translation methods we have developed for nonclassical logics, in particular for modal logics. Optimized ‘functional’ and semi-functional translation into predicate logic is described. Using normal modal logic as an intermediate logic, other logics can be translated into predicate logic as well. As an example, the translation of modal logic of graded modalities is sketched. In the second part of the paper it is shown how to translate Hilbert axioms into properties of the semantic structure (...) and vice versa., i.e. we can automate important parts of correspondence theory. The exact formalisms and the soundness and completeness proofs can be found in the original papers. (shrink)

Masini, A., 2-Sequent calculus: a proof theory of modalities, Annals of Pure and Applied Logic 58 229–246. In this work we propose an extension of the Getzen sequent calculus in order to deal with modalities. We extend the notion of a sequent obtaining what we call a 2-sequent. For the obtained calculus we prove a cut elimination theorem.

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.