Natural deduction, hybrid systems and modal logics (Q659458)

The first part of the book (Chapters 1--4) deals with natural deduction systems in standard and extended form. Chapter 1 contains preliminaries (a reader of the book does not need to have a hard training in logic -- only some background in classical propositional and first-order logic and set theory, but not modal logic) such as classical and free logic, deductive systems, rules and proofs. Chapter 2 is devoted to standard natural deduction (origins, data structures, trees, sequences, the system of Kalish and Montague, and natural deduction for first-order logic). Chapter 3 deals with sequent systems and tableaux, resolution, the Davis/Putman system, cut and proof complexity. The last chapter of this part is devoted to extended natural deduction (its analytic and universal versions, resolution-based natural deduction). The second part of the book (Chapters 5--7) deals with modal logics and their formalization in standard natural deduction systems. Chapter 5 brings a survey of modal logics (basic modal logic and tense language, modal logics in general, an axiomatic approach to modal logics, relational semantics, completeness, decidability, complexity and first-order modal logics). Chapter 6 presents the standard formalization of modal logics in sequent and tableau calculi and surveys different approaches to the construction of natural deduction for modal logics. Chapter 7 deals with other possible extensions (beyond basic normal logics, limitations of the standard approach, redundancy of standard systems, two variants of RND systems (systems with only one proof construction rule called Subsumption) for logics and nonstandard deductive systems). The last part is devoted to a detailed exploration of one of the nonstandard approaches to the formalization of modal logics, based on application of labels. Chapter 8 deals with labeled systems in modal logic and Chapter 9 with logics of linear frames. Chapter 10 is devoted to analytic labeled deduction systems and proof search and the next two chapters deal with modal hybrid logics and their proof theory, respectively.