Skip to main content

2010 | Buch

Natural Deduction, Hybrid Systems and Modal Logics

insite
SUCHEN

Über dieses Buch

A good title should be informative enough to illuminate a potential reader on the content of a book. We hope that the present title gives at least some hints of what this book is about. The notion of natural deduction or modal logic are rather well known, but the notion of “hybrid system” certainly needs some explanation. In short, this study may be seen as a kind of search for good deductive systems. We think of systems good in practice which may be applied with easenotonlybywelltrainedlogiciansbutalso, forexample, byphilosophers who need handy deductive tools accompanying their analyses. In parti- lar, we are interested in providing systems that may be widely applied in teaching logic. Nowadays one may observe that several courses in “critical thinking” tend to eliminate courses in practical logic. On the other hand, logic is often taught as a strictly mathematical discipline in very dema- ing courses. It is important to ?ll the gap between these extrema, and the crucial ingredient of any course which is supposed to teach how to use logic, is certainly a suitable deductive system. Since we address this work to a wide audience interested in applications of logic, we were trying to make it self-contained and accessible to a reader with no hard training in logic. The assumed reader should have some ba- ground in logic (an elementary course covering classical propositional and ?rst-order logic with basics of set theory is enough) but not necessarily in modal logic.

Inhaltsverzeichnis

