Proof Methods for Modal and Intuitionistic Logics (Synthese Library) by M. Fitting

by Melvin Fitting

"Necessity is the mother of invention. " Part What is in this book - details. There are several different types of formal proof procedures that logicians have invented. The ones we consider 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 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.

Paperback

First published January 1, 1983

About the author

Melvin "Mel" Fitting (born January 24, 1942) is a logician with special interests in philosophical logic and tableau proof systems. He was a Professor at City University of New York, Lehman College and the Graduate Center from 1968 to 2013. At the Graduate Center he was in the departments of Computer Science, Philosophy, and Mathematics, and at Lehman College he was in the department of Mathematics and Computer Science. He is now Professor emeritus.

Fitting was born in Troy, New York. His undergraduate degree is from Rensselaer Polytechnic Institute, and his doctorate is from Yeshiva University, both in mathematics. His thesis advisor was Raymond Smullyan.

In June 2012 Melvin Fitting was given the Herbrand Award by CADE, for distinguished contributions to automated deduction.

A loose motivation for much of Melvin Fitting's work can be formulated succinctly as follows. There are many logics. Our principles of reasoning vary with context and subject matter. Multiplicity is one of the glories of modern formal logic. The common thread tying logics together is a concern for what can be said (syntax), what that means (semantics), and relationships between the two. A philosophical position that can be embodied in a formal logic has been shown to be coherent, not correct. Logic is a tool, not a master, but it is an enjoyable tool to use