THAT the study of the logic of possibility and necessity has 'come of age' is evidenced not only by the continuing publication of many articles on modal logic, but also by the recent appearance of a number of books dealing with the subject. This book is intended to serve the logical-philosophical-mathematical community on several levels; it does so, I think, in a manner complementary to books already available. First of all, there are a number of results about and manners of presentation of modal logic which appear here for the first time. Secondly, the book is intended to present these results as well as results already in the literature in a unified manner and so provide a useful reference source for working modal logicians as well as for other logicians, philosophers, and mathematicians who have occasion to deal with the logic of necessity and possibility. And this work can also serve as a text for a sequence of courses or seminars in modal logic. The book, in fact, contains a detailed development of non-modal propositional logic, both classical and intuitionist, and so can be used as supplementary material for a course in general symbolic logic. There are no exercises explicitly included, but ample opportunity is provided the student to provide or complete proofs for theorems in the text.

The logics studied herein are presented as formal mathematical systems. This does not signify a lack of interest on my part in the philosophical aspects of these systems; indeed, my studies of modal logic have suggested the possibility of applications of modal logic in areas as diverse as the methodology of C. S. Peirce and the foundations of relativity and of quantum theory. Before the application of modal logic, however, must come the study of the pure, unapplied systems. A comprehensive study of formal modal logic is the aim of this book.

We assume that the student has had sufficient logic to appreciate what a formal system is. Although we intend the various calculi and structures studied to be rigorously defined systems, we try to make the text run more smoothly by leaving implicit much of the metalinguistic mechanism usually associated with such formal rigour. The general presentation, then, is 'semi-formal', with the student making explicit for himself or herself the metatheory left implicit in the book; there should be no trouble in so doing.

The approach to virtually all the systems studied is three-pronged. First, 'Hilbert-style' axiomatizations (with detachment and substitution for variables as the only non-modal rules of inference) with various primitive connectives are presented. The proof-theory of these systems is further explored from the point of view of Gentzen-style 'sequent logics'. Finally, the systems are studied model-theoretically, using methods originally due to Prior, Beth, and Kripke; the standard model-theoretic tool of this book is the semantic tableau construction. Completeness results are supplied for all but a very few of the systems studied. These results follow naturally by the association of the semantic modal structures with the proof-theoretical Gentzen sequent logics. One comment on the notation employed is in order here: the symbols of the object language systems studied are in general those of Łukasiewicz; in the model-theoretically oriented portions of this book we do, however, make some use of the `standard' notation with binary connectives as infixes (horseshoe for 'if-then', backward 'E' for existential quantifier, etc.). This notation is used strictly as shorthand within the metalanguage, and is employed to keep as clear as possible the distinction between metalanguage and object language while retaining the advantages inherent in a symbolic notation. Enough familiarity with quantification theory is assumed to handle the very elementary quantificational concepts involved.

I have been aided in the production of this book by colleagues, both at Florida and elsewhere, who have looked over portions of the typescript and have informally discussed with me various aspects of the work. I have also been aided by the students who have been willing to serve as pedagogical guinea pigs in the development of certain of the approaches employed. I thank students and colleagues alike, and regret that I cannot name them all here. I do wish, however, to name one man without whom this book would certainly never have been written. I was fortunate enough to have him as teacher in 1962; the direction imparted on me at that time carried not only through my doctoral work, but also into fruitful research which continues to today. The proof techniques of Chapter 1 are based directly on what he taught in class; these techniques have by and large not been set down in print, and so I make it clear that they are originally his rather than mine. In my years after graduate school he offered encouragement and advice that was warmly appreciated. He had begun to look at and comment on the first drafts of early chapters of this book when he died suddenly in the fall of 1969; the loss to mankind was not only that of an original and powerful philosopher and logician, but of a warm and inspiring human being as well. I dedicate this book, then, to the memory of Arthur Prior.

University of Florida    
Gainesville, August 1972