Frontmatter
Chapter 1. Preliminaries
Abstract
This Chapter has an introductory character. The main objective of Section 1.1. has been to recall the basic information on the language of classical propositional logicCPL and on the quantificational logic in classical (CQL) and free version (FQL). The approach chosen here is rather informal. In case of CPL we introduce only the language and syntactical conventions applied throughout, while in case of QL, a brief outline of classical and free logic is additionaly highlighted by some comments concerning philosophical motivations. The section contains also some technical information, e.g. on relations and trees, essential in the foregoing. It should be emphasized that this section is just to establish notation and to keep the text self-contained, so much of it may be skipped in the first reading and consulted when necessary for understanding later chapters.
Andrzej Indrzejczak
Chapter 2. Standard Natural Deduction
Abstract
This Chapter is devoted to the description of standard systems of natural deduction (ND). After historical introduction in Section 2.1 we present some preliminary criteria which should be satisfied by any system of natural deduction. Sections 2.3 and 2.4 develop a systematization of existing systems based on two features: the kind of data used by a system and the format of proof setting. As a result we divide traditional ND systems into F- and S-systems (rules defined on formulae or sequents), and on L- and T-systems (linear or tree proofs). The division is not exhaustive as there may be systems operating on other types of items (e.g. labelled formulae – cf. Chapter 8) The main conclusion of this part is that almost all of the known variants of ND may be traced back to the independent works of Jaśkowski and Gentzen who started the investigation on non-axiomatic deductive systems.
Andrzej Indrzejczak
Chapter 3. Other Deductive Systems
Abstract
The Chapter provides a set of preliminary notes to the next one, where several forms of extended ND systems are discussed. These nonstandard forms of ND are strongly based on solutions occuring in different kinds of deductive systems. Therefore we need to recall some basic information concerning them, which is taken up successively in two sections: the first presents sequent and tableau calculi, systems strongly connected with ND; the second deals with systems popular in automated theorem proving like resolution and Davis/Putnam procedure. It happens that the latter systems are based on the application of cut, whereas the former rather tend to eliminate this rule in practice.
It should be noted that the presentation of different types of deductive systems has an elementary character and is limited in two senses. From the variety of systems we have selected only those that are used further as the source of inspiration in building the enriched versions of ND, particularly in the setting of formalization of modal logic. In result many important kinds of deductive systems like connection calculi, goal oriented proof systems or refutation calculi, are not taken into account. Either we do not know how to take advantage of them for the needs of ND (which is not to say that it is not possible!), or they were not used in modal logic, at least not in the way suitable for our purposes. Moreover, we focus only on some theoretical aspects of the discussed systems that are vital for us. In particular, we focus upon the cut rule and its importance for strategies of proof search, and to some related properties of rules like: subformula property, analyticity, confluency.
The last section of this Chapter contains a discussion of some complexity problems connected with cut and its elimination or bounded application. Again, because of the rudimentary character, much of this Chapter may be skipped in the first reading and consulted when necessary in further lecture.
Andrzej Indrzejczak
Chapter 4. Extended Natural Deduction
Abstract
In this Chapter there is a continual emphasis on the application of ND as a tool of proof search and possibly of automation. In particular, we take up the question of how to make ND a universal system. In order to find satisfactory solutions we compare ND with other types of DS’s. Although ND systems are rather rarely considered in the context of automated deduction they presumably accord with each other and ND systems may be turned into useful automatic proof search procedures. Moreover, even if there are some problems with the construction of efficient ND-based provers, it seems that for the widely understood computer-aided forms of teaching logic, ND should be acknowledged. A good evidence for this claim is provided by the increasing number of proof assistants, tutors, checkers and other interactive programs of this sort based on some forms of ND. Section 4.1. is devoted to the general discussion of these questions, whereas the rest of the Chapter takes up successively the presentation of some concrete, universal and analytic versions of ND for classical and free logic.
Andrzej Indrzejczak
Chapter 5. Survey of Modal Logics
Abstract
This Chapter provides a necessary background for studying applications of ND in modal logics. It is a collection of basic facts needed for understanding of the remaining chapters. Section 5.1. introduces propositional languages of multimodal logics and establishes notational conventions. After a presentation of general taxonomy of modal logics in Section 5.2. we characterize them axiomatically in the next section. Section 5.4. introduces relational semantics for different families of modal logics. Except standard Krikpe’s semantics it contains the basics of neighborhood semantics for weak modal logics. Some attention is paid to correspondence theory and some general schemata investigated later. After short section on completeness and decidability matters we finally present various kinds of first-order modal logic in Section 5.6.
Andrzej Indrzejczak
Chapter 6. Standard Approach to Basic Modal Logics
Abstract
In this Chapter we focus on the class of non-axiomatic systems that are called standard in the sense of keeping intact all the machinery of suitable systems for classical logic. Extensions are obtained by means of additional modal rules. This group covers modal extensions of standard Gentzen SC, Hintikka-style modal TS, and some ND systems.
Andrzej Indrzejczak
Chapter 7. Beyond Basic Logics and Standard Systems
Abstract
This Chapter has a transitional character. We consider several ways of extending standard approach presented in the last Chapter and point out their limitations. Section 7.1. is devoted to an application of standard approach in ND to other modal logics. We discuss them in order of complications they introduce into the structure of ND.
Andrzej Indrzejczak
Chapter 8. Labelled Systems in Modal Logics
Abstract
One of the most important nonstandard approaches to formalization of modal logics is based on the application of labels. This technique is connected not only with modal logics but has a really wide scope of application in several branches of logic. In modal logic labels extend a language with a representation of states in a model. Their addition considerably increase the flexibility of expression.
Andrzej Indrzejczak
Chapter 9. Logics of Linear Frames
Abstract
Logics of linear frames, called here for short linear logics form a particularly interesting and important class, especially in temporal interpretation. But we devote a separate Chapter for their treatment not because of their importance but rather because of special problems generated by their formalization in the setting of labelled systems.
Andrzej Indrzejczak
Chapter 10. Analytic Labelled ND and Proof Search
Abstract
LND system from Chapter 8 allows us to construct simple derivations but is not analytic. We have mentioned in Section 8.5 that one may obtain complete, universal and analytic version similarly as in Chapter 4; by step-wise simulation of every tableau with the help of only elimination rules and analytic applications of cut (i.e. [LRED]).
Andrzej Indrzejczak
Chapter 11. Modal Hybrid Logics
Abstract
In this Chapter we briefly describe a powerfull extension of standard modal logic obtained by some modifications of the language. The fundamental change, forming the basis of the whole family of hybrid languages, involves the addition of special symbols called nominals. They enable explicit reference to states in Kripke models. The name of this approach reflects the fact that nominals are at the same time names of states in a model, and sentences of a modal language.
Andrzej Indrzejczak
Chapter 12. Proof Methods for MHL
Abstract
The final Chapter covers proof theory of hybrid logics. In contrast to the rest of the book, where ND performs a priviliged position, we have tried to present almost all deductive systems constructed so far for hybrid logics and describe their most interesting features. It follows from the author's conviction that on the field of investigation on proof methods for modal logics, the application of hybrid languages instead of standard modal languages may offer a real breakthrough, so careful analysis is vital
Andrzej Indrzejczak
Backmatter
Metadaten
Titel
Natural Deduction, Hybrid Systems and Modal Logics
verfasst von
Andrzej Indrzejczak
Copyright-Jahr
2010
Verlag
Springer Netherlands
Electronic ISBN
978-90-481-8785-0
Print ISBN
978-90-481-8784-3
DOI
https://doi.org/10.1007/978-90-481-8785-0