© 1983

Proof Methods for Modal and Intuitionistic Logics


Part of the Synthese Library book series (SYLI, volume 169)

Table of contents

  1. Front Matter
    Pages i-viii
  2. Melvin Fitting
    Pages 1-10
  3. Melvin Fitting
    Pages 11-32
  4. Melvin Fitting
    Pages 118-190
  5. Melvin Fitting
    Pages 191-261
  6. Melvin Fitting
    Pages 262-331
  7. Melvin Fitting
    Pages 332-385
  8. Melvin Fitting
    Pages 386-436
  9. Melvin Fitting
    Pages 437-525
  10. Back Matter
    Pages 526-555

About this book


"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 of the two tableau systems has its own uses; each provides us with different information about the logics involved. They complement each other more than they overlap. Of the two Gentzen systems, one is of the conventional sort, common in the literature.


English literature literature logic modal logic notation present proposition quantifiers

Authors and affiliations

  1. 1.Herbert H. Lehman College of the City University of New YorkUSA

Bibliographic information

  • Book Title Proof Methods for Modal and Intuitionistic Logics
  • Authors M. Fitting
  • Series Title Synthese Library
  • DOI
  • Copyright Information Springer Science+Business Media B.V. 1983
  • Publisher Name Springer, Dordrecht
  • eBook Packages Springer Book Archive
  • Hardcover ISBN 978-90-277-1573-9
  • Softcover ISBN 978-90-481-8381-4
  • eBook ISBN 978-94-017-2794-5
  • Edition Number 1
  • Number of Pages VIII, 555
  • Number of Illustrations 0 b/w illustrations, 0 illustrations in colour
  • Topics Logic
  • Buy this book on publisher's site