书目名称 | Proof Methods for Modal and Intuitionistic Logics | 编辑 | Melvin Fitting | 视频video | | 丛书名称 | Synthese Library | 图书封面 |  | 描述 | "Necessity is the mother of invention. " Part I: What is in this book - details. There are several different types of formal proof procedures that logicians have invented. The ones we consider are: 1) tableau systems, 2) Gentzen sequent calculi, 3) natural deduction systems, and 4) axiom systems. We present proof procedures of each of these types for the most common normal modal logics: S5, S4, B, T, D, K, K4, D4, KB, DB, and also G, the logic that has become important in applications of modal logic to the proof theory of Peano arithmetic. Further, we present a similar variety of proof procedures for an even larger number of regular, non-normal modal logics (many introduced by Lemmon). We also consider some quasi-regular logics, including S2 and S3. Virtually all of these proof procedures are studied in both propositional and first-order versions (generally with and without the Barcan formula). Finally, we present the full variety of proof methods for Intuitionistic logic (and of course Classical logic too). We actually give two quite different kinds of tableau systems for the logics we consider, two kinds of Gentzen sequent calculi, and two kinds of natural deduction systems. Each | 出版日期 | Book 1983 | 关键词 | English literature; literature; logic; modal logic; notation; present; proposition; quantifiers | 版次 | 1 | doi | https://doi.org/10.1007/978-94-017-2794-5 | isbn_softcover | 978-90-481-8381-4 | isbn_ebook | 978-94-017-2794-5Series ISSN 0166-6991 Series E-ISSN 2542-8292 | issn_series | 0166-6991 | copyright | Springer Science+Business Media Dordrecht 1983 |
The information of publication is updating
|
|