The completeness of quantified modal logics can be shown with the tree method by modifying the strategy used in propositional modal logic. Section 8.4 explains how to use trees to demonstrate the completeness of propositional modal logics S that result from adding one or more of the following axioms to K: (D), (M), (4), (B), (5), (CD). In this chapter, the tree method will be extended to quantified modal logics based on the same propositional modal logics. The reader may want to review Sections 8.3 and 8.4 now, since details there will be central to this discussion. The fundamental idea is to show that every S-valid argument is provable in S in two stages. Assuming that H / C is S-valid, use the Tree Model Theorem (of Section 8.3) to prove that the S-tree for H / C closes. Then use the method for converting closed S-trees into proofs to construct a proof in S of H / C from the closed S-tree. This will show that any S-valid argument has a proof in S, which is, of course, what the completeness of S amounts to.

The Quantified Tree Model Theorem

In order to demonstrate completeness for quantified modal logics, a quantified version of the Tree Model Theorem will be developed here. This will also be useful in showing the correctness of trees for the quantified systems. Proofs of the appropriate tree model theorems are complicated by the fact that there are so many different systems to be considered in quantified modal logic. Several different interpretations of the quantifiers have been developed. However, the transfer theorems proven in Sections 15.7 and 15.8 show how results for all these systems can be obtained from a proof of completeness for truth value models (tS-models). So a demonstration of the Tree Model Theorem will be given for tS-validity.

Preface

The main purpose of this book is to help bridge a gap in the landscape of modal logic. A great deal is known about modal systems based on propositional logic. However, these logics do not have the expressive resources to handle the structure of most philosophical argumentation. If modal logics are to be useful to philosophy, it is crucial that they include quantifiers and identity. The problem is that quantified modal logic is not as well developed, and it is difficult for the student of philosophy who may lack mathematical training to develop mastery of what is known. Philosophical worries about whether quantification is coherent or advisable in certain modal settings partly explain this lack of attention. If one takes such objections seriously, they exert pressure on the logician to either eliminate modality altogether or eliminate the allegedly undesirable forms of quantification.

Even if one lays those philosophical worries aside, serious technical problems must still be faced. There is a rich menu of choices for formulating the semantics of quantified modal languages, and the completeness problem for some of these systems is difficult or unresolved. The philosophy of this book is that this variety is to be explored rather than shunned. We hope to demonstrate that modal logic with quantifiers can be simplified so that it is manageable, even teachable. Some of the simplifications depend on the foundations – in the way the systems for propositional modal logic are developed. Some ideas that were designed to make life easier when quantifiers are introduced are also genuinely helpful even for those who will study only the propositional systems. So this book can serve a dual purpose. It is, I hope, a simple and accessible introduction to propositional modal logic for students who have had a first course in formal logic (preferably one that covers natural deduction rules and truth trees). I hope, however, that students who had planned to use this book to learn only propositional modal logic will be inspired to move on to study quantification as well.

Here we give completeness proofs for many quantified modal logics, using a variant of the method of maximally consistent sets. Although the previous chapter already established completeness for many quantified modal logics using the tree method, there are good reasons for covering the method of maximally consistent sets as well. First, this is the standard approach to obtaining completeness results, so most students of modal logic will want some understanding of the method. Second, the tree method applied only to those systems for which it was shown how to convert a tree into a proof. The method of maximally consistent sets applies to more systems, though it has limitations described below in Section 17.2.

How Quantifiers Complicate Completeness Proofs

One might expect that proving completeness of quantified modal logic could be accomplished by simply “pasting together” standard results for quantifiers with those for propositional modal logic. Unfortunately, it is not so easy. In order to appreciate the problems that arise, and how they may be overcome, let us first review the strategies used to show completeness for propositional modal logic with maximally consistent sets. Then it will be possible to outline the difficulties that arise when quantifiers are added.

Preface to the Second Edition

