A modal is an expression (like ‘necessarily’ or‘possibly’) that is used to qualify the truth of ajudgement. Modal logic is, strictly speaking, the study of thedeductive behavior of the expressions ‘it is necessarythat’ and ‘it is possible that’. However, the term‘modal logic’ may be used more broadly for a family ofrelated systems. These include logics for belief, for tense and othertemporal expressions, for the deontic (moral) expressions such as‘it is obligatory that’ and ‘it is permittedthat’, and many others. An understanding of modal logic isparticularly valuable in the formal analysis of philosophicalargument, where expressions from the modal family are both common andconfusing. Modal logic also has important applications in computerscience.

• 1. What is Modal Logic?
• 2. Modal Logics
• 3. Deontic Logics
• 4. Temporal Logics
• 5. Conditional Logics
• 6. Possible Worlds Semantics
• 7. Modal Axioms and Conditions on Frames
• 8. Map of the Relationships Between Modal Logics
• 9. The General Axiom
• 10. Two Dimensional Semantics
• 11. Provability Logics
• 12. Advanced Modal Logic
• 13. Bisimulation
• 14. Correspondence Theory
• 15. Modal Logic and Games
• 16. Quantifiers in Modal Logic
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. What is Modal Logic?

Narrowly construed, modal logic studies reasoning that involves theuse of the expressions ‘necessarily’ and‘possibly’. However, the term ‘modal logic’ isused more broadly to cover a family of logics with similar rules and avariety of different symbols.

A list describing the best known of these logics follows.

2. Modal Logics

The most familiar logics in the modal family are constructed from aweak logic called \(\bK\) (after Saul Kripke). Under the narrowreading, modal logic concerns necessity and possibility. A variety ofdifferent systems may be developed for such logics using \(\bK\) as afoundation. The symbols of \(\bK\) include ‘\({\sim}\)’for ‘not’, ‘\(\rightarrow\)’ for‘if…then’, and ‘\(\Box\)’ for the modaloperator ‘it is necessary that’. (The connectives‘\(\amp\)’, ‘\(\vee\)’, and‘\(\leftrightarrow\)’ may be defined from‘\({\sim}\)’ and ‘\(\rightarrow\)’ as is donein propositional logic.) \(\bK\) results from adding the following tothe principles of propositional logic.

Necessitation Rule:   If \(A\) is a theorem of \(\bK\), thenso is \(\Box A\).

Distribution Axiom: \(\Box(A\rightarrow B) \rightarrow (\BoxA\rightarrow \Box B)\).

(In these principles we use ‘\(A\)’ and‘\(B\)’ as metavariables ranging over formulas of thelanguage.) According to the Necessitation Rule, any theorem of logicis necessary. The Distribution Axiom says that if it is necessary thatif \(A\) then \(B\), then if necessarily \(A\), then necessarily\(B\).

The operator \(\Diamond\) (for ‘possibly’) can be definedfrom \(\Box\) by letting \(\Diamond A = {\sim}\Box{\sim}A\). In\(\bK\), the operators \(\Box\) and \(\Diamond\) behave very much likethe quantifiers \(\forall\) (all) and \(\exists\) (some). For example,the definition of \(\Diamond\) from \(\Box\) mirrors the equivalenceof \(\forall xA\) with \({\sim}\exists x{\sim}A\) in predicate logic.Furthermore, \(\Box(A \amp B)\) entails \(\Box A \amp \Box B\) andvice versa; while \(\Box A\vee \Box B\) entails \(\Box (A\vee B)\),butnot vice versa. This reflects the patterns exhibited bythe universal quantifier: \(\forall x(A \amp B)\) entails \(\forall xA\amp \forall xB\) and vice versa, while \(\forall xA \vee \forall xB\)entails \(\forall x(A \vee B)\) but not vice versa. Similar parallelsbetween \(\Diamond\) and \(\exists\) can be drawn. The basis for thiscorrespondence between the modal operators and the quantifiers willemerge more clearly in the section onPossible Worlds Semantics.

The system \(\bK\) is too weak to provide an adequate account ofnecessity. The following axiom is not provable in \(\bK\), but it isclearly desirable.

\((M)\) claims that whatever is necessary is the case. Notice that\((M)\) would be incorrect were \(\Box\) to be read ‘it ought tobe that’, or ‘it was the case that’. So the presenceof axiom \((M)\) distinguishes logics for necessity from other logicsin the modal family. A basic modal logic \(M\) results from adding\((M)\) to \(\bK\). (Some authors call this system\(\mathbf{T}\).)

Many logicians believe that \(M\) is still too weak to correctlyformalize the logic of necessity and possibility. They recommendfurther axioms to govern the iteration or repetition of modaloperators. Here are two of the most famous iteration axioms:

\(\mathbf{S4}\) is the system that results from adding (4) to \(M\).Similarly \(\mathbf{S5}\) is \(M\) plus (5). In \(\mathbf{S4}\), thesentence \(\Box \Box A\) is equivalent to \(\Box A\). As a result, anystring of boxes may be replaced by a single box, and the same goes forstrings of diamonds. This amounts to the idea that iteration of thesame modal operator is superfluous. Saying that \(A\) is necessarilynecessary is considered a uselessly long-winded way of saying that\(A\) is necessary. The system \(\mathbf{S5}\) has even strongerprinciples for simplifying strings of modal operators. In\(\mathbf{S4}\), a string of operators ofthe same kind canbe replaced by that operator; in \(\mathbf{S5}\), strings containingboth boxes and diamonds are equivalent to the last operator in thestring. So, for example, saying that it is possible that \(A\) isnecessary is the same as saying that \(A\) is necessary. A summary ofthese features of \(\mathbf{S4}\) and \(\mathbf{S5}\) follows.

One could engage in endless argument over the correctness orincorrectness of these and other iteration principles for \(\Box\) and\(\Diamond\). The controversy can be partly resolved by recognizingthat the words ‘necessarily’ and ‘possibly’have many different uses. So the acceptability of axioms for modallogic depends on which of these uses we have in mind. For this reason,there is no one modal logic, but rather a whole family of systemsbuilt around \(M\). The relationship between these systems isdiagrammed inSection 8, and their application to different uses of ‘necessarily’and ‘possibly’ can be more deeply understood by studyingtheir possible world semantics inSection 6.

The system \(\mathbf{B}\) (for the logician Brouwer) is formed byadding axiom \((B)\) to \(M\).

It is interesting to note that \(\mathbf{S5}\) can be formulatedequivalently by adding \((B)\) to \(\mathbf{S4}\). The axiom \((B)\)raises an important point about the interpretation of modal formulas.\((B)\) says that if \(A\) is the case, then \(A\) is necessarilypossible. One might argue that \((B)\) should always be adopted in anymodal logic, for surely if \(A\) is the case, then it is necessarythat \(A\) is possible. However, there is a problem with this claimthat can be exposed by noting that \(\Diamond \Box A\rightarrow A\) isprovable from \((B)\). So \(\Diamond \Box A\rightarrow A\) should beacceptable if \((B)\) is. However, \(\Diamond \Box A\rightarrow A\)says that if \(A\) is possibly necessary, then \(A\) is the case, andthis is far from obvious. Why does \((B)\) seem obvious, while one ofthe things it entails seems not obvious at all? The answer is thatthere is a dangerous ambiguity in the English interpretation of\(A\rightarrow \Box \Diamond A\). We often use the expression‘If \(A\) then necessarily \(B\)’ to express that theconditional ‘if \(A\) then \(B\)’ is necessary. Thisinterpretation corresponds to \(\Box(A\rightarrow B)\). On otheroccasions, we mean that if \(A\), then \(B\) is necessary:\(A\rightarrow \Box B\). In English, ‘necessarily’ is anadverb, and since adverbs are usually placed near verbs, we have nonatural way to indicate whether the modal operator applies to thewhole conditional or to its consequent. For these reasons, there is atendency to confuse \((B): A\rightarrow \Box \Diamond A\) with\(\Box(A\rightarrow \Diamond A)\). But \(\Box(A\rightarrow \DiamondA)\) is not the same as \((B)\), for \(\Box(A\rightarrow \Diamond A)\)is already a theorem of \(M\), and \((B)\) is not. One must takespecial care that our positive reaction to \(\Box(A\rightarrow\Diamond A)\) does not infect our evaluation of \((B)\). One simpleway to protect ourselves is to formulate \(B\) in an equivalent wayusing the axiom \(\Diamond \Box A\rightarrow A\), where theseambiguities of scope do not arise.

3. Deontic Logics

Deontic logics introduce the primitive symbol \(O\) for ‘it isobligatory that’, from which symbols \(P\) for ‘it ispermitted that’ and \(F\) for ‘it is forbidden that’are defined: \(PA = {\sim}O{\sim}A\) and \(FA = O{\sim}A\). Thedeontic analog of the modal axiom \((M): OA\rightarrow A\) is clearlynot appropriate for deontic logic. (Unfortunately, what ought to be isnot always the case.) However, a basic system \(\mathbf{D}\) ofdeontic logic can be constructed by adding the weaker axiom \((D)\) to\(\bK\).

Axiom \((D)\) guarantees the consistency of the system of obligationsby insisting that when \(A\) is obligatory, \(A\) is permissible. Asystem which obligates us to bring about \(A\), but doesn’tpermit us to do so, puts us in an inescapable bind. Although some willargue that such conflicts of obligation are at least possible, mostdeontic logicians accept \((D)\).

\(O(OA\rightarrow A)\) is another deontic axiom that seems desirable.Although it is wrong to say that if \(A\) is obligatory then \(A\) isthe case \((OA\rightarrow A)\), still, this conditionaloughtto be the case. So some deontic logicians believe that \(D\) needs tobe supplemented with \(O(OA\rightarrow A)\) as well.

Controversy about iteration (repetition) of operators arises again indeontic logic. In some conceptions of obligation, \(OOA\) just amountsto \(OA\). ‘It ought to be that it ought to be’ is treatedas a sort of stuttering; the extra ‘ought’s do not addanything new. So axioms are added to guarantee the equivalence of\(OOA\) and \(OA\). The more general iteration policy embodied in\(\mathbf{S5}\) may also be adopted. However, there are conceptions ofobligation where distinction between \(OA\) and \(OOA\) is preserved.The idea is that there are genuine differences between the obligationsweactually have and the obligations weshouldadopt. So, for example, ‘it ought to be that it ought to be that\(A\)’ commands adoption of some obligation which may notactually be in place, with the result that \(OOA\) can be true evenwhen \(OA\) is false.

For a more detailed discussion, see the entry ondeontic logic.

