Labelled Non-Classical Logics

by Vigano, Luca

• ISBN13: 9780792377498
• ISBN10: 0792377494
• Format: Hardcover
• Copyright: 2000-01-01
• Publisher: Kluwer Academic Pub

Summary

The subject of Labelled Non-Classical Logics is the development and investigation of a framework for the modular and uniform presentation and implementation of non-classical logics, in particular modal and relevance logics. Logics are presented as labelled deduction systems, which are proved to be sound and complete with respect to the corresponding Kripke-style semantics. We investigate the proof theory of our systems, and show them to possess structural properties such as normalization and the subformula property, which we exploit not only to establish advantages and limitations of our approach with respect to related ones, but also to give, by means of a substructural analysis, a new proof-theoretic method for investigating decidability and complexity of (some of) the logics we consider. All of our deduction systems have been implemented in the generic theorem prover Isabelle, thus providing a simple and natural environment for interactive proof development. Labelled Non-Classical Logics is essential reading for researchers and practitioners interested in the theory and applications of non-classical logics.

Author Biography

Luca Vigan+¦ is an assistant professor at the Institute for Computer Science of the University of Freiburg (Germany). His research focuses on the theory and applications of non-classical logics, of proof development systems, of logical frameworks, and of logics for security.

Table of Contents

List of Figures	vii
List of Tables	ix
Acknowledgments	xi
Foreword	xiii
Introduction	1	(16)
Background and motivation	1	(2)
Contribution	3	(9)
Main results	12	(1)
Synopsis	13	(4)
Part I Labelled deduction for non-classical logics
Labelled Natural Deduction Systems for Propositional Modal Logics	17	(36)
A modular presentation of propositional modal logics	18	(11)
Soundness and completeness	29	(8)
Normalization and its consequences	37	(16)
Labelled Natural Deduction Systems for Propositional Non-Classical Logics	53	(38)
Modular presentations of propositional non-classical logics	54	(17)
Soundness and completeness	71	(10)
Normalization and its consequences	81	(10)
Labelled Natural Deduction Systems for Quantified Modal Logics	91	(24)
A modular presentation of quantified modal logics	93	(7)
Soundness and completeness	100	(7)
Normalization and its consequences	107	(8)
Encoding Labelled Non-Classical Logics in Isabelle	115	(22)
Encoding propositional modal logics	115	(11)
Encoding propositional non-classical logics	126	(5)
Encoding quantified modal logics	131	(6)
Labelled Sequent Systems for Non-Classical Logics	137	(20)
Labelled sequent systems for propositional modal logics	138	(9)
Labelled sequent systems for non-classical logics	147	(2)
Equivalence of labelled natural deduction and sequent systems	149	(8)
Discussion	157	(10)
Related work	157	(10)
Part II Substructural and complexity analysis of modal sequent systems
Introduction and Preliminaries	167	(20)
Introduction	167	(3)
Preliminary results	170	(17)
Substructural Analysis of S(K)	187	(14)
Eliminating contractions in S(K)	187	(8)
S(K) and SS(K)	195	(6)
Substructural Analysis of S(T)	201	(22)
Bounding contractions in S(T)	201	(18)
S(T) and SS(T)	219	(4)
Substructural Analysis of S(K4) And S(S4)	223	(24)
Infinite chains, infinite branches and periodicity	225	(5)
Bounding contraction in S(K4) and S(S4)	230	(8)
S(K4) and SS(K4)	238	(7)
S(S4) and SS(S4)	245	(2)
Complexity of Proof Search in K, T, K4 and S4	247	(6)
Summary of our substructural analysis	247	(1)
Complexity of proof search in K	248	(2)
Complexity of proof search in T	250	(1)
Complexity of proof search in K4 and S4	251	(2)
Discussion	253	(10)
Related work	253	(10)
Conclusions and Further Research	263	(4)
References	267	(16)
Index	283