In the years since the first publication of Modal Logic for Philosophers, I have received many suggestions for its improvement. The most substantial change in the new edition is a response to requests for a chapter on logics for conditionals. This topic is widely mentioned in the philosophical literature, so any book titled “Modal Logic for Philosophers” should do it justice. Unfortunately, the few pages on the topic provided in the first edition did no more than whet the reader’s appetite for a more adequate treatment. In this edition, an entire chapter (Chapter 20) is devoted to conditionals. It includes a discussion of material implication and its failings, strict implication, relevance logic, and (so-called) conditional logic. Although this chapter still qualifies as no more than an introduction, I hope it will be useful for philosophers who wish to get their bearings in the area.

While the structure of the rest of the book has not changed, there have been improvements everywhere. Thanks to several classes in modal logic taught using the first edition, and suggestions from attentive students, a number of revisions have been made that clarify and simplify the technical results. The first edition also contained many errors. While most of these were of the minor kind from which a reader could easily recover, there were still too many where it was difficult to gather what was intended. A list of errata for the first edition has been widely distributed on the World Wide Web, and this has been of some help. However, it is time to gather these corrections together to produce a new edition where (I can hope) the remaining errors are rare.

Many different systems of quantified modal logic have been presented in this book, each one based on the minimal system fK. In the next few chapters, we will show the adequacy of many of these logics by showing both their soundness and completeness. When S is one of the quantified modal logics discussed, and the corresponding notion of an S-model has been defined, soundness and completeness together amount to the claim that provability-in-S and S-validity match.

1. (Soundness) If H ⊢S C then H ⊨S C.

2. (Completeness) If H ⊨S C then H ⊢S C.

This chapter will be devoted to soundness and to some theorems that will be useful for the completeness proofs to come. Some of these results are interesting in their own right, since they show how the various treatments of the quantifier are interrelated. Sections 15.4–15.8 will explain how notions of validity for the substitution, intensional, and objectual interpretations are shown equivalent to corresponding brands of validity on truth value models – the simplest kind of models. This will mean that the relatively easy completeness results for truth value models can be quickly transferred to substitution, intensional, and objectual forms of validity. Readers who wish to study only truth value models may omit those sections.

Two different strategies will be presented to demonstrate completeness for truth value models. Chapter 16 covers completeness using a variation on the tree method found in Chapter 8. The modifications needed to extend the completeness result to systems with quantifiers are fairly easy to supply. Chapter 17 presents completeness results using the canonical model technique of Chapter 9. This method is the standard technique found in the literature, but it requires fairly extensive modifications to the strategy used for propositional modal logic. Chapters 16 and 17 are designed to be read independently, so that one may be understood without the other.

Why Conditional Logics Are Needed

This chapter describes a number of different logics that introduce a two-place operator (Ó, ⇒, or >) to help represent conditional expressions – expressions of the form: if A, then B (or of related forms such as the subjunctive conditional: if A were to be the case, then B would be). But why are such logics needed? Why not simply handle conditionals using the symbol → for material implication? The rules for → (namely, Modus Ponens and Conditional Proof) are quite intuitive. Furthermore, we know that the system of propositional logic that employs these rules is sound and complete for a semantics that adopts the material implication truth table embodied in (→).

1. (→) aw(A→B)=T iff aw(A)=F or aw(B)=T.

So it appears that → is all we need to manage ‘if .. then’.

On the other hand, objections to the idea that material implication is an adequate account of conditionals have been with us for almost as long as formal logic has existed. According to (→), A→B is true when A is false, and yet this is hardly the way ‘if A then B’ is understood in natural language. It is false that I am going to live another 1,000 years, but that hardly entails the truth of (1).

1. (1) If I am going to live another 1,000 years, then I will die tomorrow.

When A and B are incompatible with each other as in this case, the normal reaction is to count ‘if A then B’ false, even when the antecedent A is false. This illustrates that in English, the truth of ‘if A then B’ requires some sort of relevant connection between A and B. When A and B are incompatible, as they are in (1), there is no such connection, and so we reject ‘if A then B’.

