## Labelled Non-Classical LogicsI am very happy to have this opportunity to introduce Luca Vigano's book on Labelled Non-Classical Logics. I put forward the methodology of labelled deductive systems to the participants of Logic Colloquium'90 (Labelled Deductive systems, a Position Paper, In J. Oikkonen and J. Vaananen, editors, Logic Colloquium '90, Volume 2 of Lecture Notes in Logic, pages 66-68, Springer, Berlin, 1993), in an attempt to bring labelling as a recognised and significant component of our logic culture. It was a response to earlier isolated uses of labels by various distinguished authors, as a means to achieve local proof theoretic goals. Labelling was used in many different areas such as resource labelling in relevance logics, prefix tableaux in modal logics, annotated logic programs in logic programming, proof tracing in truth maintenance systems, and various side annotations in higher-order proof theory, arithmetic and analysis. This widespread local use of labels was an indication of an underlying logical pattern, namely the simultaneous side-by-side manipulation of several kinds of logical information. It was clear that there was a need to establish the labelled deductive systems methodology. Modal logic is one major area where labelling can be developed quickly and sys tematically with a view of demonstrating its power and significant advantage. In modal logic the labels can play a double role. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

INTRODUCTION | 1 |

12 CONTRIBUTION | 3 |

13 MAIN RESULTS | 12 |

14 SYNOPSIS | 13 |

LABELLED NATURAL DEDUCTION SYSTEMS FOR PROPOSITIONAL MODAL LOGICS | 17 |

21 A MODULAR PRESENTATION OF PROPOSITIONAL MODAL LOGICS | 18 |

22 SOUNDNESS AND COMPLETENESS | 29 |

23 NORMALIZATION AND ITS CONSEQUENCES | 37 |

63 EQUIVALENCE OF LABELLED NATURAL DEDUCTION AND SEQUENT SYSTEMS | 149 |

DISCUSSION | 157 |

INTRODUCTION AND PRELIMINARIES | 167 |

82 PRELIMINARY RESULTS | 170 |

SUBSTRUCTURAL ANALYSIS OF SK | 187 |

92 SK AND SSK | 195 |

SUBSTRUCTURAL ANALYSIS OF ST | 201 |

102 ST AND SST | 219 |

LABELLED NATURAL DEDUCTION SYSTEMS FOR PROPOSITIONAL NONCLASSICAL LOGICS | 53 |

31 MODULAR PRESENTATIONS OF PROPOSITIONAL NONCLASSICAL LOGICS | 54 |

32 SOUNDNESS AND COMPLETENESS | 71 |

33 NORMALIZATION AND ITS CONSEQUENCES | 81 |

LABELLED NATURAL DEDUCTION SYSTEMS FOR QUANTIFIED MODAL LOGICS | 91 |

41 A MODULAR PRESENTATION OF QUANTIFIED MODAL LOGICS | 93 |

42 SOUNDNESS AND COMPLETENESS | 100 |

43 NORMALIZATION AND ITS CONSEQUENCES | 107 |

ENCODING LABELLED NONCLASSICAL LOGICS IN ISABELLE | 115 |

52 ENCODING PROPOSITIONAL NONCLASSICAL LOGICS | 126 |

53 ENCODING QUANTIFIED MODAL LOGICS | 131 |

LABELLED SEQUENT SYSTEMS FOR NONCLASSICAL LOGICS | 137 |

61 LABELLED SEQUENT SYSTEMS FOR PROPOSITIONAL MODAL LOGICS | 138 |

62 LABELLED SEQUENT SYSTEMS FOR NONCLASSICAL LOGICS | 147 |

SUBSTRUCTURAL ANALYSIS OF SK4 AND SS4 | 223 |

111 INFINITE CHAINS INFINITE BRANCHES AND PERIODICITY | 225 |

112 BOUNDING CONTRACTION IN SK4 AND SS4 | 230 |

113 SK4 AND SSK4 | 238 |

114 SS4 AND SSS4 | 245 |

COMPLEXITY OF PROOF SEARCH IN K T K4 AND S4 | 247 |

122 COMPLEXITY OF PROOF SEARCH IN K | 248 |

123 COMPLEXITY OF PROOF SEARCH IN T | 250 |

124 COMPLEXITY OF PROOF SEARCH IN K4 AND S4 | 251 |

DISCUSSION | 253 |

CONCLUSIONS AND FURTHER RESEARCH | 263 |

267 | |

283 | |

### Other editions - View all

### Common terms and phrases

accessibility relation active rwff application of DL applications of C1L assumption axiom schemas base system bound branch conclude consider contains define Definition domain theory elimination rule encoding equivalent example falsum first-order logic follows h xi:D Hilbert systems Horn relational rules Horn relational theories I=OT implies induction hypothesis introduced intuitionistic logic Isabelle Iwffs Kripke frames Kripke semantics labelled ND systems labelled sequent systems labelling algebra left contractions Lemma lwffs metalogic modal operators modular monl multiset N(QK natural deduction natural deduction systems nbs(S negation non-classical logics normal derivation normal form notation pbs(S permute premise present principal formula proof context proof-theoretical propositional modal logics propositional non-classical logics propositional variable provable prove quantified modal logics relevance logics require restrict rtac semantic embedding Skolem function sound and complete subderivations subformula property subgoals substructural analysis substructural logics t=OT Theorem transform weakening x:OA xi+i