4. Temporal Logics

In temporal logic (also known as tense logic), there are two basicoperators, \(G\) for the future, and \(H\) for the past. \(G\) is read‘it always will be that’ and the defined operator \(F\)(read ‘it will be the case that’) can be introduced by\(FA = {\sim}G{\sim}A\). Similarly \(H\) is read ‘it always wasthat’ and \(P\) (for ‘it was the case that’) isdefined by \(PA={\sim}H{\sim}A\). A basic system of temporal logiccalled \(\mathbf{Kt}\) results from adopting the principles of \(\bK\)for both \(G\) and \(H\), along with two axioms to govern theinteraction between the past and future operators:

Necessitation Rules:
If \(A\) is a theorem then so are \(GA\) and \(HA\).

Distribution Axioms:
\(G(A\rightarrow B) \rightarrow(GA\rightarrow GB)\) and\(H(A\rightarrow B) \rightarrow (HA\rightarrow HB)\)

Interaction Axioms:
\(A\rightarrow GPA\) and \(A\rightarrow HFA\)

The interaction axioms raise questions concerning asymmetries betweenthe past and the future. A standard intuition is that the past isfixed, while the future is still open. The first interaction axiom\((A\rightarrow GPA)\) conforms to this intuition in reporting thatwhat is the case \((A)\) will at all future times be in the past\((GPA)\). However \(A\rightarrow HFA\) may appear to haveunacceptably deterministic overtones, for it claims, apparently, thatwhat is true now \((A)\) has always been such that it will occur inthe future \((HFA)\). However, possible world semantics for temporallogic reveals that this worry results from a simple confusion and thatthe two interaction axioms are equally acceptable.

Note that the characteristic axiom of modal logic, \((M): \BoxA\rightarrow A\), is not acceptable for either \(H\) or \(G\), since\(A\) does not follow from ‘it always was the case that\(A\)’, nor from ‘it always will be the case that\(A\)’. However, it is acceptable in a closely related temporallogic where \(G\) is read ‘it is and always will be’, and\(H\) is read ‘it is and always was’.

Depending on which assumptions one makes about the structure of time,further axioms must be added to temporal logics. A list of axiomscommonly adopted in temporal logics follows. An account of how theydepend on the structure of time will be found in the sectionPossible Worlds Semantics.

It is interesting to note that certain combinations of past tense andfuture tense operators may be used to express complex tenses inEnglish. For example, \(FPA\), corresponds to sentence \(A\) in thefuture perfect tense (as in ‘20 seconds from now the light willhave changed’). Similarly, \(PPA\) expresses the past perfecttense.

For a more detailed discussion, see the entry ontemporal logic.

5. Conditional and Relevance Logics

The founder of modal logic, C. I. Lewis, defined a series of modallogics which did not have \(\Box\) as a primitive symbol. Lewis wasconcerned to develop a logic of conditionals that was free of the socalled Paradoxes of Material Implication, namely the classicaltheorems \(A\rightarrow({\sim}A\rightarrow B)\) and\(B\rightarrow(A\rightarrow B)\). He introduced the symbol\(\fishhook\) for “strict implication” and developedlogics where neither \(A\fishhook ({\sim}A\fishhook B)\) nor\(B\fishhook (A\fishhook B)\) is provable. The modern practice hasbeen to define \(A\fishhook B\) by \(\Box(A\rightarrow B)\) and usemodal logics governing \(\Box\) to obtain similar results. However,the provability of such formulas as \((A \amp{\sim}A)\fishhook B\) insuch logics seems at odds with concern for the paradoxes. Anderson andBelnap (1975) have developed systems \(\mathbf{R}\) (for RelevanceLogic) and \(\mathbf{E}\) (for Entailment) which are designed toovercome such difficulties. These systems require revision of thestandard systems of propositional logic. (See Mares (2004) and theentry onrelevance logic.)

David Lewis (1973), Robert Stalnaker (1968), and others have developedconditional logics to handle counterfactual expressions, that is, expressions of theform ‘if \(A\)were to happen then \(B\)wouldhappen’. (Kvart (1980) is another good source on the topic.)Counterfactual logics differ from those based on strict implicationbecause the former reject while the latter accept contraposition.

6. Possible Worlds Semantics

The purpose of logic is to characterize the difference between validand invalid arguments. A logical system for a language is a set ofaxioms and rules designed to proveexactly the validarguments statable in the language. Creating such a logic may be adifficult task. The logician must make sure that the system issound, i.e. that every argument proven using the rules andaxioms is in fact valid. Furthermore, the system should becomplete, meaning that every valid argument has a proof inthe system. Demonstrating soundness and completeness of formal systemsis one of a logician’s central concern.

Such a demonstration cannot get underway until the concept of validityis defined rigorously. Formal semantics for a logic provides adefinition of validity by characterizing the truth behavior of thesentences of the system. In propositional logic, validity can bedefined using truth tables. A valid argument is simply one where everytruth table row that makes its premises true also makes its conclusiontrue. However, truth tables cannot be used to provide an account ofvalidity in modal logics because there are no truth tables forexpressions such as ‘it is necessary that’, ‘it isobligatory that’, and the like. (The problem is that the truthvalue of \(A\) does not determine the truth value for \(\Box A\). Forexample, when \(A\) is ‘Dogs are dogs’, \(\Box A\) istrue, but when \(A\) is ‘Dogs are pets’, \(\Box A\) isfalse.) Nevertheless, semantics for modal logics can be defined byintroducing possible worlds. We will illustrate possible worldssemantics for a logic of necessity containing the symbols \({\sim},\rightarrow\), and \(\Box\). Then we will explain how the samestrategy may be adapted to other logics in the modal family.