Chapter 3 introduced the accessibility relation R on the set of worlds W in defining the truth condition for the generic modal operator. In K-models, the frame <W, R> of the model was completely arbitrary. Any nonempty set W and any binary relation R on W counts as a frame for a K-model. However, when we actually apply modal logic to a particular domain and give □ a particular interpretation, the frame <W, R> may take on special properties. Variations in the principles appropriate for a given modal logic will depend on what properties the frame should have. The rest of this chapter explains how various conditions on frames emerge from the different readings we might choose for □.

Conditions Appropriate for Tense Logic

In future-tense logic, □ reads ‘it will always be the case that’. Given (□), we have that □A is true at w iff A is true at all worlds v such that wRv. According to the meaning assigned to □, R must be the relation earlier than defined over a set W of times. There are a number of conditions on the frame <W, R> that follow from this interpretation. One fairly obvious feature of earlier than is transitivity.

1. Transitivity: If wRv and vRu, then wRu.

The Language of Propositional Modal Logic

We will begin our study of modal logic with a basic system called K in honor of the famous logician Saul Kripke. K serves as the foundation for a whole family of systems. Each member of the family results from strengthening K in some way. Each of these logics uses its own symbols for the expressions it governs. For example, modal (or alethic) logics use □ for necessity, tense logics use H for what has always been, and deontic logics use O for obligation. The rules of K characterize each of these symbols and many more. Instead of rewriting K rules for each of the distinct symbols of modal logic, it is better to present K using a generic operator. Since modal logics are the oldest and best known of those in the modal family, we will adopt □ for this purpose. So □ need not mean necessarily in what follows. It stands proxy for many different operators, with different meanings. In case the reading does not matter, you may simply call □A ‘box A’.

First we need to explain what a language for propositional modal logic is. The symbols of the language are ⊥, →, □; the propositional variables: p, q, r, p′, and so forth; and parentheses. The symbol ⊥ represents a contradiction, → represents ‘if . . then’, and □ is the modal operator. A sentence of propositional modal logic is defined as follows:

1. ⊥ and any propositional variable is a sentence.

2. If A is a sentence, then □A is a sentence.

3. If A is a sentence and B is a sentence, then (A→B) is a sentence.

4. No other symbol string is a sentence.

In this book, we will use letters ‘A’, ‘B’, ‘C’ for sentences. So A may be a propositional variable, p, or something more complex like (p→q), or ((p→ ⊥)→q). To avoid eyestrain, we usually drop the outermost set of parentheses. So we abbreviate (p→q) to p→q. (As an aside for those who are concerned about use-mention issues, here are the conventions of this book. We treat ‘⊥’, ‘→’, ‘□’, and so forth as used to refer to symbols with similar shapes. It is also understood that ‘□A’, for example, refers to the result of concatenating □ with the sentence A.)

Since there are so many different possible systems for modal logic, it is important to determine which system are equivalent, and which ones distinct from others. Figure 11.1 (on the next page) lays out these relationships for some of the best-known modal logics. It names systems by listing their axioms. So, for example, M4B is the system that results from adding (M), (4), and (B) to K. In boldface, we have also indicated traditional names of some systems, namely, S4, B, and S5. When system S appears below and/or to the left of S′ connected by a line, then S′ is an extension of S. This means that every argument provable in S is provable in S′, but S is weaker than S′, that is, not all arguments provable in S′ are provable in S.

Showing Systems Are Equivalent

One striking fact shown in Figure 11.1 is the large number of alternative ways of formulating S5. It is possible to prove these formulations are equivalent by proving the derivability of the official axioms of S5 (namely, (M) and (5)) in each of these systems and vice versa. However, there is an easier way. By the adequacy results given in Chapter 8 (or Chapter 9), we know that for each collection of axioms, there is a corresponding concept of validity. Adequacy guarantees that these notions of provability and validity correspond. So if we can show that two forms of validity are equivalent, then it will follow that the corresponding systems are equivalent. Let us illustrate with an example.