Labelled Non-Classical LogicsSpringer Science & Business Media, 31 de jan. de 2000 - 291 páginas I 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. |
Conteúdo
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 | |
Outras edições - Ver todos
Termos e frases comuns
A₁ accessibility relation active rwff AN(c applications of CIL assumption axiom schemas AxRy base system bound branch consider define Definition domain theory elimination rule encoding equivalent example extend falsum first-order logic FN(c follows Hilbert systems Horn relational rules Horn relational theories II₁ implies induction hypothesis introduced intuitionistic logic Isabelle 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 form obtain pbs(S permute premise principal formula proof context proof-theoretical propositional modal logics propositional non-classical logics propositional variable provable prove quantified modal logics Rabc refl relevance logics restrict rtac semantic embedding Skolem function sound and complete subderivations subformula property subgoals substructural logics T₁ Theorem transform x:OA x:OB x₁:D xi+1 xRyxRy Πι Πο г₁