In propositional logic, a valuation of the atomic sentences (or row ofa truth table) assigns a truth value \((T\) or \(F)\) to eachpropositional variable \(p\). Then the truth values of the complexsentences are calculated with truth tables. In modal semantics, a set\(W\) of possible worlds is introduced. A valuation then gives a truthvalue to each propositional variablefor each of the possibleworlds in \(W\). This means the value assigned to \(p\) for world\(w\) may differ from the value assigned to \(p\) for another world\(w'\).

The truth value of the atomic sentence \(p\) at world \(w\) given bythe valuation \(v\) may be written \(v(p, w)\). Given this notation,the truth values \((T\) for true, \(F\) for false) of complexsentences of modal logic for a given valuation \(v\) (and member \(w\)of the set of worlds \(W)\) may be defined by the following truthclauses. (‘iff’ abbreviates ‘if and onlyif’.)

Clauses \(({\sim})\) and \((\rightarrow)\) simply describe thestandard truth table behavior for negation and material implicationrespectively. According to (5), \(\Box A\) is true (at a world \(w)\)exactly when \(A\) is true inall possible worlds. Given thedefinition of \(\Diamond\) (namely \(\Diamond A ={\sim}\Box{\sim}A)\), the truth condition (5) insures that \(\DiamondA\) is true just in case \(A\) is true insome possibleworld. Since the truth clauses for \(\Box\) and \(\Diamond\) involvethe quantifiers ‘all’ and ‘some’(respectively), the parallels in logical behavior between \(\Box\) and\(\forall x\) and between \(\Diamond\) and \(\exists x\) noted inSection 2 will be expected.

Clauses \(({\sim}), (\rightarrow)\), and (5) allow us to calculate thetruth value of any sentence at any world on a given valuation. Adefinition of validity is now just around the corner. An argument is5-valid for a given set W (of possible worlds) if and only ifevery valuation of the atomic sentences that assigns the premises\(T\) at a world in \(W\) also assigns the conclusion \(T\) at thesame world. An argument is said to be5-valid iff it is validfor every non-empty set \(W\) of possible worlds.

It has been shown that \(\mathbf{S5}\) is sound and complete for5-validity (hence our use of the symbol ‘5’). The 5-validarguments are exactly the arguments provable in \(\mathbf{S5}\). Thisresult suggests that \(\mathbf{S5}\) is the correct way to formulate alogic of necessity.

However, \(\mathbf{S5}\) is not a reasonable logic for all members ofthe modal family. In deontic logic, temporal logic, and others, theanalog of the truth condition (5) is clearly not appropriate;furthermore there are even conceptions of necessity where (5) shouldbe rejected as well. The point is easiest to see in the case oftemporal logic. Here, the members of \(W\) are moments of time, orworlds “frozen”, as it were, at an instant. For simplicitylet us consider afuture temporal logic, a logic where \(\BoxA\) reads: ‘itwill always be the case that’. (Weformulate the system using \(\Box\) rather than the traditional \(G\)so that the connections with other modal logics will be easier toappreciate.) The correct clause for \(\Box\) should say that \(\BoxA\) is true at time \(w\) iff \(A\) is true at all timesin thefuture of \(w\). To restrict attention to the future, therelation \(R\) (for ‘earlier than’) needs to beintroduced. Then the correct clause can be formulated as follows.

This says that \(\Box A\) is true at \(w\) just in case \(A\) is trueat all timesafter \(w\).

Validity for this brand of temporal logic can now be defined. Aframe \(\langle W, R\rangle\) is a pair consisting of anon-empty set \(W\) (of worlds) and a binary relation \(R\) on \(W\).Amodel \(\langle F, v\rangle\) consists of a frame \(F\) anda valuation \(v\) that assigns truth values to each atomic sentence ateach world in \(W\). Given a model, the values of all complexsentences can be determined using \(({\sim}), (\rightarrow)\), and\((K)\). An argument is \(\bK\)-valid just in case any model whosevaluation assigns the premises \(T\) at a world also assigns theconclusion \(T\) at the same world. As the reader may have guessedfrom our use of ‘\(\bK\)’, it has been shown that thesimplest modal logic \(\bK\) is both sound and complete for\(\bK\)-validity.

7. Modal Axioms and Conditions on Frames

One might assume from this discussion that \(\bK\) is the correctlogic when \(\Box\) is read ‘it will always be the casethat’. However, there are reasons for thinking that \(\bK\) istoo weak. One obvious logical feature of the relation \(R\) (earlierthan) is transitivity. If \(wRv\) (\(w\) is earlier than \(v)\) and\(vRu\) (\(v\) is earlier than \(u)\), then it follows that \(wRu\)(\(w\) is earlier than \(u)\). So let us define a new kind of validitythat corresponds to this condition on \(R\). Let a 4-model be anymodel whose frame \(\langle W, R\rangle\) is such that \(R\) is atransitive relation on \(W\). Then an argument is 4-valid iff any4-model whose valuation assigns \(T\) to the premises at a world alsoassigns \(T\) to the conclusion at the same world. We use‘4’ to describe such a transitive model because the logicwhich is adequate (both sound and complete) for 4-validity is\(\mathbf{K4}\), the logic which results from adding the axiom (4):\(\Box A\rightarrow \Box \Box A\) to \(\bK\).

Transitivity is not the only property which we might want to requireof the frame \(\langle W, R\rangle\) if \(R\) is to be read‘earlier than’ and \(W\) is a set of moments. Onecondition (which is only mildly controversial) is that there is nolast moment of time, i.e. that for every world \(w\) there is someworld \(v\) such that \(wRv\). This condition on frames is calledseriality. Seriality corresponds to the axiom \((D): \BoxA\rightarrow \Diamond A\), in the same way that transitivitycorresponds to (4). A \(\mathbf{D}\)-model is a \(\bK\)-model with aserial frame. From the concept of a \(\mathbf{D}\)-model thecorresponding notion of \(\mathbf{D}\)-validity can be defined just aswe did in the case of 4-validity. As you probably guessed, the systemthat is adequate with respect to \(\mathbf{D}\)-validity is\(\mathbf{KD}\), or \(\bK\) plus \((D)\). Not only that, but thesystem \(\mathbf{KD4}\) (that is \(\bK\) plus (4) and \((D))\) isadequate with respect to \(\mathbf{D4}\)-validity, where a\(\mathbf{D4}\)-model is one where \(\langle W, R\rangle\) isboth serial and transitive.

Another property which we might want for the relation ‘earlierthan’ is density, the condition which says that between any twotimes we can always find another. Density would be false if time wereatomic, i.e. if there were intervals of time which could not be brokendown into any smaller parts. Density corresponds to the axiom \((C4):\Box \Box A\rightarrow \Box A\), the converse of (4), so for example,the system \(\mathbf{KC4}\), which is \(\bK\) plus \((C4)\) isadequate with respect to models where the frame \(\langle W,R\rangle\) is dense, and \(\mathbf{KDC4}\) is adequate with respect tomodels whose frames are serial and dense, and so on.

Each of the modal logic axioms we have discussed corresponds to acondition on frames in the same way. The relationship betweenconditions on frames and corresponding axioms is one of the centraltopics in the study of modal logics. Once an interpretation of theintensional operator \(\Box\) has been decided on, the appropriateconditions on \(R\) can be determined to fix the corresponding notionof validity. This, in turn, allows us to select the right set ofaxioms for that logic.

For example, consider a deontic logic, where \(\Box\) is read‘it is obligatory that’. Here the truth of \(\Box A\) doesnot demand the truth of \(A\) inevery possible world, butonly in a subset of those worlds where people do what they ought. Sowe will want to introduce a relation \(R\) for this kind of logic aswell, and use the truth clause \((K)\) to evaluate \(\Box A\) at aworld. However, in this case, \(R\) is not earlier than. Instead\(wRw'\) holds just in case world \(w'\) is a morally acceptablevariant of \(w\), i.e. a world that our actions can bring about whichsatisfies what is morally correct, or right, or just. Under such areading, it should be clear that the relevant frames should obeyseriality, the condition that requires that each possible world have amorally acceptable variant. The analysis of the properties desired for\(R\) makes it clear that a basic deontic logic can be formulated byadding the axiom \((D)\) and to \(\bK\).

Even in modal logic, one may wish to restrict the range of possibleworlds which are relevant in determining whether \(\Box A\) is true ata given world. For example, I might say that it is necessary that Ipay my bills, even though I know full well that there is a possibleworld where I fail to pay them. In ordinary speech, the claim that\(A\) is necessary does not require the truth of \(A\) inallpossible worlds, but rather only in a certain class of worlds which Ihave in mind (for example, worlds where I avoid penalties for failureto pay). In order to provide a generic treatment of necessity, we mustsay that \(\Box A\) is true in \(w\) iff \(A\) is true in all worldsthat are related to \(w\) in the right way. So for anoperator \(\Box\) interpreted as necessity, we introduce acorresponding relation \(R\) on the set of possible worlds \(W\),traditionally called the accessibility relation. The accessibilityrelation \(R\) holds between worlds \(w\) and \(w'\) iff \(w'\) ispossible given the facts of \(w\). Under this reading for \(R\), itshould be clear that frames for modal logic should be reflexive. Itfollows that modal logics should be founded on \(M\), the system thatresults from adding \((M)\) to \(\bK\). Depending on exactly how theaccessibility relation is understood, symmetry and transitivity mayalso be desired.

A list of some of the more commonly discussed conditions on frames andtheir corresponding axioms along with a map showing the relationshipbetween the various modal logics can be found in the next section.

8. Map of the Relationships Between Modal Logics

The following diagram shows the relationships between the best knownmodal logics, namely logics that can be formed by adding a selectionof the axioms \((D), (M)\), (4), \((B)\) and (5) to \(\bK\). A list ofthese (and other) axioms along with their corresponding frameconditions can be found below the diagram.

Diagram of Modal Logics

In this chart, systems are given by the list of their axioms. So, forexample \(\mathbf{M4B}\) is the result of adding \((M)\), (4) and\((B)\) to \(\bK\). In boldface, we have indicated traditional namesof some systems. When system \(\mathbf{S}\) appears below and/or tothe left of \(\mathbf{S}'\) connected by a line, then \(\mathbf{S}'\)is an extension of \(\mathbf{S}\). This means that every argumentprovable in \(\mathbf{S}\) is provable in \(\mathbf{S}'\), but\(\mathbf{S}\) is weaker than \(\mathbf{S}'\), i.e. not all argumentsprovable in \(\mathbf{S}'\) are provable in \(\mathbf{S}\).

The following list indicates axioms, their names, and thecorresponding conditions on the accessibility relation \(R\), foraxioms so far discussed in this encyclopedia entry.

In the list of conditions on frames, and in the rest of this article,the variables ‘\(w\)’, ‘\(v\)’,‘\(u\)’, ‘\(x\)’ and the quantifier‘\(\exists u\)’ are understood to range over \(W\).‘&’ abbreviates ‘and’ and‘\(\Rightarrow\)’ abbreviates‘if…then’.

The notion of correspondence between axioms and frame conditions thatis at issue here was illustrated in the previous section. The idea isthat when S is a list of axioms and F(S) is the corresponding set offrame conditions, then S corresponds to F(S) exactly when the systemK+S is adequate (sound and complete) for F(S)-validity, that is, anargument is provable in K+S iff it is F(S)-valid. However, a strongernotion of the correspondence between axioms and frame conditions hasemerged in research on modal logic. (SeeSection 14 below.)

9. The General Axiom

The correspondence between axioms and conditions on frames may seemsomething of a mystery. A beautiful result of Lemmon and Scott (1977)goes a long way towards explaining those relationships. Their theoremconcerned axioms which have the following form:

We use the notation ‘\(\Diamond^n\)’ to represent \(n\)diamonds in a row, so, for example, ‘\(\Diamond^3\)’abbreviates a string of three diamonds: ‘\(\Diamond \Diamond\Diamond\)’. Similarly ‘\(\Box^n\)’ represents astring of \(n\) boxes. When the values of \(h, i, j\), and \(k\) areall 1, we have axiom \((C)\):

The axiom \((B)\) results from setting \(h\) and \(i\) to 0, andletting \(j\) and \(k\) be 1:

To obtain (4), we may set \(h\) and \(k\) to 0, set \(i\) to 1 and\(j\) to 2:

Many (but not all) axioms of modal logic can be obtained by settingthe right values for the parameters in \((G).\)

Our next task will be to give the condition on frames whichcorresponds to \((G)\) for a given selection of values for \(h, i,j\), and \(k\). In order to do so, we will need a definition. Thecomposition of two relations \(R\) and \(R'\) is a new relation \(R\circ R'\) which is defined as follows:

For example, if \(R\) is the relation of being a brother and \(R'\) isthe relation of being a parent then \(R \circ R'\) is the relation ofbeing an uncle (because \(w\) is the uncle of \(v\) iff for someperson \(u\), both \(w\) is the brother of \(u\) and \(u\) is theparent of \(v)\). A relation may be composed with itself. For example,when \(R\) is the relation of being a parent, then \(R \circ R\) isthe relation of being a grandparent, and \(R \circ R \circ R\) is therelation of being a great-grandparent. It will be useful to write‘\(R^n\)’, for the result of composing \(R\) with itself\(n\) times. So \(R^2\) is \(R \circ R\), and \(R^4\) is \(R \circ R\circ R \circ R\). We will let \(R^1\) be \(R\), and \(R^0\) will bethe identity relation, i.e. \(wR^0 v\) iff \(w=v\).

We may now state the Scott-Lemmon result. It is that the condition onframes which corresponds exactly to any axiom of the shape \((G)\) isthe following:

It is interesting to see how the familiar conditions on \(R\) resultfrom setting the values for \(h\), \(i\), \(j\), and \(k\) accordingto the values in the corresponding axiom. For example, consider (5).In this case \(i=0\), and \(h=j=k=1\). So the corresponding conditionis

We have explained that \(R^0\) is the identity relation. So if \(vR^0x\) then \(v=x\). But \(\exists x (v=x \amp uRx)\) is equivalent to\(uRv\), and so the Euclidean condition is obtained:

In the case of axiom (4), \(h=0, i=1, j=2\) and \(k=0\). So thecorresponding condition on frames is

Resolving the identities, this amounts to:

By the definition of \(R^2, vR^2 u\) iff \(\exists x(vRx \amp xRu)\),so this comes to:

which by predicate logic, is equivalent to transitivity:

The reader may find it a pleasant exercise to see how thecorresponding conditions fall out of hijk-Convergence when the valuesof the parameters \(h\), \(i\), \(j\), and \(k\) are set by otheraxioms.

The Scott-Lemmon results provides a quick method for establishingresults about the relationship between axioms and their correspondingframe conditions. Since they showed the adequacy of any logic thatextends \(\bK\) with a selection of axioms of the form \((G)\) withrespect to models that satisfy the corresponding set of frameconditions, they provided “wholesale” adequacy proofs forthe majority of systems in the modal family. Sahlqvist (1975) hasdiscovered important generalizations of the Scott-Lemmon resultcovering a much wider range of axiom types.

10. Two Dimensional Semantics

Two-dimensional semantics is a variant of possible world semanticsthat uses two (or more) kinds of parameters in truth evaluation,rather than possible worlds alone. For example, a logic of indexicalexpressions, such as ‘I’, ‘here’,‘now’, and the like, needs to bring in the linguisticcontext (or context for short). Given a context \(c = \langle s, p,t\rangle\) where \(s\) is the speaker, \(p\) the place, and \(t\) thetime of utterance, then ‘I’ refers to \(s\),‘here’ to \(p\), and ‘now’ to \(t\). So in thecontext \(c = \langle\)Jim Garson, Houston, 3:00 P.M. CST on4/3/\(2014\rangle\) ‘I am here now’ is T iff Jim Garson isin Houston, at 3:00 P.M. CST on 4/3/2014.

In possible worlds semantics, a sentence’s truth-value dependedon the world at which it is evaluated. However, indexicals bring in asecond dimension – so we need to generalize again. Kaplan (1989)defines thecharacter of a sentence \(B\) to be a functionfrom the set of (linguistic) contexts to the content of \(B\), wherethe content, in turn, is simply the intension of \(B\), that is, afunction from possible worlds to truth-values. Here, truth evaluationis doubly dependent – on both linguistic contexts and possibleworlds.

One of Kaplan’s most interesting observations is that someindexical sentences are contingent but at the same time analyticallytrue. An example is (1).

• (1) I am here now.

Just from the meaning of the words, you can see that (1) must be truein any context \(c = \langle s, p, t\rangle\). After all, \(c\) countsas a linguistic context just in case \(s\) is a speaker who is atplace \(p\) at time \(t\). Therefore (1) is true at \(c\), and thatmeans that the pattern of truth-values (1) has along the contextdimension must be all Ts (given the possible world is held fixed).This suggests that the context dimension is apt for tracking analyticknowledge obtained from the mastery of our language. On the otherhand, the possible-worlds dimension keeps track of what is necessary.Holding the context fixed, there there are possible worlds where (1)is false. For example, when \(c = \langle\)Jim Garson, Houston, 3:00P.M. CST on 4/3/\(2014\rangle\), (1) fails at \(c\) in a possibleworld where Jim Garson is in Boston at 3:00 P.M. CST on 4/3/2014. Itfollows that ‘I am here now’ is a contingent analytictruth. Therefore, two-dimensional semantics can handle situationswhere necessity and analyticity come apart.

Another example where bringing in two dimension is useful is in thelogic for an open future (Thomason, 1984; Belnap, et al., 2001). Hereone employs a temporal structure where many possible future historiesextend from a given time. Consider (2).

• (2) Joe will order asea battle tomorrow.

If (2) is contingent, then there is a possible history where thebattle occurs the day after the time of evaluation and another onewhere it does not occur then. So to evaluate (2) you need to know twothings: what is the time \(t\) of evaluation, and which of thehistories \(h\) that run through \(t\) is the one to be considered. Soa sentence in such a logic is evaluated at a pair \(\langle t,h\rangle\).

Another problem resolved by two-dimensional semantics is theinteraction between ‘now’ and other temporal expressionslike the future tense ‘it will be the case that’. It isplausible to think that ‘now’ refers to the time ofevaluation. So we would have the following truth condition:

However this will not work for sentences like (3).

• (3) At some point inthe future, everyone now living will be unknown.

With \(\mathrm{F}\) as the future tense operator, (3) might betranslated:

(The correct translation cannot be \(\forall x(\text{Now} Lx\rightarrow \mathrm{F}Ux)\), with \(\mathrm{F}\) taking narrow scope,because (3) says there is a future time when all things now living areunknown together, not that each living thing will be unknown in somefuture time of its own.) When the truth conditions for (3)\('\) arecalculated, using (Now) and the truth condition (\(\mathrm{F}\)) for\(\mathrm{F}\), it turns out that (3)\('\) is true at time \(u\) iffthere is a time \(t\) after \(u\) such that everything that is livingat \(t\) (not \(u\)!) is unknown at \(t\).

To evaluate (3)\('\) correctly, so that it matches what we mean by(3), we must make sure that ‘now’ always refers back tothe original time of utterance when ‘now’ lies in thescope of other temporal operators such as F. Therefore we need to keeptrack of which time is the time of utterance \((u)\) as well as whichtime is the time of evaluation \((t)\). So our indices take the formof a pair \(\langle u, e\rangle\), where \(u\) is the time ofutterance, and \(e\) is the time of evaluation. Then the truthcondition (Now) is revised to (2DNow).

This has it that the Now\(B\) is true at a time \(u\) of utterance andtime \(e\) of evaluation provided that \(B\) is true when \(u\) istaken to be the time of evaluation. When the truth conditions for F,\(\forall\), and \(\rightarrow\) are revised in the obvious way (justignore the \(u\) in the pair), (3)\('\) is true at \(\langle u,e\rangle\) provided that there is a time \(e'\) later than \(e\) suchthat everything that is living at \(u\) is unknown at \(e'\). Bycarrying along a record of what \(u\) is during the truth calculation,we can always fix the value for ‘now’ to the original timeof utterance, even when ‘now’ is deeply embedded in othertemporal operators.

A similar phenomenon arises in modal logics with an actuality operatorA (read ‘it is actually the case that’). To properlyevaluate (4) we need to keep track of which world is taken to be theactual (or real) world as well as which one is taken to be the worldof evaluation.

• (4) It is possiblethat everyone actually living be unknown.

The idea of distinguishing different possible world dimensions insemantics has had useful applications in philosophy. For example,Chalmers (1996) has presented arguments from the conceivability of(say) zombies to dualist conclusions in the philosophy of mind.Chalmers (2006) has deployed two-dimensional semantics to helpidentify an a priori aspect of meaning that would support suchconclusions.

The idea has also been deployed in the philosophy of language. Kripke(1980) famously argued that ‘Water is H2O’ is a posterioribut nevertheless a necessary truth, for given that water just is H20,there is no possible world where THAT stuff is (say) a basic elementas the Greeks thought. On the other hand, there is a strong intuitionthat had the real world been somewhat different from what it is, theodorless liquid that falls from the sky as rain, fills our lakes andrivers, etc. might perfectly well have been an element. So in somesense it is conceivable that water is not H20. Two dimensionalsemantics makes room for these intuitions by providing a separatedimension that tracks a conception of water that lays aside thechemical nature of what water actually is. Such a ‘narrowcontent’ account of the meaning of ‘water’ canexplain how one may display semantical competence in the use of thatterm and still be ignorant about the chemistry of water (Chalmers,2002).

For a more detailed discussion, see the entry ontwo-dimensional semantics.

11. Provability Logics

Modal logic has been useful in clarifying our understanding of centralresults concerning provability in the foundations of mathematics(Boolos, 1993). Provability logics are systems where the propositionalvariables \(p, q, r\), etc. range over formulas of some mathematicalsystem, for example Peano’s system \(\mathbf{PA}\) forarithmetic. (The system chosen for mathematics might vary, but assumeit is \(\mathbf{PA}\) for this discussion.) Gödel showed thatarithmetic has strong expressive powers. Using code numbers forarithmetic sentences, he was able to demonstrate a correspondencebetween sentences of mathematics and facts about which sentences areand are not provable in \(\mathbf{PA}\). For example, he showed therethere is a sentence \(C\) that is true just in case no contradictionis provable in \(\mathbf{PA}\) and there is a sentence \(G\) (thefamous Gödel sentence) that is true just in case it is notprovable in \(\mathbf{PA}\).

In provability logics, \(\Box p\) is interpreted as a formula (ofarithmetic) that expresses that what \(p\) denotes is provable in\(\mathbf{PA}\). Using this notation, sentences of provability logicexpress facts about provability. Suppose that \(\bot\) is a constantof provability logic denoting a contradiction. Then \({\sim}\Box\bot\) says that \(\mathbf{PA}\) is consistent and \(\Box A\rightarrowA\) says that \(\mathbf{PA}\) is sound in the sense that when itproves \(A, A\) is indeed true. Furthermore, the box may be iterated.So, for example, \(\Box{\sim}\Box \bot\) makes the dubious claim that\(\mathbf{PA}\) is able to prove its own consistency, and \({\sim}\Box\bot \rightarrow{\sim}\Box{\sim}\Box \bot\) asserts (correctly asGödel proved) that if \(\mathbf{PA}\) is consistent then\(\mathbf{PA}\) is unable to prove its own consistency.

Although provability logics form a family of related systems, thesystem \(\mathbf{GL}\) is by far the best known. It results fromadding the following axiom to \(\bK\):

The axiom (4): \(\Box A\rightarrow \Box \Box A\) is provable in\(\mathbf{GL}\), so \(\mathbf{GL}\) is actually a strengthening of\(\mathbf{K4}\). However, axioms such as \((M): \Box A\rightarrow A\),and even the weaker \((D): \Box A\rightarrow \Diamond A\) are notavailable (nor desirable) in \(\mathbf{GL}\). In provability logic,provability is not to be treated as a brand of necessity. The reasonis that when \(p\) is provable in an arbitrary system \(\mathbf{S}\)for mathematics, it does not follow that \(p\) is true, since\(\mathbf{S}\) may be unsound. Furthermore, if \(p\) is provable in\(\mathbf{S} (\Box p)\) it need not even follow that \({\sim}p\) lacksa proof \(({\sim}\Box{\sim}p = \Diamond p). \mathbf{S}\) might beinconsistent and so prove both \(p\) and \({\sim}p\).

Axiom \((GL)\) captures the content of Loeb’s Theorem, animportant result in the foundations of arithmetic. \(\Box A\rightarrowA\) says that \(\mathbf{PA}\) is sound for \(A\), i.e. that if \(A\)were proven, A would be true. (Such a claim might not be secure for anarbitrarily selected system \(\mathbf{S}\), since \(A\) might beprovable in \(\mathbf{S}\) and false.) \((GL)\) claims that if\(\mathbf{PA}\) manages to prove the sentence that claims soundnessfor a given sentence \(A\), then \(A\) is already provable in\(\mathbf{PA}\). Loeb’s Theorem reports a kind of modesty on\(\mathbf{PA}\)’s part (Boolos, 1993, p. 55). \(\mathbf{PA}\)never insists (proves) that a proof of \(A\) entails \(A\)’struth, unless it already has a proof of \(A\) to back up thatclaim.

It has been shown that \(\mathbf{GL}\) is adequate for provability inthe following sense. Let a sentence of \(\mathbf{GL}\) bealwaysprovable exactly when the sentence of arithmetic it denotes isprovable no matter how its variables are assigned values to sentencesof \(\mathbf{PA}\). Then the provable sentences of \(\mathbf{GL}\) areexactly the sentences that are always provable. This adequacy resulthas been extremely useful, since general questions concerningprovability in \(\mathbf{PA}\) can be transformed into easierquestions about what can be demonstrated in \(\mathbf{GL}\).

\(\mathbf{GL}\) can also be outfitted with a possible world semanticsfor which it is sound and complete. A corresponding condition onframes for \(\mathbf{GL}\)-validity is that the frame be transitive,finite and irreflexive.

For a more detailed discussion, see the entry onprovability logic.

12. Advanced Modal Logic

The applications of modal logic to mathematics and computer sciencehave become increasingly important. Provability logic is only oneexample of this trend. The term “advanced modal logic”refers to a tradition in modal logic research that is particularlywell represented in departments of mathematics and computer science.This tradition has been woven into the history of modal logic rightfrom its beginnings (Goldblatt, 2006). Research into relationshipswith topology and algebras represents some of the very first technicalwork on modal logic. However the term ‘advanced modallogic’ generally refers to a second wave of work done since themid 1970s. Some examples of the many interesting topics dealt withinclude results on decidability (whether it is possible to computewhether a formula of a given modal logic is a theorem) and complexity(the costs in time and memory needed to compute such facts about modallogics). The next two sections describe examples of research in thistradition.

13. Bisimulation

Bisimulation provides a good example of the fruitful interactions thathave been developed between modal logic and computer science. Incomputer science, labeled transition systems (LTSs) are commonly usedto represent possible computation pathways during execution of aprogram. LTSs are generalizations of Kripke frames, consisting of aset \(W\) of states and a collection of \(i\)-accessibility relations\(R_i\), one for each computer process \(i\). Intuitively, \(wR_i w'\)holds exactly when \(w'\) is a state that results from applying theprocess \(i\) to state \(w\).

The language of poly-modal or dynamic logic introduces a collection ofmodal operators \(\Box_i\), one for each program \(i\) (Harel, 1984).Then \(\Box_i A\) states that sentence \(A\) holds in every result ofapplying \(i\). So ideas like the correctness and successfultermination of programs can be expressed in this language. Models forsuch a language are like Kripke models save that LTSs are used inplace of frames. Abisimulation is a counterpart relationbetween states of two such models such that exactly the samepropositional variables are true in counterpart states, and wheneverworld \(v\) is \(i\)-accessible from one of two counterpart states,then the other counterpart bears the \(i\)-accessibility relation tosome counterpart of \(v\). In short, the \(i\)-accessibility structureone can “see” from a given state mimics what one sees froma counterpart. Bisimulation is a weaker notion than isomorphism (abisimulation relation need not be 1-1), but it is sufficient toguarantee equivalence in processing.

In the 70s, bisimulation had already been developed by modal logiciansto help better understand the relationship between modal logic axiomsand their corresponding conditions on Kripke frames. Kripke’ssemantics provides a basis for translating modal formulas intosentences of first-order logic with quantification over possibleworlds. Replace metavariables \(A\) in an axiom with open sentences\(Ax\), and translate \(\Box Ax\) to \(\forall y(Rxy \rightarrowAy)\), in the result. (The translation for \(\Diamond Ax\) is given by\( \exists y(Rxy \amp Ay)\).) For example, the translation of theaxiom schema \(\Diamond \Box A\rightarrow A\) comes to \(\exists y(Rxy \amp \forall z(Ryz \rightarrow Az)) \rightarrow Ax\). This openformula with a free variable ‘\(x\)’ reflects what\(\Diamond \Box A\rightarrow A\) “says” in the language offirst-order logic. Obviously the translations of modal formulas arespecial; most first-order formulas are not equivalent to the result oftranslating modal formulas in this way. The modal translations form aspecial subset of the predicate logic language, which delimits whatmodal logic formulas can express.

Is there any interesting way to characterize the expressive power ofthe modal translations? The answer is that bisimulation serves exactlythat purpose. Van Benthem showed (Blackburn et al., 2001, p. 103) thata first-order formula is equivalent to a modal translation exactlywhen its holding in a model entails that it holds in any bisimularmodel, and the idea easily generalizes to the poly-modal case. Thissuggests that poly-modal logic lies at exactly the right level ofabstraction to describe, and reason about, computation and otherprocesses. (After all, what really matters there is the preservationof truth values of formulas in models, rather than the finer detailsof the frame structures.) Furthermore, the implicit translation ofmodal logics into well-understood fragments of predicate logicprovides a wealth of information of interest to computer scientists.As a result, a fruitful area of research in computer science hasdeveloped with bisimulation as its core idea (Ponseet al.1995).

14. Frame Validity and Incompleteness

Work on modal logic in the 60s was primarily concerned with obtainingcompleteness results with respect to various conditions on theaccessibility relation. However as research progressed into the 70s,deeper connections were discovered concerning what modal axiomsexpress about frames. A central idea in this work is the notion offrame validity, which differs from the kind of validity which was laidout in Section 6 above. There an argument was considered valid for aset of conditions \(C\) on frames exactly when for every model\(\langle W, R, v\rangle\) whose frame obeys \(C\), and every world\(w\) in \(W\), the truth of the premises at \(w\) entails the truthof the conclusion at \(w\). In short, model validity amounts topreservation of truth on every model. Frame validity, on the otherhand, focuses more clearly on the frames of the model. A sentence issaid to bevalid on a frame \(\langle W, R\rangle\) iff it istrue in every world in any model with frame \(\langle W, R\rangle\).Then an argument is ruledframe valid for a set of conditions\(C\) on frames iff it preserves frame validity, that is, for everyframe that obeys \(C\), if the premises are valid on that frame, thenso is the conclusion.

Frame validity appears a better way to understand what a modal axiomexpresses about frames. There are models that assign the axiom (M):\(\Box A\rightarrow A\) true, even though its frame does not satisfyreflexivity - the corresponding frame condition for (M). That isbecause the valuation function for a model can be specially crafted sothat it does the work of ensuring that \(\Box A\rightarrow A\) istrue. However, as we will soon see, if \(\Box A\rightarrow A\) isvalid for frame \(\langle W, R\rangle\), then it follows that\(\langle W, R\rangle\) is reflexive. By abstracting away from detailsabout the valuation function, one obtains better insight into therelationship between axioms and frame conditions.

The concept of frame validity provides a basis for translating whatmodal axioms express into sentences of a second-order language wherequantification is allowed over one-place predicate letters \(P\).Replace metavariables \(A\) with open sentences \(Px\), translate\(\Box Px\) to \(\forall y(Rxy \rightarrow Py)\), and close freevariables \(x\) and predicate letters \(P\) with universalquantifiers. For example, the predicate logic translation of the axiomschema \(\Box A\rightarrow A\) comes to \(\forall P \forall x[\forally(Rxy\rightarrow Py) \rightarrow Px\)]. (The basis for thequantification over the predicate letters P is that frame validityquantifies over all valuations of the propositional variables p, butvaluations over p are functions from the set of possible worlds totruth values, and these can be likened to properties of worldsexpressed by p, namely the property that world w has when p is truethere.)

Given this translation for \(\Box A\rightarrow A\), one mayinstantiate the variable \(P\) to an arbitrary one-place predicate,for example to the predicate \(Rx\) whose extension is the set of allworlds w such that \(Rxw\) for a given value of \(x\). Then oneobtains \(\forall x[\forall y(Rxy\rightarrow Rxy) \rightarrow Rxx\)],which reduces to \(\forall xRxx\), since \(\forall y(Rxy\rightarrowRxy)\) is a tautology. This illuminates the correspondence between\(\Box A\rightarrow A\) and reflexivity of frames \((\forall xRxx)\).Similar results hold for many other axioms and frame conditions. The“collapse” of second-order axiom conditions to first-orderframe conditions is very helpful in locating how axioms correspond toframe conditions, and in obtaining completeness results for variousmodal logics. For example, this is the core idea behind the elegantresults of Sahlqvist (1975), which are described in (Blackburn et al.,2001, Ch. 3, especially section 3.6).

The striking successes along these lines suggests that every modallogic can be shown to be sound and complete with respect to the frameconditions that its axioms express. Unfortunately, this is not thecase. Some logics are incomplete for their frame conditions as isillustrated by the following example (Boolos, 1993 pp. 148ff). Theprovability logic GL results from adding the axiom \(\Box(\BoxA\rightarrow A) \rightarrow \Box A\) to the basic modal logic K.System H results from adding the weaker axiom: \(\Box(\Box A\leftrightarrow A) \rightarrow \Box A\) to K. GL is stronger than H asit is able to prove the standard axiom for S4: \(\Box A \rightarrow\Box\Box A\), but H is not. The problem is that GL and H expressequivalent second-order conditions. That means in turn that H isincomplete, for it cannot prove a formula \(\Box A \rightarrow\Box\Box A\) which is in fact valid for the frames it expresses.

So from the frame validity perspective, there is no way to alwaysconvert the second-order translation of an axiom into a first-orderframe condition for which a given system is both sound and complete.The reason is that if there were, both GL and H would have to be soundand complete with respect to the same first order condition C. Butthat means (by soundness of GL) that \(\Box A \rightarrow \Box\Box A\)would be frame valid for C, but not provable in H. The upshot is thatin general, what modal logics express in the frame-validity paradigmmay be more powerful than what can be said in a first-orderlanguage.

15. Modal Logic and Games

The interaction between the theory of games and modal logic is aflourishing new area of research (van der Hoek and Pauly, 2007; vanBenthem, 2011, Ch. 10, and 2014). This work has interestingapplications to understanding cooperation and competition among agentsas information available to them evolves.

The Prisoner’s Dilemma illustrates some of the concepts in gametheory that can be analyzed using modal logics. Imagine two playersthat choose to either cooperate or defect. If both cooperate, theyboth achieve a reward of 3 points, if they both defect, they both get1 point, and if one cooperates and the other defects, the defectormakes off with 5 points and the cooperator gets nothing. If bothplayers are altruistic and motivated to maximize the sum of theirrewards, they will both cooperate, as this is the best they can dotogether. However, they are both tempted to defect to increase theirown reward from 3 to 5, leaving their opponent with nothing. On theother hand, if they are both rational, they may recognize that ifdefection is the best strategy, their opponent will choose this aswell, leaving them with only 1 point. So unless there is enough trustbetween the players to motivate cooperation, they will be doomed toreceiving 1 point apiece. However, if each thinks the other realizesthis, they may be willing to risk cooperating anyway.

An extended (or iterated) version of this game gives the playersmultiple moves, that is, repeated opportunities to play and collectrewards. If players have information about the history of the movesand their outcomes, new concerns come into play, as success in thegame depends on knowing their opponent’s strategy anddetermining (for example) when he/she can be trusted not to defect. Inmulti-player versions of the game, where players are drawn in pairsfrom a larger pool at each move, one’s own best strategy maywell depend on whether one can recognize one’s opponents and thestrategies they have adopted. (See Grim et. al., 1998 for fascinatingresearch on Interated Prisoner’s Dilemmas.)

In games like Chess, players take turns making their moves and theiropponents can see the moves made. If we adopt the convention that theplayers in a game take turns making their moves, then the IteratedPrisoner’s Dilemma is a game with missing information about thestate of play – the player with the second turn lacksinformation about what the other player’s last move was. Thisillustrates the interest of games with imperfect information.

The application of games to logic has a long history. One influentialapplication with important implications for linguistics is GameTheoretic Semantics (GTS) (Hintikka et. al. 1983), where validity isdefined by the outcome of a game between two players, one trying toverify and the other trying to falsify a given formula. GTS hassignificantly stronger resources that standard Tarski-style semantics,as it can be used (for example) to explain how meaning evolves in adiscourse (a sequence of sentences).

However, the work on games and modal logic to be described here issomewhat different. Instead of using games to analyze the semantics ofa logic, the modal logics at issue are used to analyze games. Thestructure of games and their play is very rich, as it involves thenature of the game itself (the allowed moves and the rewards for theoutcomes), the strategies (which are sequences of moves through time),and the flow of information available to the players as the gameprogresses. Therefore, the development of modal logic for games drawson features found in logics involving concepts like time, agency,preference, goals, knowledge, belief, and cooperation.

To provide some hint at this variety, here is a limited description ofsome of the modal operators that turn up in the analysis of games andsome of the things that can be expressed with them. The basic idea inthe semantics is that a game consists of a set of players 1, 2, 3,…, and a set of W of game states. For each player \(i\), thereis an accessibility relation \(R_i\) understood so that \(sR_i t\)holds for states \(s\) and \(t\) iff when the game has come to state\(s\) player \(i\) has the option of making a move that results in\(t\). This collection of relations defines a tree whose branchesdefine every possible sequence of moves in the game. The semanticsalso assigns truth-values to atoms that keep track of the payoffs. So,for example in a game like Chess, there could be an atom \(\win_i\)such that \(v(\win_i, s)=T\) iff state \(s\) is a win for player\(i\). Model operators \(\Box_i\) and \(\Diamond_i\) for each player\(i\) may then be given truth conditions as follows.

So \(\Box_i A\) \((\Diamond_i A)\) is true in s provided that sentence\(A\) holds true in every (some) state that \(i\) can chose from state\(s\). Given that \(\bot\) is a contradiction (so \({\sim}\bot\) is atautology), \(\Diamond_i {\sim}\bot\) is true at a state when it is\(i\)’s turn to move. For a two-player game \(\Box_1\bot\) &\(\Box_2\bot\) is true of a state that ends the game, because neither1 nor 2 can move. \(\Box_1\Diamond_2\)win\(_2\) asserts that player 1has a loss because whatever 1 does from the present state, 2 can winin the following move.

For a more general account of the player’s payoffs, orderingrelations \(\leq_i\) can be defined over the states so that \(s\leq_it\) means that \(i\)’s payoff for \(t\) is at least as good asthat for \(s\). Another generalization is to express facts aboutsequences \(q\) of moves, by introducing operators interpreted byrelations \(sR_q t\) indicating that the sequence \(q\) starting froms eventually arrives at \(t\). With these and related resources, it ispossible to express (for example) that \(q\) is \(i\)’s beststrategy given the present state.

It is crucial to the analysis of games to have a way to express theinformation available to the players. One way to accomplish this is toborrow ideas from epistemic logic. Here we may introduce anaccessibility relation \({\sim}_i\) for each player such that\(s{\sim}_i t\) holds iff \(i\) cannot distinguish between states\(s\) and \(t\). Then knowledge operators \(\rK_i\) for the playerscan be defined so that \(\rK_i A\) says at \(s\) that \(A\) holds inall worlds that \(i\) cannot distinguish from \(s\); that is, despite\(i\)’s ignorance about the state of play, he/she can still beconfident that \(A\). \(\rK\) operators may be used to say that player1 is in a position to resign, for he knows that 2 sees she has a win:\(\rK_1 \rK_2\Box_1\Diamond_2\win_2\).

Since player’s information varies as the game progresses, it isuseful to think of moves of the game as indexed by times, and tointroduce operators \(O\) and \(U\) from tense logic for‘next’ and ‘until’. Then \(K_i OA \rightarrowOK_i A\) expresses that player \(i\) has “perfect recall”,that is, that when \(i\) knows that \(A\) happens next, then at thenext moment \(i\) has not forgotten that \(A\) has happened. Thisillustrates how modal logics for games can reflect cognitiveidealizations and a player’s success (or failure) at living upto them.

The technical side of the modal logics for games is challenging. Theproject of identifying systems of rules that are sound and completefor a language containing a large collection of operators may beguided by past research, but the interactions between the variety ofaccessibility relations leads to new concerns. Furthermore, thecomputational complexity of various systems and their fragments is alarge landscape largely unexplored.

Game theoretic concepts can be applied in a surprising variety of ways– from checking an argument for validity to succeeding in thepolitical arena. So there are strong motivations for formulatinglogics that can handle games. What is striking about this research isthe power one obtains by weaving together logics of time, agency,knowledge, belief, and preference in a unified setting. The lessonslearned from that integration have value well beyond what theycontribute to understanding games.

16. Quantifiers in Modal Logic

It would seem to be a simple matter to outfit a modal logic with thequantifiers \(\forall\) (all) and \(\exists\) (some). One would simplyadd the standard (or classical) rules for quantifiers to theprinciples of whichever propositional modal logic one chooses.However, adding quantifiers to modal logic involves a number ofdifficulties. Some of these are philosophical. For example, Quine(1953) has famously argued that quantifying into modal contexts issimply incoherent, a view that has spawned a gigantic literature.Quine’s complaints do not carry the weight they once did. SeeBarcan (1990) for a good summary, and note Kripke’s (2017)(written in the 60’s for a class with Quine) which provides astrong formal argument that there can be nothing wrong with“quantifying in”.

A second kind of complication is technical. There is a wide variety inthe choices one can make in the semantics for quantified modal logic,and the proof that a system of rules is correct for a given choice canbe difficult. The work of Corsi (2002) and Garson (2005) goes some waytowards bringing unity to this terrain, and Johannesson (2018)introduces constraints that help reduce the number of options;nevertheless the situation still remains challenging.

Another complication is that some logicians believe that modalityrequires abandoning classical quantifier rules in favor of the weakerrules of free logic (Garson 2001). The main points of disagreementconcerning the quantifier rules can be traced back to decisions abouthow to handle the domain of quantification. The simplest alternative,the fixed-domain (sometimes called the possibilist) approach, assumesa single domain of quantification that contains all the possibleobjects. On the other hand, the world-relative (or actualist)interpretation, assumes that the domain of quantification changes fromworld to world, and contains only the objects that actually exist in agiven world.

The fixed-domain approach requires no major adjustments to theclassical machinery for the quantifiers. Modal logics that areadequate for fixed domain semantics can usually be axiomatized byadding principles of a propositional modal logic to classicalquantifier rules together with the Barcan Formula \((BF)\) (Barcan1946). (For an account of some interesting exceptions see Cresswell(1995).)

The fixed-domain interpretation has advantages of simplicity andfamiliarity, but it does not provide a direct account of the semanticsof certain quantifier expressions of natural language. We do not thinkthat ‘Some man exists who signed the Declaration ofIndependence’ is true, at least not if we read‘exists’ in the present tense. Nevertheless, this sentencewas true in 1777, which shows that the domain for the natural languageexpression ‘some man exists who’ changes to reflect whichmen exist at different times. A related problem is that on thefixed-domain interpretation, the sentence \(\forall y\Box \existsx(x=y)\) is valid. Assuming that \(\exists x(x=y)\) is read: \(y\)exists, \(\forall y\Box \exists x(x=y)\) says that everything existsnecessarily. However, it seems a fundamental feature of common ideasabout modality that the existence of many things is contingent andthat different objects exist in different possible worlds.

The defender of the fixed-domain interpretation may respond to theseobjections by insisting that on his (her) reading of the quantifiers,the domain of quantification containsall possible objects,not just the objects that happen to exist at a given world. So thetheorem \(\forall y\Box \exists x(x=y)\) makes the innocuous claimthat everypossible object is necessarily found in the domainof all possible objects. Furthermore, those quantifier expressions ofnatural language whose domain is world (or time) dependent can beexpressed using the fixed-domain quantifier \(\exists x\) and apredicate letter \(E\) with the reading ‘actually exists’.For example, instead of translating ‘Some \(M\)an exists who\(S\)igned the Declaration of Independence’ by

the defender of fixed domains may write:

thus ensuring the translation is counted false at the present time.Cresswell (1991) makes the interesting observation that world-relativequantification has limited expressive power relative to fixed-domainquantification. World-relative quantification can be defined withfixed-domain quantifiers and \(E\), but there is no way to fullyexpress fixed-domain quantifiers with world-relative ones. Althoughthis argues in favor of the classical approach to quantified modallogic, the translation tactic also amounts to something of aconcession in favor of free logic, for the world-relative quantifiersso defined obey exactly the free logic rules.

A problem with the translation strategy used by defenders offixed-domain quantification is that rendering the English into logicis less direct, since \(E\) must be added to all translations of allsentences whose quantifier expressions have domains that are contextdependent. A more serious objection to fixed-domain quantification isthat it strips the quantifier of a role which Quine recommended forit, namely to record robust ontological commitment. On this view, thedomain of \(\exists x\) must contain only entities that areontologically respectable, and possible objects are too abstract toqualify. Actualists of this stripe will want to develop the logic of aquantifier \(\exists x\) which reflects commitment to what is actualin a given world rather than to what is merely possible.

However, some work on actualism tends to undermine this objection. Forexample, Linsky and Zalta (1994) and Williamson (2013) argue that thefixed-domain quantifier can be given an interpretation that isperfectly acceptable to actualists. Pavone (2018) even contends thaton the haecceitist interpretation, which quantifies over individualessences, fixed domains are required. Actualists who employ possibleworlds semantics routinely quantify over possible worlds in theirsemantical theory of language. So it would seem that possible worldsare actual by these actualist’s lights. By populating the domainwith abstract entities no more objectionable than possible worlds,actualists may vindicate the Barcan Formula and classicalprinciples.

However, recent work suggests that the fixed domain option may not beas actualist as originally thought; see Menzel 2020 and the entry onthe possibilism-actualismdebate. And some actualists might respond that they need not becommitted to the actuality of possible worlds so long as it isunderstood that quantifiers used in their theory of language lackstrong ontological import. Furthermore, Hayaki (2006) argues thatquantifying over abstract entities is actually incompatible with anyserious form of actualism. In any case, it is open to actualists (andnon-actualists as well) to investigate the logic of quantifiers withmore robust domains, for example domains excluding possible worlds andother such abstract entities, and containing only the spatio-temporalparticulars found in a given world. For quantifiers of this kind,world-relative domains are appropriate.

Such considerations motivate interest in systems that acknowledge thecontext dependence of quantification by introducing world-relativedomains. Here each possible world has its own domain of quantification(the set of objects that actually exist in that world), and thedomains vary from one world to the next. When this decision is made, adifficulty arises for classical quantification theory. Notice that thesentence \(\exists x(x=t)\) is a theorem of classical logic, and so\(\Box \exists x(x=t)\) is a theorem of \(\bK\) by the NecessitationRule. Let the term \(t\) stand for Saul Kripke. Then this theorem saysthat it is necessary that Saul Kripke exists, so that he is in thedomain of every possible world. The whole motivation for theworld-relative approach was to reflect the idea that objects in oneworld may fail to exist in another. If standard quantifier rulers areused, however, every term \(t\) must refer to something that exists inall the possible worlds. This seems incompatible with our ordinarypractice of using terms to refer to things that only existcontingently.

One response to this difficulty is simply to eliminate terms. Kripke(1963) gives an example of a system that uses the world-relativeinterpretation and preserves the classical rules. However, the costsare severe. First, his language is artificially impoverished, andsecond, the rules for the propositional modal logic must beweakened.

Presuming that we would like a language that includes terms, and thatclassical rules are to be added to standard systems of propositionalmodal logic, a new problem arises. In such a system, it is possible toprove \((CBF)\), the converse of the Barcan Formula.

This fact has serious consequences for the system’s semantics.It is not difficult to show that every world-relative model of\((CBF)\) must meet condition \((ND)\) (for ‘nesteddomains’).

• \((ND)\) If \(wRv\)then the domain of \(w\) is a subset of the domain of \(v\).

However \((ND)\) conflicts with the point of introducingworld-relative domains. The whole idea was that existence of objectsis contingent so that there are accessible possible worlds where oneof the things in our world fails to exist.

A straightforward solution to these problems is to abandon classicalrules for the quantifiers and to adopt rules for free logic\((\mathbf{FL})\) instead. The rules of \(\mathbf{FL}\) are the sameas the classical rules, except that inferences from \(\forall xRx\)(everything is real) to \(Rp\) (Pegasus is real) are blocked. This isdone by introducing a predicate ‘\(E\)’ (for‘actually exists’) and modifying the rule of universalinstantiation. From \(\forall xRx\) one is allowed to obtain \(Rp\)only if one also has obtained \(Ep\). Assuming that the universalquantifier \(\forall x\) is primitive, and the existential quantifier\(\exists x\) is defined by \(\exists xA =_{df} {\sim}\forallx{\sim}A\), then \(\mathbf{FL}\) may be constructed by adding thefollowing two principles to the rules of propositional logic.

Free Universal Generalization.
If \(B\rightarrow(Ey\rightarrow A(y))\) is a theorem, so is\(B\rightarrow \forall xA(x)\).

Free Universal Instantiation.
\(\forall xA(x)\rightarrow(Et\rightarrow A(t))\)

(Here it is assumed that \(A(x)\) is any well-formed formula ofpredicate logic and that \(A(y)\) and \(A(t)\) result from replacing\(y\) and \(t\) properly for each occurrence of \(x\) in \(A(x)\).)Note that the instantiation axiom is restricted by mention of \(Et\)in the antecedent. The rule of Free Universial Generalization ismodified in the same way. In \(\mathbf{FL}\), proofs of formulas like\(\exists x\Box(x=t)\), \(\forall y\Box \exists x(x=y)\), \((CBF)\),and \((BF)\), which seem incompatible with the world-relativeinterpretation, are blocked.

One philosophical objection to \(\mathbf{FL}\) is that \(E\) appearsto be an existence predicate, and many would argue that existence isnot a legitimate property like being green or weighing more than fourpounds. So philosophers who reject the idea that existence is apredicate may object to \(\mathbf{FL}\). However in most (but not all)quantified modal logics that include identity \((=)\) these worriesmay be skirted by defining \(E\) as follows.

The most general way to formulate quantified modal logic is to create\(\mathbf{FS}\) by adding the rules of \(\mathbf{FL}\) to a givenpropositional modal logic \(\mathbf{S}\). In situations whereclassical quantification is desired, one may simply add \(Et\) as anaxiom to \(\mathbf{FS}\), so that the classical principles becomederivable rules. Adequacy results for such systems can be obtained formost choices of the modal logic \(\mathbf{S}\), but there areexceptions (Cresswell (1995).

There is another way to formulate quantified modal logics forworld-relative domains that avoids the non-standard quantifier rulesof free logic and allows term constants in the language. Deutsch(1990) shows how to define such a semantics, where the classicalprinciple \(\exists x(x=t)\) comes out valid. His strategy is inspiredby Kaplan’s (1989) idea that validity and necessity may partcompany. (See the discussion of two-dimensional semantics inSection 10 above.) Kaplan showed that there are sentences such as ‘I amhere now’ that qualify as logically valid, because they are truein any context of their assertion, but which are not necessary. Thatsuggests a reply to anyone who objects to the classical theorem\(\exists x(x=t)\) on the grounds that ‘\(t\) exists’ isnot necessary. One need only point out that the validity of \(\existsx(x=t)\) is in fact compatible with its contingency.

Special adjustments to the formal semantics are needed to flesh outthis idea. Deutsch introduces what he calls ‘contexts oforigin’ as sequences of possible worlds. (These are not to beconfused with Kaplan’s linguistic contexts.) However, Stephanou(2002) shows how to streamline the definition of a model so that thisextra machinery is avoided. Deutsch’s main idea is that a modeldistinguishes one of the possible worlds \(w^*\) as actual, and theterm constants are directly assigned referents in the domain for\(w^*\). That ensures that \(\exists x(x=t)\) is true in \(w^*\).Although \(\exists x(x=t)\) is false in other worlds where thereferent of \(t\) does not exist, the definition of validity for thissemantics rates a sentence true provided it is true at the actualworld \(w^*\) for each model. The result is that \(\exists x(x=t)\)and all classical quantifier principles are rated valid, even though\(\Box\exists x(x=t)\) is not.

Stephanou (2002) provides a set of axioms and rules that exactlycapture this notion of validity. Classical laws of quantification arepreserved in the sense that the provable formulas lacking any modaloperator are the classical ones. However, restrictions must be placedon the rules of propositional modal logic. The Necessitation Rule (If\(A\) is a theorem, then so is \(\Box A\)) cannot be accepted because\(\exists x(x=t)\) is valid, while \(\Box\exists x(x=t)\) is not.Furthermore, the rules for quantification are more complex. Two axiomsof Universal Instantiation are needed. One is restricted: \(\forallxA(x)\rightarrow(Ft\rightarrow A(t))\), where \(Ft\) is any atomicsentence containing term \(t\). Since the semantics requires allpredicate letters to have extensions for a world in the domain of thatworld, \(Ft\) ensures that \(t\) refers to something that exists. Sothis restricted axiom reminds one of Free Universal Instantiation. Thesecond axiom is an unrestricted form of Instantiation: \(\forallxA(x)\rightarrow A(t)\). However, this principle comes with theproviso that once it is used in a proof, no axioms or rules may beused other than it and Modus Ponens. This has the effect of blockingthe use of Necessitation to obtain \(\Box\exists x(x=t)\) from\(\exists x(x=t)\).

Note that this strategy cannot treat all proper names in English asterms of the formal language, since those terms refer to what existsin the actual world. Therefore names for fictional entities(‘Pegasus’) must be dealt with in another way, perhapswith Russell’s theory of descriptions. An alternative treatmentwould also be need in a temporal logic for names of those who aredeceased (‘Benjamin Franklin’).

A final complication in the semantics for quantified modal logic isworth mentioning. It arises when non-rigid expressions such as‘the inventor of bifocals’ are introduced to the language.A term is non-rigid when it picks out different objects in differentpossible worlds. The semantical value of such a term can be given bywhat Carnap (1947) called an individual concept, a function that picksout the denotation of the term for each possible world. One approachto dealing with non-rigid terms is to employ Russell’s theory ofdescriptions. However, in a language that treats non rigid expressionsas genuine terms, it turns out that neither the classical nor the freelogic rules for the quantifiers are acceptable. (The problem cannot beresolved by weakening the rule of substitution for identity.) Asolution to this problem is to employ a more general treatment of thequantifiers, where the domain of quantification contains individualconcepts rather than objects. This more general interpretationprovides a better match between the treatment of terms and thetreatment of quantifiers and results in systems that are adequate forclassical or free logic rules (depending on whether the fixed domainsor world-relative domains are chosen). It also provides a languagewith strong and much needed expressive powers (Bressan, 1973, Belnapand Müller, 2013a, 2013b). (See also Aloni (2005) who exploresthe pros and cons of quantifying over individual concepts inepistemic logic.)

Bibliography

Texts on modal logic with philosophers in mind include Hughes andCresswell (1968, 1984, 1996), Chellas (1980), Fitting and Mendelsohn(1998), Garson (2013), Girle (2009), and Humberstone (2015).

Humberstone (2015) provides a superb guide to the literature on modallogics and their applications to philosophy. The bibliography (of overa thousand entries) provides an invaluable resource for all the majortopics, including logics of tense, obligation, belief, knowledge,agency and nomic necessity.

Gabbay and Guenthner (2001) provides useful summary articles on majortopics, while Blackburn et. al. (2007) is an invaluable resource froma more advanced perspective.

An excellent bibliography of historical sources can be found in Hughesand Cresswell (1968).

• Aloni, M., 2005, “Individual Concepts in Modal PredicateLogic,”Journal of Philosophical Logic, 34:1–64.
• Anderson, A. and N. Belnap, 1975, 1992,Entailment: The Logicof Relevance and Necessity, vol. 1 (1975), vol. 2 (1992),Princeton: Princeton University Press.
• Barcan (Marcus), R., 1947, “A Functional Calculus of FirstOrder Based on Strict Implication,”Journal of SymbolicLogic, 11: 1–16.
• –––, 1967, “Essentialism in ModalLogic,”Noûs, 1: 91–96.
• –––, 1990, “A Backwards Look atQuine’s Animadversions on Modalities,” in R. Bartrett andR. Gibson (eds.),Perspectives on Quine, Cambridge:Blackwell.
• Belnap, N., M. Perloff, and M. Xu, 2001,Facing theFuture, New York: Oxford University Press.
• Belnap, N. and T. Müller, 2013a, “CIFOL: A CaseIntensional First Order Logic (I): Toward a Logic of Sorts,”Journal of Philosophical Logic, doi:10.1007/s10992-012-9267-x
• –––, 2013b, “BH-CIFOL: A Case IntensionalFirst Order Logic (II): Branching Histories,”Journal ofPhilosophical Logic, doi:10.1007/s10992-013-9292-4
• Bencivenga, E., 1986, “Free Logics,” in D. Gabbay andF. Guenthner (eds.),Handbook of Philosophical Logic, III.6,Dordrecht: D. Reidel, 373–426.
• Benthem, J. F. van, 1982,The Logic of Time, Dordrecht:D. Reidel.
• –––, 1983,Modal Logic and ClassicalLogic, Naples: Bibliopolis.
• –––, 2010,Modal Logic for Open Minds,Stanford: CSLI Publications.
• –––, 2011,Logical Dynamics of Informationand Interaction, Cambridge: Cambridge University Press.
• –––, 2014,Logic in Games, Cambridge,Mass: MIT Press.
• Blackburn, P., with M. de Rijke and Y. Venema, 2001,ModalLogic, Cambridge: Cambridge University Press.
• Blackburn, P., with J. van Bentham and F. Wolter, 2007,Handbook of Modal Logic, Amsterdam: Elsevier.
• Bonevac, D., 1987,Deduction, Part II, Palo Alto:Mayfield Publishing Company.
• Boolos, G., 1993,The Logic of Provability, Cambridge:Cambridge University Press.
• Bressan, A., 1973,A General Interpreted Modal Calculus,New Haven: Yale University Press.
• Bull, R. and K. Segerberg, 1984, “Basic Modal Logic,”in D. Gabbay and F. Guenthner (eds.),Handbook of PhilosophicalLogic, II.1, Dordrecht: D. Reidel, 1–88.
• Carnap, R., 1947,Meaning and Necessity, Chicago: U.Chicago Press.
• Carnielli, W. and C. Pizzi, 2008,Modalities andMultimodalities, Heidelberg: Springer-Verlag.
• Chagrov, A. and M. Zakharyaschev, 1997,Modal Logic,Oxford: Oxford University Press.
• Chalmers, D., 1996,The Conscious Mind, New York: OxfordUniversity Press.
• –––, 2002, “The Components ofContent”, in D. Chalmers (ed.),Philosophy of Mind:Classical and Contemporary Readings, Oxford: Oxford UniversityPress, 608–633.
• –––, 2006, “The Foundations ofTwo-Dimensional Semantics”, in M. Garcia-Carpintero and J.Macia, Two-Dimensional Semantics: Foundations andApplications, Oxford: Oxford University Press, 55–140.
• Chellas, B., 1980,Modal Logic: An Introduction,Cambridge: Cambridge University Press.
• Cresswell, M. J., 2001, “Modal Logic”, in L. Goble(ed.),The Blackwell Guide to Philosophical Logic, Oxford:Blackwell, 136–158.
• –––, 1991, “In Defence of the BarcanFormula,”Logique et Analyse, 135–136:271–282.
• –––, 1995, “Incompleteness and the Barcanformula”,Journal of Philosophical Logic, 24:379–403.
• Cocchiarella, N. and M. Freund, 2008,Modal Logic AnIntroduction to its Syntax and Semantics, New York: Oxford.
• Corsi, G., 2002, “A Unified Completeness Theorem forQuantified Modal Logics,”Journal of Symbolic Logic,67: 1483–1510.
• Crossley, J and L. Humberstone, 1977, “The Logic of‘Actuality’”,Reports on MathematicalLogic, 8: 11–29.
• Deutsch, H., 1990, “Contingency and Modal Logic,”Philosophical Studies, 60: 89–102.
• Fitting, M. and R. Mendelsohn, 1998,First Order ModalLogic, Dordrecht: Kluwer.
• Gabbay, D., 1976,Investigations in Modal and TenseLogics, Dordrecht: D. Reidel.
• –––, 1994,Temporal Logic: MathematicalFoundations and Computational Aspects, New York: OxfordUniversity Press.
• Gabbay, D. and F. Guenthner, F. (eds.), 2001,Handbook ofPhilosophical Logic, second edition, volume 3, Dordrecht: D.Reidel,
• Garson, J., 2001, “Quantification in Modal Logic,” inGabbay and Guenthner (2001), 267–323.
• –––, 2005, “Unifying Quantified ModalLogic,”Journal of Philosophical Logic, 34:621–649.
• –––, 2013,Modal Logic for Philosophers,Second Edition, Cambridge: Cambridge University Press.
• Girle, R., 2009,Modal Logics and Philosophy (2ndEdition), Routledge, New York, New York.
• Grim, P., Mar, G, and St. Denis, P., 1998,The PhilosophicalComputer, Cambridge, Mass.: MIT Press.
• Goldblatt, R., 1993,Mathematics of Modality, CSLILecture Notes #43, Chicago: University of Chicago Press.
• –––, 2006, “Mathematical Modal Logic: aView of its Evolution,” in D. Gabbay and J. Woods (eds.),Handbook of the History of Logic, vol. 6, Amsterdam:Elsevier.
• Harel, D., 1984, “Dynamic Logic,” in D. Gabbay and F.Guenthner (eds.),Handbook of Philosophical Logic, II.10,Dordrecht: D. Reidel, 497–604.
• Hayaki, R., 2006, “Contingent Objects and the BarcanFormula,”Erkenntnis, 64: 75–83.
• Hintikka, J., 1962,Knowledge and Belief: An Introduction tothe Logic of the Two Notions, Ithaca, NY: Cornell UniversityPress.
• –––, 1983,The Game of Language,Dordrecht: D. Reidel.
• Hilpinen, R., 1971,Deontic Logic: Introductory and SystematicReadings, Dordrecht: D. Reidel.
• van der Hoek, W. and Pauly, M., 2007, “Model Logics forGames and Information,” Chapter 20 of Blackburn et. al., 2007.
• Hughes, G. and M. Cresswell, 1968,An Introduction to ModalLogic, London: Methuen.
• –––, 1984,A Companion to Modal Logic,London: Methuen.
• –––, 1996,A New Introduction to ModalLogic, London: Routledge.
• Humberstone, L. 2015,Philosophical Applications of ModalLogic, College Publications, London.
• Johannesson, E., 2018, “Partial Semantics for QuantifiedModal Logics,”Journal of Philosophical Logic,1–12.
• Kaplan, D., 1989, “Demonstratives”, inThemes fromKaplan, Oxford: Oxford University Press.
• Kripke, S., 1963, “Semantical Considerations on ModalLogic,”Acta Philosophica Fennica, 16:83–94.
• –––, 1980,Naming and Necessity,Cambridge, Mass.: Harvard University Press.
• –––, 2017, “Quantified Modality andEssentialism,”Nous, 51, #2: 221–234.
• Konyndik, K., 1986,Introductory Modal Logic, Notre Dame:University of Notre Dame Press.
• Kvart, I., 1986,A Theory of Counterfactuals,Indianapolis: Hackett Publishing Company.
• Lemmon, E. and D. Scott, 1977,An Introduction to ModalLogic, Oxford: Blackwell.
• Lewis, C.I. and C.H. Langford, 1959 (1932),SymbolicLogic, New York: Dover Publications.
• Lewis, D., 1973,Counterfactuals, Cambridge, Mass.:Harvard University Press.
• Linsky, B. and E. Zalta, 1994, “In Defense of the SimplestQuantified Modal Logic,”Philosophical Perspectives,(Logic and Language), 8: 431–458.
• Mares, E., 2004,Relevant Logic: A PhilosophicalInterpretation, Cambridge: Cambridge University Press.
• Menzel, C., 2020, “In Defense of thePossibilism–Actualism Distinction,”PhilosophicalStudies, 177(7): 1971–1997. doi:10.1007/s11098-019-01294-0
• Mints, G. 1992,A Short Introduction to Modal Logic,Chicago: University of Chicago Press.
• Ponse, A., with M. de Rijke, and Y. Venema, 1995,Modal Logicand Process Algebra, A Bisimulation Perspective, Stanford: CSLIPublications.
• Pavone, L., 2018, “Plantinga’s Haecceitism andSimplest Quantified Modal Logic,”Logic and LogicalPhilosophy, 27: 151–160.
• Popkorn, S., 1995,First Steps in Modal Logic, Cambridge:Cambridge University Press.
• Prior, A. N., 1957,Time and Modality, Oxford: ClarendonPress.
• –––, 1967,Past, Present and Future,Oxford: Clarendon Press.
• Quine, W. V. O., 1953, “Reference and Modality”, inFrom a Logical Point of View, Cambridge, Mass.: HarvardUniversity Press. 139–159.
• Rescher, N, and A. Urquhart, 1971,Temporal Logic, NewYork: Springer Verlag.
• Sahlqvist, H., 1975, “Completeness and Correspondence inFirst and Second Order Semantics for Modal Logic,” in S. Kanger(ed.),Proceedings of the Third Scandinavian Logic Symposium,Amsterdam: North Holland, 110–143.
• Stalnaker, R., 1968, “A Theory of Conditionals,”, inN. Rescher (ed.),Studies in Logical Theory, Oxford:Blackwell, 98–112.
• Stephanou, Y., 2002, “Investigations into Quantified ModalLogic,” Notre Dame Journal of Formal Logic,43, #4:193–220.
• Thomason, R., 1984, “Combinations of Tense andModality”, in D. Gabbay and F. Guenthner (eds.),Handbook ofPhilosophical Logic, II.3, Dordrecht: D. Reidel,135–165.
• Williamson, T., 2013,Modal Logic as Metaphysics,Oxford: Oxford University Press.
• Zeman, J., 1973,Modal Logic, The Lewis-Modal Systems,Oxford: Oxford University Press.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

• Advances in Modal Logic
• List of Resources from Wikipedia
• Modal Logic Handbook by Blackburn, Bentham, and Wolter
• John McCarthy’s Modal Logic Page

Related Entries

logic, history of: modal logic |logic: classical |logic: deontic |logic: free |logic: provability |logic: relevance |logic: temporal |possibilism-actualism debate |possible worlds